awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonUnitalNonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
rcases :
  ∀ [toAddCommGroup : AddCommGroup R] (mul : R → R → R) (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) (zero_mul : ∀ (a : R), 0 * a = 0)
    (mul_zero : ∀ (a : R), a * 0 = 0) (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd)
    (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul),
    { toAddCommGroup := toAddCommGroup, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
        zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocRing R } =
      inst₂
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨_, ⟨⟩⟩
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₂ : NonUnitalNonAssocRing R
toAddCommGroup : AddCommGroup R
mul : R → R → R
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
zero_mul : ∀ (a : R), 0 * a = 0
mul_zero : ∀ (a : R), a * 0 = 0
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
rcases :
  ∀ [toAddCommGroup_1 : AddCommGroup R] (mul_1 : R → R → R)
    (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) (zero_mul_1 : ∀ (a : R), 0 * a = 0)
    (mul_zero_1 : ∀ (a : R), a * 0 = 0) (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd)
    (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul),
    { toAddCommGroup := toAddCommGroup, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
        zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocRing R } =
      { toAddCommGroup := toAddCommGroup_1, mul := mul_1, left_distrib := left_distrib_1,
        right_distrib := right_distrib_1, zero_mul := zero_mul_1, mul_zero := mul_zero_1 }
⊢ { toAddCommGroup := toAddCommGroup, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
      zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocRing R } =
    inst₂

Tactic:
rcases inst₂ with @⟨_, ⟨⟩⟩
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddCommGroup : AddCommGroup R
mul : R → R → R
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
zero_mul : ∀ (a : R), 0 * a = 0
mul_zero : ∀ (a : R), a * 0 = 0
toAddCommGroup_1 : AddCommGroup R
mul_1 : R → R → R
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
zero_mul_1 : ∀ (a : R), 0 * a = 0
mul_zero_1 : ∀ (a : R), a * 0 = 0
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
e_toAddCommGroup : toAddCommGroup = toAddCommGroup_1
⊢ { toAddCommGroup := toAddCommGroup, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
      zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocRing R } =
    { toAddCommGroup := toAddCommGroup_1, mul := mul_1, left_distrib := left_distrib_1,
      right_distrib := right_distrib_1, zero_mul := zero_mul_1, mul_zero := mul_zero_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddCommGroup : AddCommGroup R
mul : R → R → R
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
zero_mul : ∀ (a : R), 0 * a = 0
mul_zero : ∀ (a : R), a * 0 = 0
toAddCommGroup_1 : AddCommGroup R
mul_1 : R → R → R
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
zero_mul_1 : ∀ (a : R), 0 * a = 0
mul_zero_1 : ∀ (a : R), a * 0 = 0
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
e_toAddCommGroup : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
⊢ toAddCommGroup = toAddCommGroup_1

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddCommGroup : AddCommGroup R
mul : R → R → R
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
zero_mul : ∀ (a : R), 0 * a = 0
mul_zero : ∀ (a : R), a * 0 = 0
toAddCommGroup_1 : AddCommGroup R
mul_1 : R → R → R
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
zero_mul_1 : ∀ (a : R), 0 * a = 0
mul_zero_1 : ∀ (a : R), a * 0 = 0
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
a₁ : NonUnitalNonAssocRing R
_ :
  ∀ ⦃a₂ : NonUnitalNonAssocRing R⦄,
    Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring → a₁ = a₂
⊢ ∀ ⦃a₂ : NonUnitalNonAssocRing R⦄,
    Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalNonAssocRing R
h : Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
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₂ : NonUnitalNonAssocRing R
h : Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
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₂ : NonUnitalNonAssocRing R
h : Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
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₂ : NonUnitalNonAssocRing R
h : Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
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₂ : NonUnitalNonAssocRing R
h : Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
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₂ : NonUnitalRing 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} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonUnitalRing 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₂ : NonUnitalRing 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₂ : NonUnitalRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing

Tactic:
have : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by
    ext : 1 <;> assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonUnitalRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
this : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
mk :
  ∀ [toNonUnitalNonAssocRing : NonUnitalNonAssocRing R] (mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c))
    (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd) (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul)
    (this :
      Eq.{u + 1} (α := NonUnitalNonAssocRing R) NonUnitalRing.toNonUnitalNonAssocRing
        NonUnitalRing.toNonUnitalNonAssocRing),
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, mul_assoc := mul_assoc : NonUnitalRing R } = inst₂
⊢ inst₁ = inst₂

Tactic:
cases inst₁
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₂ : NonUnitalRing R
toNonUnitalNonAssocRing : NonUnitalNonAssocRing R
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
this :
  Eq.{u + 1} (α := NonUnitalNonAssocRing R) NonUnitalRing.toNonUnitalNonAssocRing NonUnitalRing.toNonUnitalNonAssocRing
mk :
  ∀ [toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing R] (mul_assoc_1 : ∀ (a b c : R), a * b * c = a * (b * c))
    (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd) (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul)
    (this :
      Eq.{u + 1} (α := NonUnitalNonAssocRing R) NonUnitalRing.toNonUnitalNonAssocRing
        NonUnitalRing.toNonUnitalNonAssocRing),
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, mul_assoc := mul_assoc : NonUnitalRing R } =
      { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing_1, mul_assoc := mul_assoc_1 }
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, mul_assoc := mul_assoc : NonUnitalRing R } = inst₂

Tactic:
cases inst₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocRing : NonUnitalNonAssocRing R
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing R
mul_assoc_1 : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
this :
  Eq.{u + 1} (α := NonUnitalNonAssocRing R) NonUnitalRing.toNonUnitalNonAssocRing NonUnitalRing.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, mul_assoc := mul_assoc : NonUnitalRing R } =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing_1, mul_assoc := mul_assoc_1 }

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

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalRing 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₂ : NonUnitalRing 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₂ : NonUnitalRing 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₂ : NonUnitalRing 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₂ : NonUnitalRing 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₁ : NonUnitalRing R
_ :
  ∀ ⦃a₂ : NonUnitalRing R⦄,
    Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing → a₁ = a₂
⊢ ∀ ⦃a₂ : NonUnitalRing R⦄,
    Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalRing R
_ : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing → a₁ = a₂
⊢ Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing → a₁ = a₂

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

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalRing R
h : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
x x_1 : R
⊢ x + x_1 = x + x_1

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonUnitalRing R
h : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
x x_1 : R
⊢ x * x_1 = x * x_1

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
⊢ Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne

Tactic:
have : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne :=
    AddMonoidWithOne.ext h_add h_one
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
⊢ Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast

Tactic:
have : inst₁.toNatCast = inst₂.toNatCast := congrArg (·.toNatCast) this
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
h_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
⊢ Eq.{u + 1} (α := AddGroup R) toAddGroup toAddGroup

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
exact h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
⊢ Eq.{u + 1} (α := AddGroup R) toAddGroup toAddGroup

Tactic:
have h_group : inst₁.toAddGroup = inst₂.toAddGroup := by ext : 1; exact h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
h_group : Eq.{u + 1} (α := AddGroup R) toAddGroup toAddGroup
⊢ Eq.{u + 1} (α := SubNegMonoid R)
    { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
    { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }

Tactic:
injection h_group with h_group
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
h_group :
  Eq.{u + 1} (α := SubNegMonoid R)
    { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
    { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
⊢ Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid

Tactic:
injection h_group
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
h_group :
  Eq.{u + 1} (α := SubNegMonoid R)
    { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
    { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
⊢ Eq.{u + 1} (α := Neg R) toNeg toNeg

Tactic:
injection h_group
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
h_group :
  Eq.{u + 1} (α := SubNegMonoid R)
    { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
    { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
⊢ Eq.{u + 1} (α := Sub R) toSub toSub

Tactic:
injection h_group
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
h_group :
  Eq.{u + 1} (α := SubNegMonoid R)
    { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
    { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, sub_eq_add_neg := ⋯,
      zsmul := AddGroupWithOne.zsmul, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
⊢ Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul

Tactic:
injection h_group
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
h : ∀ (n : ℤ), Eq.{u + 1} (α := R) (IntCast.intCast n) (IntCast.intCast n)
⊢ Eq.{u + 1} (α := ℤ → R) IntCast.intCast IntCast.intCast

Tactic:
funext n
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
n : ℕ
h : Eq.{u + 1} (α := R) (↑n : R) (↑n : R)
⊢ Eq.{u + 1} (α := R) (IntCast.intCast (Int.ofNat n)) (IntCast.intCast (Int.ofNat n))

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

Premises used: Int.ofNat_eq_natCast, AddGroupWithOne.intCast_ofNat
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑n : R) (↑n : R)

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
n : ℕ
h : Eq.{u + 1} (α := R) (-(↑(n + 1) : R)) (-(↑(n + 1) : R))
⊢ Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (IntCast.intCast (Int.negSucc n))

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

Premises used: AddGroupWithOne.intCast_negSucc