-- Mathlib/Algebra/Ring/Ext.lean
theorem AddMonoidWithOne.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₂

Proof state:
case mk.mk.mk.mk
R : Type u
toAddMonoid✝¹ : AddMonoid R
toOne✝¹ : One R
natCast✝¹ : ℕ → R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
toAddMonoid✝ : AddMonoid R
toOne✝ : One R
natCast✝ : ℕ → R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ mk natCast_zero✝¹ natCast_succ✝¹ = mk natCast_zero✝ natCast_succ✝

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ inst₁ = inst₂

Tactic:
have h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid := by ext : 1; exact h_add

Result:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
⊢ inst₁ = inst₂

Proof state:
case h
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
n : ℕ
⊢ NatCast.natCast n = NatCast.natCast n

Tactic:
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

Result:
no goals

Proof state:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨⟨⟩⟩

Result:
case mk.mk
R : Type u
inst₂ : AddMonoidWithOne R
toAddMonoid✝ : AddMonoid R
toOne✝ : One R
natCast✝ : ℕ → R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ mk natCast_zero✝ natCast_succ✝ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
⊢ inst₁ = inst₂

Tactic:
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

Result:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
⊢ NatCast.natCast = NatCast.natCast

Tactic:
funext n

Result:
case h
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
n : ℕ
⊢ NatCast.natCast n = NatCast.natCast n

Proof state:
case h.succ
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
n : ℕ
h : NatCast.natCast n = NatCast.natCast n
⊢ NatCast.natCast (n + 1) = NatCast.natCast (n + 1)

Tactic:
rw [inst₁.natCast_succ, inst₂.natCast_succ, h_add]

Result:
case h.succ
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
n : ℕ
h : NatCast.natCast n = NatCast.natCast n
⊢ NatCast.natCast n + 1 = NatCast.natCast n + 1

Proof state:
case h.zero
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
⊢ NatCast.natCast 0 = NatCast.natCast 0

Tactic:
rewrite [inst₁.natCast_zero, inst₂.natCast_zero]

Result:
case h.zero
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
⊢ 0 = 0

Proof state:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ toAddMonoid = toAddMonoid

Tactic:
ext : 1

Result:
case h_mul
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ HAdd.hAdd = HAdd.hAdd

Proof state:
case h.zero
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
⊢ 0 = 0

Tactic:
exact congrArg (@Zero.zero R) h_zero'

Result:
no goals

Proof state:
case mk.mk
R : Type u
inst₂ : AddMonoidWithOne R
toAddMonoid✝ : AddMonoid R
toOne✝ : One R
natCast✝ : ℕ → R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ mk natCast_zero✝ natCast_succ✝ = inst₂

Tactic:
rcases inst₂ with @⟨⟨⟩⟩

Result:
case mk.mk.mk.mk
R : Type u
toAddMonoid✝¹ : AddMonoid R
toOne✝¹ : One R
natCast✝¹ : ℕ → R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
toAddMonoid✝ : AddMonoid R
toOne✝ : One R
natCast✝ : ℕ → R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ mk natCast_zero✝¹ natCast_succ✝¹ = mk natCast_zero✝ natCast_succ✝

Proof state:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
⊢ inst₁ = inst₂

Tactic:
have h_one' : inst₁.toOne = inst₂.toOne :=
  congrArg One.mk h_one

Result:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : toAddMonoid = toAddMonoid
h_zero' : AddMonoid.toZero = AddMonoid.toZero
h_one' : toOne = toOne
⊢ inst₁ = inst₂