awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Semiring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₀ : Eq.{u + 1} (α := AddCommMonoid R) toAddCommMonoid toAddCommMonoid
h₁ : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := Monoid R) MonoidWithZero.toMonoid MonoidWithZero.toMonoid
mk :
  ∀ [toAddCommMonoid : AddCommMonoid R] [toMonoid : Monoid R] (zero_mul : ∀ (a : R), 0 * a = 0)
    (mul_zero : ∀ (a : R), a * 0 = 0) (left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c)
    (right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c) [toNatCast : NatCast R]
    (natCast_zero : Eq.{u + 1} (α := R) (↑0) 0) (natCast_succ : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1)
    (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd) (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul)
    (h₀ : Eq.{u + 1} (α := AddCommMonoid R) Semiring.toAddCommMonoid Semiring.toAddCommMonoid)
    (h₁ : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring)
    (h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring)
    (h₃ : Eq.{u + 1} (α := Monoid R) MonoidWithZero.toMonoid MonoidWithZero.toMonoid),
    { toAddCommMonoid := toAddCommMonoid, toMonoid := toMonoid, zero_mul := zero_mul, mul_zero := mul_zero,
        left_distrib := left_distrib, right_distrib := right_distrib, toNatCast := toNatCast,
        natCast_zero := natCast_zero, natCast_succ := natCast_succ : Semiring R } =
      inst₂
⊢ inst₁ = inst₂

Tactic:
cases inst₁
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₂ : Semiring R
toAddCommMonoid : AddCommMonoid R
toMonoid : Monoid R
zero_mul : ∀ (a : R), 0 * a = 0
mul_zero : ∀ (a : R), a * 0 = 0
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
toNatCast : NatCast R
natCast_zero : Eq.{u + 1} (α := R) (↑0) 0
natCast_succ : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₀ : Eq.{u + 1} (α := AddCommMonoid R) Semiring.toAddCommMonoid Semiring.toAddCommMonoid
h₁ : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := Monoid R) MonoidWithZero.toMonoid MonoidWithZero.toMonoid
mk :
  ∀ [toAddCommMonoid_1 : AddCommMonoid R] [toMonoid_1 : Monoid R] (zero_mul_1 : ∀ (a : R), 0 * a = 0)
    (mul_zero_1 : ∀ (a : R), a * 0 = 0) (left_distrib_1 : ∀ (a b c : R), a * (b + c) = a * b + a * c)
    (right_distrib_1 : ∀ (a b c : R), (a + b) * c = a * c + b * c) [toNatCast_1 : NatCast R]
    (natCast_zero_1 : Eq.{u + 1} (α := R) (↑0) 0) (natCast_succ_1 : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1)
    (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd) (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul)
    (h₀ : Eq.{u + 1} (α := AddCommMonoid R) Semiring.toAddCommMonoid Semiring.toAddCommMonoid)
    (h₁ : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring)
    (h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring)
    (h₃ : Eq.{u + 1} (α := Monoid R) MonoidWithZero.toMonoid MonoidWithZero.toMonoid),
    { toAddCommMonoid := toAddCommMonoid, toMonoid := toMonoid, zero_mul := zero_mul, mul_zero := mul_zero,
        left_distrib := left_distrib, right_distrib := right_distrib, toNatCast := toNatCast,
        natCast_zero := natCast_zero, natCast_succ := natCast_succ : Semiring R } =
      { toAddCommMonoid := toAddCommMonoid_1, toMonoid := toMonoid_1, zero_mul := zero_mul_1, mul_zero := mul_zero_1,
        left_distrib := left_distrib_1, right_distrib := right_distrib_1, toNatCast := toNatCast_1,
        natCast_zero := natCast_zero_1, natCast_succ := natCast_succ_1 }
⊢ { toAddCommMonoid := toAddCommMonoid, toMonoid := toMonoid, zero_mul := zero_mul, mul_zero := mul_zero,
      left_distrib := left_distrib, right_distrib := right_distrib, toNatCast := toNatCast,
      natCast_zero := natCast_zero, natCast_succ := natCast_succ : Semiring R } =
    inst₂

Tactic:
cases inst₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddCommMonoid : AddCommMonoid R
toMonoid : Monoid R
zero_mul : ∀ (a : R), 0 * a = 0
mul_zero : ∀ (a : R), a * 0 = 0
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
toNatCast : NatCast R
natCast_zero : Eq.{u + 1} (α := R) (↑0) 0
natCast_succ : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1
toAddCommMonoid_1 : AddCommMonoid R
toMonoid_1 : Monoid R
zero_mul_1 : ∀ (a : R), 0 * a = 0
mul_zero_1 : ∀ (a : R), a * 0 = 0
left_distrib_1 : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib_1 : ∀ (a b c : R), (a + b) * c = a * c + b * c
toNatCast_1 : NatCast R
natCast_zero_1 : Eq.{u + 1} (α := R) (↑0) 0
natCast_succ_1 : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₀ : Eq.{u + 1} (α := AddCommMonoid R) Semiring.toAddCommMonoid Semiring.toAddCommMonoid
h₁ : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := Monoid R) MonoidWithZero.toMonoid MonoidWithZero.toMonoid
mk : toNatCast = toNatCast_1
⊢ { toAddCommMonoid := toAddCommMonoid, toMonoid := toMonoid, zero_mul := zero_mul, mul_zero := mul_zero,
      left_distrib := left_distrib, right_distrib := right_distrib, toNatCast := toNatCast,
      natCast_zero := natCast_zero, natCast_succ := natCast_succ : Semiring R } =
    { toAddCommMonoid := toAddCommMonoid_1, toMonoid := toMonoid_1, zero_mul := zero_mul_1, mul_zero := mul_zero_1,
      left_distrib := left_distrib_1, right_distrib := right_distrib_1, toNatCast := toNatCast_1,
      natCast_zero := natCast_zero_1, natCast_succ := natCast_succ_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddCommMonoid : AddCommMonoid R
toMonoid : Monoid R
zero_mul : ∀ (a : R), 0 * a = 0
mul_zero : ∀ (a : R), a * 0 = 0
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
toNatCast : NatCast R
natCast_zero : Eq.{u + 1} (α := R) (↑0) 0
natCast_succ : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1
toAddCommMonoid_1 : AddCommMonoid R
toMonoid_1 : Monoid R
zero_mul_1 : ∀ (a : R), 0 * a = 0
mul_zero_1 : ∀ (a : R), a * 0 = 0
left_distrib_1 : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib_1 : ∀ (a b c : R), (a + b) * c = a * c + b * c
toNatCast_1 : NatCast R
natCast_zero_1 : Eq.{u + 1} (α := R) (↑0) 0
natCast_succ_1 : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₀ : Eq.{u + 1} (α := AddCommMonoid R) Semiring.toAddCommMonoid Semiring.toAddCommMonoid
h₁ : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := Monoid R) MonoidWithZero.toMonoid MonoidWithZero.toMonoid
⊢ toNatCast = toNatCast_1

Tactic:
injection h₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ : Semiring R
_ : ∀ ⦃a₂ : Semiring R⦄, Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring → a₁ = a₂
⊢ ∀ ⦃a₂ : Semiring R⦄, Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
h_add : ∀ (x y : R), x + y = x + y
h_mul : ∀ (x y : R), x * y = x * y
⊢ a₁ = a₂

Tactic:
ext x y
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
x y : R
⊢ x + y = x + y

Tactic:
congrArg (·.toAdd.add x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
x y : R
⊢ x + y = x + y

Tactic:
exact congrArg (·.toAdd.add x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Tactic:
congrArg (·.toMul.mul x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Tactic:
exact congrArg (·.toMul.mul x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ : Semiring R
_ : ∀ ⦃a₂ : Semiring R⦄, Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring → a₁ = a₂
⊢ ∀ ⦃a₂ : Semiring R⦄, Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h_add : ∀ (x y : R), x + y = x + y
h_mul : ∀ (x y : R), x * y = x * y
⊢ a₁ = a₂

Tactic:
ext x y
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
x y : R
⊢ x + y = x + y

Tactic:
congrArg (·.toAdd.add x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
x y : R
⊢ x + y = x + y

Tactic:
exact congrArg (·.toAdd.add x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
congrArg (·.toMul.mul x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : Semiring R
h : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
x y : R
⊢ x * y = x * y

Tactic:
exact congrArg (·.toMul.mul x y) h

Premises used: congrArg
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul₁ : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := Semiring R) toSemiring toSemiring

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq (α := R → R → R) HMul.hMul HMul.hMul

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := Semiring R) toSemiring toSemiring

Tactic:
have h₁ : inst₁.toSemiring = inst₂.toSemiring := by
    ext : 1 <;> assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
h_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul₁ : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
⊢ Eq (α := R → R → R) HMul.hMul HMul.hMul

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
⊢ Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing

Tactic:
have h₂ : inst₁.toNonAssocRing = inst₂.toNonAssocRing := by
    ext : 1 <;> assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
⊢ Eq.{u + 1} (α := AddGroup R) AddCommGroup.toAddGroup AddCommGroup.toAddGroup

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
exact h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
⊢ Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid

Tactic:
have h₃ : (inst₁.toAddCommGroup).toAddGroup.toSubNegMonoid
            = (inst₂.toAddCommGroup).toAddGroup.toSubNegMonoid :=
    congrArg (@AddGroup.toSubNegMonoid R) <| by ext : 1; exact h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : Ring R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
mk :
  ∀ [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 : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R))
    (intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R)))
    (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd) (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul)
    (h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring)
    (h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing)
    (h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid),
    { toSemiring := toSemiring, toNeg := toNeg, toSub := toSub, sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul,
        zsmul_zero' := zsmul_zero', zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg',
        neg_add_cancel := neg_add_cancel, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
        intCast_negSucc := intCast_negSucc : Ring R } =
      inst₂
⊢ inst₁ = inst₂

Tactic:
cases inst₁
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
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 : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
mk :
  ∀ [toSemiring_1 : Semiring R] [toNeg_1 : Neg R] [toSub_1 : Sub R] (sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b)
    (zsmul_1 : ℤ → R → R) (zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0)
    (zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a)
    (zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a)
    (neg_add_cancel_1 : ∀ (a : R), -a + a = 0) [toIntCast_1 : IntCast R]
    (intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R))
    (intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R)))
    (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd) (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul)
    (h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring)
    (h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing)
    (h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid),
    { toSemiring := toSemiring, toNeg := toNeg, toSub := toSub, sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul,
        zsmul_zero' := zsmul_zero', zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg',
        neg_add_cancel := neg_add_cancel, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
        intCast_negSucc := intCast_negSucc : Ring R } =
      { toSemiring := toSemiring_1, toNeg := toNeg_1, toSub := toSub_1, sub_eq_add_neg := sub_eq_add_neg_1,
        zsmul := zsmul_1, zsmul_zero' := zsmul_zero'_1, zsmul_succ' := zsmul_succ'_1, zsmul_neg' := zsmul_neg'_1,
        neg_add_cancel := neg_add_cancel_1, toIntCast := toIntCast_1, intCast_ofNat := intCast_ofNat_1,
        intCast_negSucc := intCast_negSucc_1 }
⊢ { toSemiring := toSemiring, toNeg := toNeg, toSub := toSub, sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul,
      zsmul_zero' := zsmul_zero', zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg',
      neg_add_cancel := neg_add_cancel, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
      intCast_negSucc := intCast_negSucc : Ring R } =
    inst₂

Tactic:
cases inst₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
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 : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
mk : toNeg = toNeg_1
mk₁ : toSub = toSub_1
mk₂ : zsmul = zsmul_1
mk₃ : toIntCast = toIntCast_1
⊢ { toSemiring := toSemiring, toNeg := toNeg, toSub := toSub, sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul,
      zsmul_zero' := zsmul_zero', zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg',
      neg_add_cancel := neg_add_cancel, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
      intCast_negSucc := intCast_negSucc : Ring R } =
    { toSemiring := toSemiring_1, toNeg := toNeg_1, toSub := toSub_1, sub_eq_add_neg := sub_eq_add_neg_1,
      zsmul := zsmul_1, zsmul_zero' := zsmul_zero'_1, zsmul_succ' := zsmul_succ'_1, zsmul_neg' := zsmul_neg'_1,
      neg_add_cancel := neg_add_cancel_1, toIntCast := toIntCast_1, intCast_ofNat := intCast_ofNat_1,
      intCast_negSucc := intCast_negSucc_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
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 : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
⊢ toNeg = toNeg_1

Tactic:
injection h₃