-- Mathlib/Algebra/Ring/Ext.lean
theorem AddCommGroupWithOne.ext ⦃inst₁ inst₂ : AddCommGroupWithOne 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
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
toIntCast✝¹ : IntCast R
toNatCast✝¹ : NatCast R
toOne✝¹ : One R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toAddCommGroup✝ : AddCommGroup R
toIntCast✝ : IntCast R
toNatCast✝ : NatCast R
toOne✝ : One R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
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 : toAddCommGroup = toAddCommGroup
toIntCast_eq✝ : toIntCast = toIntCast
toNeg_eq✝ : SubNegMonoid.toNeg = SubNegMonoid.toNeg
toSub_eq✝ : SubNegMonoid.toSub = SubNegMonoid.toSub
zsmul_eq✝ : SubNegMonoid.zsmul = SubNegMonoid.zsmul
toNatCast_eq✝ : toNatCast = toNatCast
toAddMonoid_eq✝ : SubNegMonoid.toAddMonoid = SubNegMonoid.toAddMonoid
toOne_eq✝ : toOne = toOne
⊢ mk natCast_zero✝¹ natCast_succ✝¹ intCast_ofNat✝¹ intCast_negSucc✝¹ =
    mk natCast_zero✝ natCast_succ✝ intCast_ofNat✝ intCast_negSucc✝

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : toAddCommGroup = toAddCommGroup
this : toAddGroupWithOne = toAddGroupWithOne
⊢ inst₁ = inst₂

Tactic:
injection this with _ h_addMonoidWithOne

Result:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : toAddCommGroup = toAddCommGroup
toIntCast_eq✝ : toIntCast = toIntCast
h_addMonoidWithOne : AddMonoidWithOne.mk ⋯ ⋯ = AddMonoidWithOne.mk ⋯ ⋯
toNeg_eq✝ : SubNegMonoid.toNeg = SubNegMonoid.toNeg
toSub_eq✝ : SubNegMonoid.toSub = SubNegMonoid.toSub
zsmul_eq✝ : SubNegMonoid.zsmul = SubNegMonoid.zsmul
⊢ inst₁ = inst₂

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

Tactic:
have : inst₁.toAddCommGroup = inst₂.toAddCommGroup :=
  AddCommGroup.ext h_add

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

Proof state:
case mk
R : Type u
inst₂ : AddCommGroupWithOne R
toAddCommGroup✝ : AddCommGroup R
toIntCast✝ : IntCast R
toNatCast✝ : NatCast R
toOne✝ : One R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
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 : toAddCommGroup = toAddCommGroup
toIntCast_eq✝ : toIntCast = toIntCast
toNeg_eq✝ : SubNegMonoid.toNeg = SubNegMonoid.toNeg
toSub_eq✝ : SubNegMonoid.toSub = SubNegMonoid.toSub
zsmul_eq✝ : SubNegMonoid.zsmul = SubNegMonoid.zsmul
toNatCast_eq✝ : toNatCast = toNatCast
toAddMonoid_eq✝ : SubNegMonoid.toAddMonoid = SubNegMonoid.toAddMonoid
toOne_eq✝ : toOne = toOne
⊢ mk natCast_zero✝ natCast_succ✝ intCast_ofNat✝ intCast_negSucc✝ = inst₂

Tactic:
cases inst₂

Result:
case mk.mk
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
toIntCast✝¹ : IntCast R
toNatCast✝¹ : NatCast R
toOne✝¹ : One R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toAddCommGroup✝ : AddCommGroup R
toIntCast✝ : IntCast R
toNatCast✝ : NatCast R
toOne✝ : One R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
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 : toAddCommGroup = toAddCommGroup
toIntCast_eq✝ : toIntCast = toIntCast
toNeg_eq✝ : SubNegMonoid.toNeg = SubNegMonoid.toNeg
toSub_eq✝ : SubNegMonoid.toSub = SubNegMonoid.toSub
zsmul_eq✝ : SubNegMonoid.zsmul = SubNegMonoid.zsmul
toNatCast_eq✝ : toNatCast = toNatCast
toAddMonoid_eq✝ : SubNegMonoid.toAddMonoid = SubNegMonoid.toAddMonoid
toOne_eq✝ : toOne = toOne
⊢ mk natCast_zero✝¹ natCast_succ✝¹ intCast_ofNat✝¹ intCast_negSucc✝¹ =
    mk natCast_zero✝ natCast_succ✝ intCast_ofNat✝ intCast_negSucc✝

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

Tactic:
have : inst₁.toAddGroupWithOne = inst₂.toAddGroupWithOne :=
  AddGroupWithOne.ext h_add h_one

Result:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : toAddCommGroup = toAddCommGroup
this : toAddGroupWithOne = toAddGroupWithOne
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : toAddCommGroup = toAddCommGroup
toIntCast_eq✝ : toIntCast = toIntCast
h_addMonoidWithOne : AddMonoidWithOne.mk ⋯ ⋯ = AddMonoidWithOne.mk ⋯ ⋯
toNeg_eq✝ : SubNegMonoid.toNeg = SubNegMonoid.toNeg
toSub_eq✝ : SubNegMonoid.toSub = SubNegMonoid.toSub
zsmul_eq✝ : SubNegMonoid.zsmul = SubNegMonoid.zsmul
⊢ inst₁ = inst₂

Tactic:
injection h_addMonoidWithOne

Result:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : toAddCommGroup = toAddCommGroup
toIntCast_eq✝ : toIntCast = toIntCast
toNeg_eq✝ : SubNegMonoid.toNeg = SubNegMonoid.toNeg
toSub_eq✝ : SubNegMonoid.toSub = SubNegMonoid.toSub
zsmul_eq✝ : SubNegMonoid.zsmul = SubNegMonoid.zsmul
toNatCast_eq✝ : toNatCast = toNatCast
toAddMonoid_eq✝ : SubNegMonoid.toAddMonoid = SubNegMonoid.toAddMonoid
toOne_eq✝ : toOne = toOne
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : toAddCommGroup = toAddCommGroup
toIntCast_eq✝ : toIntCast = toIntCast
toNeg_eq✝ : SubNegMonoid.toNeg = SubNegMonoid.toNeg
toSub_eq✝ : SubNegMonoid.toSub = SubNegMonoid.toSub
zsmul_eq✝ : SubNegMonoid.zsmul = SubNegMonoid.zsmul
toNatCast_eq✝ : toNatCast = toNatCast
toAddMonoid_eq✝ : SubNegMonoid.toAddMonoid = SubNegMonoid.toAddMonoid
toOne_eq✝ : toOne = toOne
⊢ inst₁ = inst₂

Tactic:
cases inst₁

Result:
case mk
R : Type u
inst₂ : AddCommGroupWithOne R
toAddCommGroup✝ : AddCommGroup R
toIntCast✝ : IntCast R
toNatCast✝ : NatCast R
toOne✝ : One R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
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 : toAddCommGroup = toAddCommGroup
toIntCast_eq✝ : toIntCast = toIntCast
toNeg_eq✝ : SubNegMonoid.toNeg = SubNegMonoid.toNeg
toSub_eq✝ : SubNegMonoid.toSub = SubNegMonoid.toSub
zsmul_eq✝ : SubNegMonoid.zsmul = SubNegMonoid.zsmul
toNatCast_eq✝ : toNatCast = toNatCast
toAddMonoid_eq✝ : SubNegMonoid.toAddMonoid = SubNegMonoid.toAddMonoid
toOne_eq✝ : toOne = toOne
⊢ mk natCast_zero✝ natCast_succ✝ intCast_ofNat✝ intCast_negSucc✝ = inst₂