∀ {R : Type u_1} [inst : CommSemiring R] (asIdeal asIdeal_1 : Ideal R) (e_asIdeal : asIdeal = asIdeal_1)
  (isPrime : asIdeal.IsPrime), { asIdeal := asIdeal, isPrime := isPrime } = { asIdeal := asIdeal_1, isPrime := ⋯ }