awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
⊢ Eq.{u + 1} (α := R) 0 0

Tactic:
exact congrArg (@Zero.zero R) h_zero'

Premises used: congrArg, Zero.zero
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
n : ℕ
h : Eq.{u + 1} (α := R) ↑n ↑n
h₁ : HAdd.hAdd (α := R) (↑n) 1 = HAdd.hAdd (α := R) (↑n) 1
⊢ Eq.{u + 1} (α := R) ↑(n + 1) ↑(n + 1)

Tactic:
rw [inst₁.natCast_succ, inst₂.natCast_succ, h_add]

Premises used: AddMonoidWithOne.natCast_succ
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
n : ℕ
h : Eq.{u + 1} (α := R) ↑n ↑n
⊢ HAdd.hAdd (α := R) (↑n) 1 = HAdd.hAdd (α := R) (↑n) 1

Tactic:
congrArg₂ _ h h_one

Premises used: congrArg₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
n : ℕ
h : Eq.{u + 1} (α := R) ↑n ↑n
⊢ HAdd.hAdd (α := R) (↑n) 1 = HAdd.hAdd (α := R) (↑n) 1

Tactic:
exact congrArg₂ _ h h_one

Premises used: congrArg₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
n : ℕ
h : Eq.{u + 1} (α := R) ↑0 ↑0
h₁ : ∀ (n : ℕ) (h : Eq.{u + 1} (α := R) ↑n ↑n), Eq.{u + 1} (α := R) ↑(n + 1) ↑(n + 1)
⊢ Eq.{u + 1} (α := R) ↑n ↑n

Tactic:
induction n with
    | zero => rewrite [inst₁.natCast_zero, inst₂.natCast_zero]
              exact congrArg (@Zero.zero R) h_zero'
    | succ n h => rw [inst₁.natCast_succ, inst₂.natCast_succ, h_add]
                  exact congrArg₂ _ h h_one

Premises used: AddMonoidWithOne.natCast_zero, congrArg, Zero.zero, AddMonoidWithOne.natCast_succ
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
⊢ Eq.{u + 1} (α := ℕ → R) NatCast.natCast NatCast.natCast

Tactic:
have h_natCast : inst₁.toNatCast.natCast = inst₂.toNatCast.natCast := by
    funext n; induction n with
    | zero => rewrite [inst₁.natCast_zero, inst₂.natCast_zero]
              exact congrArg (@Zero.zero R) h_zero'
    | succ n h => rw [inst₁.natCast_succ, inst₂.natCast_succ, h_add]
                  exact congrArg₂ _ h h_one
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) toOne toOne
h_natCast : Eq.{u + 1} (α := ℕ → R) NatCast.natCast NatCast.natCast
rcases :
  ∀ [toAddMonoid : AddMonoid R] [toOne : One R] (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_one : Eq.{u + 1} (α := R) One.one One.one)
    (h_monoid : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid)
    (h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero)
    (h_one' : Eq.{u + 1} (α := One R) AddMonoidWithOne.toOne AddMonoidWithOne.toOne)
    (h_natCast : Eq.{u + 1} (α := ℕ → R) NatCast.natCast NatCast.natCast),
    { natCast := natCast, toAddMonoid := toAddMonoid, toOne := toOne, natCast_zero := natCast_zero,
        natCast_succ := natCast_succ : AddMonoidWithOne R } =
      inst₂
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨⟨⟩⟩
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₂ : AddMonoidWithOne R
toAddMonoid : AddMonoid R
toOne : One R
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_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) AddMonoidWithOne.toOne AddMonoidWithOne.toOne
h_natCast : Eq.{u + 1} (α := ℕ → R) NatCast.natCast NatCast.natCast
rcases :
  ∀ [toAddMonoid_1 : AddMonoid R] [toOne_1 : One R] (natCast_1 : ℕ → 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_one : Eq.{u + 1} (α := R) One.one One.one)
    (h_monoid : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid)
    (h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero)
    (h_one' : Eq.{u + 1} (α := One R) AddMonoidWithOne.toOne AddMonoidWithOne.toOne)
    (h_natCast : Eq.{u + 1} (α := ℕ → R) NatCast.natCast NatCast.natCast),
    { natCast := natCast, toAddMonoid := toAddMonoid, toOne := toOne, natCast_zero := natCast_zero,
        natCast_succ := natCast_succ : AddMonoidWithOne R } =
      { natCast := natCast_1, toAddMonoid := toAddMonoid_1, toOne := toOne_1, natCast_zero := natCast_zero_1,
        natCast_succ := natCast_succ_1 }
⊢ { natCast := natCast, toAddMonoid := toAddMonoid, toOne := toOne, natCast_zero := natCast_zero,
      natCast_succ := natCast_succ : AddMonoidWithOne R } =
    inst₂

Tactic:
rcases inst₂ with @⟨⟨⟩⟩
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddMonoid : AddMonoid R
toOne : One R
natCast : ℕ → R
natCast_zero : Eq.{u + 1} (α := R) (↑0) 0
natCast_succ : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1
toAddMonoid_1 : AddMonoid R
toOne_1 : One R
natCast_1 : ℕ → 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_one : Eq.{u + 1} (α := R) One.one One.one
h_monoid : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
h_one' : Eq.{u + 1} (α := One R) AddMonoidWithOne.toOne AddMonoidWithOne.toOne
h_natCast : Eq.{u + 1} (α := ℕ → R) NatCast.natCast NatCast.natCast
⊢ { natCast := natCast, toAddMonoid := toAddMonoid, toOne := toOne, natCast_zero := natCast_zero,
      natCast_succ := natCast_succ : AddMonoidWithOne R } =
    { natCast := natCast_1, toAddMonoid := toAddMonoid_1, toOne := toOne_1, natCast_zero := natCast_zero_1,
      natCast_succ := natCast_succ_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddMonoidWithOne : AddMonoidWithOne R
add_comm : ∀ (a b : R), a + b = b + a
toAddMonoidWithOne_1 : AddMonoidWithOne R
add_comm_1 : ∀ (a b : R), a + b = b + a
h : Eq.{u + 1} (α := AddMonoidWithOne R) AddCommMonoidWithOne.toAddMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne
⊢ { toAddMonoidWithOne := toAddMonoidWithOne, add_comm := add_comm : AddCommMonoidWithOne R } =
    { toAddMonoidWithOne := toAddMonoidWithOne_1, add_comm := add_comm_1 }

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

Tactic:
AddCommMonoidWithOne.toAddMonoidWithOne_injective <|
    AddMonoidWithOne.ext h_add h_one

Premises used: AddCommMonoidWithOne.toAddMonoidWithOne_injective, AddMonoidWithOne.ext
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring

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

Tactic:
have h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring := by
    ext : 1 <;> assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
⊢ Eq.{u + 1} (α := R) Zero.zero Zero.zero

Tactic:
have h_zero : (inst₁.toMulZeroClass).toZero.zero = (inst₂.toMulZeroClass).toZero.zero :=
    congrArg (fun inst => (inst.toMulZeroClass).toZero.zero) h
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h₁ : Eq.{u + 1} (α := MulOneClass R) MulZeroOneClass.toMulOneClass MulZeroOneClass.toMulOneClass
⊢ Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne

Tactic:
congr 2
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h₁ : Eq.{u + 1} (α := R → R → R) Mul.mul Mul.mul
⊢ Eq.{u + 1} (α := MulOneClass R) MulZeroOneClass.toMulOneClass MulZeroOneClass.toMulOneClass

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
⊢ Eq.{u + 1} (α := R → R → R) Mul.mul Mul.mul

Tactic:
h_mul
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
⊢ Eq.{u + 1} (α := R → R → R) Mul.mul Mul.mul

Tactic:
exact h_mul
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
⊢ Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne

Tactic:
have h_one' : (inst₁.toMulZeroOneClass).toMulOneClass.toOne
                = (inst₂.toMulZeroOneClass).toMulOneClass.toOne := by
    congr 2; ext : 1; exact h_mul
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
⊢ Eq.{u + 1} (α := R) One.one One.one

Tactic:
have h_one : (inst₁.toMulZeroOneClass).toMulOneClass.toOne.one
               = (inst₂.toMulZeroOneClass).toMulOneClass.toOne.one :=
    congrArg (@One.one R) h_one'
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
h_one : Eq.{u + 1} (α := R) One.one One.one
h_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one₁ : Eq.{u + 1} (α := R) One.one One.one
⊢ Eq.{u + 1} (α := AddCommMonoidWithOne R) toAddCommMonoidWithOne toAddCommMonoidWithOne

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
h_one : Eq.{u + 1} (α := R) One.one One.one
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
h_one : Eq.{u + 1} (α := R) One.one One.one
⊢ Eq.{u + 1} (α := R) One.one One.one

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
h_one : Eq.{u + 1} (α := R) One.one One.one
⊢ Eq.{u + 1} (α := AddCommMonoidWithOne R) toAddCommMonoidWithOne toAddCommMonoidWithOne

Tactic:
have : inst₁.toAddCommMonoidWithOne = inst₂.toAddCommMonoidWithOne := by
    ext : 1 <;> assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
h_one : Eq.{u + 1} (α := R) One.one One.one
this : Eq.{u + 1} (α := AddCommMonoidWithOne R) toAddCommMonoidWithOne toAddCommMonoidWithOne
⊢ Eq.{u + 1} (α := NatCast R) toNatCast toNatCast

Tactic:
have : inst₁.toNatCast = inst₂.toNatCast :=
    congrArg (·.toNatCast) this
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocSemiring 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} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddCommMonoidWithOne R) toAddCommMonoidWithOne toAddCommMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) toNatCast toNatCast
mk :
  ∀ [toNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring R] [toOne : One R] (one_mul : ∀ (a : R), 1 * a = a)
    (mul_one : ∀ (a : R), a * 1 = a) [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} (α := NonUnitalNonAssocSemiring R) NonAssocSemiring.toNonUnitalNonAssocSemiring
        NonAssocSemiring.toNonUnitalNonAssocSemiring)
    (h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero) (h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne)
    (h_one : Eq.{u + 1} (α := R) One.one One.one)
    (this : Eq.{u + 1} (α := AddCommMonoidWithOne R) toAddCommMonoidWithOne toAddCommMonoidWithOne)
    (this : Eq.{u + 1} (α := NatCast R) NonAssocSemiring.toNatCast NonAssocSemiring.toNatCast),
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring, toOne := toOne, one_mul := one_mul,
        mul_one := mul_one, toNatCast := toNatCast, natCast_zero := natCast_zero, natCast_succ := natCast_succ :
        NonAssocSemiring R } =
      inst₂
⊢ inst₁ = inst₂

Tactic:
cases inst₁
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₂ : NonAssocSemiring R
toNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring R
toOne : One R
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
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} (α := NonUnitalNonAssocSemiring R) NonAssocSemiring.toNonUnitalNonAssocSemiring
    NonAssocSemiring.toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddCommMonoidWithOne R) toAddCommMonoidWithOne toAddCommMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) NonAssocSemiring.toNatCast NonAssocSemiring.toNatCast
mk :
  ∀ [toNonUnitalNonAssocSemiring_1 : NonUnitalNonAssocSemiring R] [toOne_1 : One R] (one_mul_1 : ∀ (a : R), 1 * a = a)
    (mul_one_1 : ∀ (a : R), a * 1 = a) [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} (α := NonUnitalNonAssocSemiring R) NonAssocSemiring.toNonUnitalNonAssocSemiring
        NonAssocSemiring.toNonUnitalNonAssocSemiring)
    (h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero) (h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne)
    (h_one : Eq.{u + 1} (α := R) One.one One.one)
    (this : Eq.{u + 1} (α := AddCommMonoidWithOne R) toAddCommMonoidWithOne toAddCommMonoidWithOne)
    (this : Eq.{u + 1} (α := NatCast R) NonAssocSemiring.toNatCast NonAssocSemiring.toNatCast),
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring, toOne := toOne, one_mul := one_mul,
        mul_one := mul_one, toNatCast := toNatCast, natCast_zero := natCast_zero, natCast_succ := natCast_succ :
        NonAssocSemiring R } =
      { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring_1, toOne := toOne_1, one_mul := one_mul_1,
        mul_one := mul_one_1, toNatCast := toNatCast_1, natCast_zero := natCast_zero_1, natCast_succ := natCast_succ_1 }
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring, toOne := toOne, one_mul := one_mul, mul_one := mul_one,
      toNatCast := toNatCast, natCast_zero := natCast_zero, natCast_succ := natCast_succ : NonAssocSemiring R } =
    inst₂

Tactic:
cases inst₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring R
toOne : One R
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
toNatCast : NatCast R
natCast_zero : Eq.{u + 1} (α := R) (↑0) 0
natCast_succ : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1
toNonUnitalNonAssocSemiring_1 : NonUnitalNonAssocSemiring R
toOne_1 : One R
one_mul_1 : ∀ (a : R), 1 * a = a
mul_one_1 : ∀ (a : R), a * 1 = a
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} (α := NonUnitalNonAssocSemiring R) NonAssocSemiring.toNonUnitalNonAssocSemiring
    NonAssocSemiring.toNonUnitalNonAssocSemiring
h_zero : Eq.{u + 1} (α := R) Zero.zero Zero.zero
h_one' : Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddCommMonoidWithOne R) toAddCommMonoidWithOne toAddCommMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) NonAssocSemiring.toNatCast NonAssocSemiring.toNatCast
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring, toOne := toOne, one_mul := one_mul, mul_one := mul_one,
      toNatCast := toNatCast, natCast_zero := natCast_zero, natCast_succ := natCast_succ : NonAssocSemiring R } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring_1, toOne := toOne_1, one_mul := one_mul_1,
      mul_one := mul_one_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
a₁ : NonAssocSemiring R
_ :
  ∀ ⦃a₂ : NonAssocSemiring R⦄,
    Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring → a₁ = a₂
⊢ ∀ ⦃a₂ : NonAssocSemiring R⦄,
    Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring → a₁ = a₂

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

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

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

Tactic:
congr