English
Two Ring structures on R are equal if their additive and multiplicative layers align through substructures.
Русский
Две структуры Ring на R равны, если их аддитивная и мультипликативная части согласованы.
LaTeX
$$$\\\\forall A,B \\,\\in \\, \\text{Ring}(R), \\\\ (A{\\\\:}\\\\text{toAddCommGroup}) = (B{\\\\:}\\\\text{toAddCommGroup}) \\\\land (A{\\\\:}\\\\text{toNonAssocRing}) = (B{\\\\:}\\\\text{toNonAssocRing}) \\\\Rightarrow A=B.$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : Ring R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ := by
-- Show that enough substructures are equal.
have h₁ : inst₁.toSemiring = inst₂.toSemiring := by ext : 1 <;> assumption
have h₂ : inst₁.toNonAssocRing = inst₂.toNonAssocRing := by
ext : 1 <;>
assumption
/- We prove that the `SubNegMonoid`s are equal because they are one
field away from `Sub` and `Neg`, enabling use of `injection`. -/
have h₃ : (inst₁.toAddCommGroup).toAddGroup.toSubNegMonoid = (inst₂.toAddCommGroup).toAddGroup.toSubNegMonoid :=
congrArg (@AddGroup.toSubNegMonoid R) <| by ext : 1; exact h_add
cases inst₁; cases inst₂
congr <;>
solve
| injection h₂
| injection h₃
