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

Proof state:
case mk.mk.mk.mk
R : Type u
toAddMonoidWithOne✝¹ : AddMonoidWithOne R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul✝¹ : ℤ → R → R
zsmul_zero'✝¹ : ∀ (a : R), zsmul✝¹ 0 a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), zsmul✝¹ (↑n.succ) a = zsmul✝¹ (↑n) a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), zsmul✝¹ (Int.negSucc n) a = -zsmul✝¹ (↑n.succ) a
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
intCast✝¹ : ℤ → R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toAddMonoidWithOne✝ : AddMonoidWithOne R
toNeg✝ : Neg R
toSub✝ : Sub R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul✝ : ℤ → R → R
zsmul_zero'✝ : ∀ (a : R), zsmul✝ 0 a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), zsmul✝ (↑n.succ) a = zsmul✝ (↑n) a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), zsmul✝ (Int.negSucc n) a = -zsmul✝ (↑n.succ) a
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
intCast✝ : ℤ → R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝¹ : toAddMonoidWithOne = toAddMonoidWithOne
this✝ : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast
toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid
toNeg_eq✝ : toNeg = toNeg
toSub_eq✝ : toSub = toSub
zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul
this : IntCast.intCast = IntCast.intCast
⊢ mk sub_eq_add_neg✝¹ zsmul✝¹ zsmul_zero'✝¹ zsmul_succ'✝¹ zsmul_neg'✝¹ neg_add_cancel✝¹ intCast_ofNat✝¹
      intCast_negSucc✝¹ =
    mk sub_eq_add_neg✝ zsmul✝ zsmul_zero'✝ zsmul_succ'✝ zsmul_neg'✝ neg_add_cancel✝ intCast_ofNat✝ intCast_negSucc✝

Tactic:
congr

Result:
no goals

Proof state:
case mk.mk
R : Type u
inst₂ : AddGroupWithOne R
toAddMonoidWithOne✝ : AddMonoidWithOne R
toNeg✝ : Neg R
toSub✝ : Sub R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul✝ : ℤ → R → R
zsmul_zero'✝ : ∀ (a : R), zsmul✝ 0 a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), zsmul✝ (↑n.succ) a = zsmul✝ (↑n) a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), zsmul✝ (Int.negSucc n) a = -zsmul✝ (↑n.succ) a
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
intCast✝ : ℤ → R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝¹ : toAddMonoidWithOne = toAddMonoidWithOne
this✝ : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast
toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid
toNeg_eq✝ : toNeg = toNeg
toSub_eq✝ : toSub = toSub
zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul
this : IntCast.intCast = IntCast.intCast
⊢ mk sub_eq_add_neg✝ zsmul✝ zsmul_zero'✝ zsmul_succ'✝ zsmul_neg'✝ neg_add_cancel✝ intCast_ofNat✝ intCast_negSucc✝ =
    inst₂

Tactic:
rcases inst₂ with @⟨⟨⟩⟩

Result:
case mk.mk.mk.mk
R : Type u
toAddMonoidWithOne✝¹ : AddMonoidWithOne R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul✝¹ : ℤ → R → R
zsmul_zero'✝¹ : ∀ (a : R), zsmul✝¹ 0 a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), zsmul✝¹ (↑n.succ) a = zsmul✝¹ (↑n) a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), zsmul✝¹ (Int.negSucc n) a = -zsmul✝¹ (↑n.succ) a
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
intCast✝¹ : ℤ → R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toAddMonoidWithOne✝ : AddMonoidWithOne R
toNeg✝ : Neg R
toSub✝ : Sub R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul✝ : ℤ → R → R
zsmul_zero'✝ : ∀ (a : R), zsmul✝ 0 a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), zsmul✝ (↑n.succ) a = zsmul✝ (↑n) a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), zsmul✝ (Int.negSucc n) a = -zsmul✝ (↑n.succ) a
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
intCast✝ : ℤ → R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝¹ : toAddMonoidWithOne = toAddMonoidWithOne
this✝ : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast
toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid
toNeg_eq✝ : toNeg = toNeg
toSub_eq✝ : toSub = toSub
zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul
this : IntCast.intCast = IntCast.intCast
⊢ mk sub_eq_add_neg✝¹ zsmul✝¹ zsmul_zero'✝¹ zsmul_succ'✝¹ zsmul_neg'✝¹ neg_add_cancel✝¹ intCast_ofNat✝¹
      intCast_negSucc✝¹ =
    mk sub_eq_add_neg✝ zsmul✝ zsmul_zero'✝ zsmul_succ'✝ zsmul_neg'✝ neg_add_cancel✝ intCast_ofNat✝ intCast_negSucc✝

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

Tactic:
have : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne :=
  AddMonoidWithOne.ext h_add h_one

Result:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : toAddMonoidWithOne = toAddMonoidWithOne
⊢ inst₁ = inst₂

Proof state:
case h.ofNat
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : toAddMonoidWithOne = toAddMonoidWithOne
this : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast
toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid
toNeg_eq✝ : toNeg = toNeg
toSub_eq✝ : toSub = toSub
zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul
n : ℕ
⊢ IntCast.intCast (Int.ofNat n) = IntCast.intCast (Int.ofNat n)

Tactic:
rewrite [Int.ofNat_eq_coe, inst₁.intCast_ofNat, inst₂.intCast_ofNat]

Result:
case h.ofNat
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : toAddMonoidWithOne = toAddMonoidWithOne
this : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast
toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid
toNeg_eq✝ : toNeg = toNeg
toSub_eq✝ : toSub = toSub
zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul
n : ℕ
⊢ ↑n = ↑n

Proof state:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : toAddMonoidWithOne = toAddMonoidWithOne
this : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast
toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid
toNeg_eq✝ : toNeg = toNeg
toSub_eq✝ : toSub = toSub
zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul
⊢ IntCast.intCast = IntCast.intCast

Tactic:
funext n

Result:
case h
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : toAddMonoidWithOne = toAddMonoidWithOne
this : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast
toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid
toNeg_eq✝ : toNeg = toNeg
toSub_eq✝ : toSub = toSub
zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul
n : ℤ
⊢ IntCast.intCast n = IntCast.intCast n

Proof state:
case h.ofNat
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : toAddMonoidWithOne = toAddMonoidWithOne
this : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast
toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid
toNeg_eq✝ : toNeg = toNeg
toSub_eq✝ : toSub = toSub
zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul
n : ℕ
⊢ ↑n = ↑n

Tactic:
congr

Result:
no goals

Proof state:
case h_mul
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : toAddMonoidWithOne = toAddMonoidWithOne
this : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast
⊢ Add.add = Add.add

Tactic:
exact h_add

Result:
no goals