∀ {R : Type u_1} {inst : CommSemiring R} {asIdeal : Ideal R} {isMaximal : asIdeal.IsMaximal} {asIdeal_1 : Ideal R}
  {isMaximal_1 : asIdeal_1.IsMaximal},
  { asIdeal := asIdeal, isMaximal := isMaximal } = { asIdeal := asIdeal_1, isMaximal := isMaximal_1 } →
    asIdeal = asIdeal_1