-- 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:
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
h_group : SubNegMonoid.mk ⋯ AddGroupWithOne.zsmul ⋯ ⋯ ⋯ = SubNegMonoid.mk ⋯ AddGroupWithOne.zsmul ⋯ ⋯ ⋯
⊢ inst₁ = inst₂

Tactic:
injection h_group

Result:
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
⊢ inst₁ = inst₂

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
this : IntCast.intCast = IntCast.intCast
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨⟨⟩⟩

Result:
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₂

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
⊢ inst₁ = inst₂

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

Result:
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
this : IntCast.intCast = IntCast.intCast
⊢ inst₁ = inst₂

Proof state:
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

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

Result:
no goals

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
⊢ inst₁ = inst₂

Tactic:
have h_group : inst₁.toAddGroup = inst₂.toAddGroup := by ext : 1; exact h_add

Result:
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
h_group : toAddGroup = toAddGroup
⊢ inst₁ = inst₂

Proof state:
case h.negSucc
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.negSucc n) = IntCast.intCast (Int.negSucc n)

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

Result:
case h.negSucc
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 + 1) = -↑(n + 1)

Proof state:
case h.negSucc
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 + 1) = -↑(n + 1)

Tactic:
congr

Result:
no goals

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
⊢ toAddGroup = toAddGroup

Tactic:
ext : 1

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

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
h_group : toAddGroup = toAddGroup
⊢ inst₁ = inst₂

Tactic:
injection h_group with h_group

Result:
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
h_group : SubNegMonoid.mk ⋯ AddGroupWithOne.zsmul ⋯ ⋯ ⋯ = SubNegMonoid.mk ⋯ AddGroupWithOne.zsmul ⋯ ⋯ ⋯
⊢ inst₁ = inst₂