English
Extensionality for AddMonoidWithOne: equality of addition structure and of the one element implies equality of the whole object.
Русский
Extensionality для AddMonoidWithOne: равенство структуры сложения и единицы влечёт равенство всей структуры.
LaTeX
$$$ \text{ext } (h\_add) (h\_one) \Rightarrow inst = inst' $$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : AddMonoidWithOne R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_one :
(letI := inst₁;
One.one :
R) =
(letI := inst₂;
One.one :
R)) :
inst₁ = inst₂ :=
by
have h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid := by ext : 1; exact h_add
have h_zero' : inst₁.toZero = inst₂.toZero := congrArg (·.toZero) h_monoid
have h_one' : inst₁.toOne = inst₂.toOne := congrArg One.mk h_one
have h_natCast : inst₁.toNatCast.natCast = inst₂.toNatCast.natCast := by funext n;
induction n with
| zero =>
rewrite [inst₁.natCast_zero, inst₂.natCast_zero]
exact congrArg (@Zero.zero R) h_zero'
| succ n h =>
rw [inst₁.natCast_succ, inst₂.natCast_succ, h_add]
exact congrArg₂ _ h h_one
rcases inst₁ with @⟨⟨⟩⟩; rcases inst₂ with @⟨⟨⟩⟩
congr
