-- Mathlib/Algebra/Ring/Ext.lean
theorem ext ⦃inst₁ inst₂ : Ring R⦄
    (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) :
    inst₁ = inst₂

Proof state:
case mk.mk.e_zsmul
R : Type u
toSemiring✝¹ : Semiring 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
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring 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
toIntCast✝ : 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_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ : AddGroup.toSubNegMonoid = AddGroup.toSubNegMonoid
⊢ zsmul✝¹ = zsmul✝

Tactic:
injection h₃

Result:
no goals

Proof state:
case mk.mk
R : Type u
toSemiring✝¹ : Semiring 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
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring 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
toIntCast✝ : 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_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ : AddGroup.toSubNegMonoid = AddGroup.toSubNegMonoid
⊢ 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 <;> solve | injection h₂ | injection h₃

Result:
no goals

Proof state:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
⊢ AddCommGroup.toAddGroup = AddCommGroup.toAddGroup

Tactic:
ext : 1

Result:
case h_mul
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
⊢ Add.add = Add.add

Proof state:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
⊢ inst₁ = inst₂

Tactic:
have h₃ : (inst₁.toAddCommGroup).toAddGroup.toSubNegMonoid
          = (inst₂.toAddCommGroup).toAddGroup.toSubNegMonoid :=
  congrArg (@AddGroup.toSubNegMonoid R) <| by ext : 1; exact h_add

Result:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ : AddGroup.toSubNegMonoid = AddGroup.toSubNegMonoid
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ : AddGroup.toSubNegMonoid = AddGroup.toSubNegMonoid
⊢ inst₁ = inst₂

Tactic:
cases inst₁

Result:
case mk
R : Type u
inst₂ : Ring R
toSemiring✝ : Semiring 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
toIntCast✝ : 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_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ : AddGroup.toSubNegMonoid = AddGroup.toSubNegMonoid
⊢ mk sub_eq_add_neg✝ zsmul✝ zsmul_zero'✝ zsmul_succ'✝ zsmul_neg'✝ neg_add_cancel✝ intCast_ofNat✝ intCast_negSucc✝ =
    inst₂

Proof state:
case mk
R : Type u
inst₂ : Ring R
toSemiring✝ : Semiring 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
toIntCast✝ : 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_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ : AddGroup.toSubNegMonoid = AddGroup.toSubNegMonoid
⊢ mk sub_eq_add_neg✝ zsmul✝ zsmul_zero'✝ zsmul_succ'✝ zsmul_neg'✝ neg_add_cancel✝ intCast_ofNat✝ intCast_negSucc✝ =
    inst₂

Tactic:
cases inst₂

Result:
case mk.mk
R : Type u
toSemiring✝¹ : Semiring 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
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring 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
toIntCast✝ : 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_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ : AddGroup.toSubNegMonoid = AddGroup.toSubNegMonoid
⊢ 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✝