English
Two AddGroupWithOne structures on R are equal if their additive structure and the unit coincide.
Русский
Две структуры AddGroupWithOne на R равны, если совпадают их аддитивная структура и единица.
LaTeX
$$$\\\\forall A,B \\,\\in \\, \\text{AddGroupWithOne}(R), \\\\ (A\\+_A = B\\+_B) \\\\land (1_A = 1_B) \\\\Rightarrow A = B.$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : AddGroupWithOne R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_one :
(letI := inst₁;
One.one :
R) =
(letI := inst₂;
One.one)) :
inst₁ = inst₂ :=
by
have : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne := AddMonoidWithOne.ext h_add h_one
have : inst₁.toNatCast = inst₂.toNatCast := congrArg (·.toNatCast) this
have h_group : inst₁.toAddGroup = inst₂.toAddGroup := by ext : 1; exact h_add
injection h_group with h_group; injection h_group
have : inst₁.toIntCast.intCast = inst₂.toIntCast.intCast := by funext n;
cases n with
| ofNat n => rewrite [Int.ofNat_eq_coe, inst₁.intCast_ofNat, inst₂.intCast_ofNat]; congr
| negSucc n => rewrite [inst₁.intCast_negSucc, inst₂.intCast_negSucc]; congr
rcases inst₁ with @⟨⟨⟩⟩; rcases inst₂ with @⟨⟨⟩⟩
congr
