awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing 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} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne
mk :
  ∀ [toNonUnitalNonAssocRing : NonUnitalNonAssocRing 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) [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} (α := NonUnitalNonAssocRing R) NonAssocRing.toNonUnitalNonAssocRing
        NonAssocRing.toNonUnitalNonAssocRing)
    (h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring)
    (h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne),
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, toOne := toOne, one_mul := one_mul, mul_one := mul_one,
        toNatCast := toNatCast, natCast_zero := natCast_zero, natCast_succ := natCast_succ, toIntCast := toIntCast,
        intCast_ofNat := intCast_ofNat, intCast_negSucc := intCast_negSucc : NonAssocRing R } =
      inst₂
⊢ inst₁ = inst₂

Tactic:
cases inst₁
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₂ : NonAssocRing R
toNonUnitalNonAssocRing : NonUnitalNonAssocRing 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
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} (α := NonUnitalNonAssocRing R) NonAssocRing.toNonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne
mk :
  ∀ [toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing 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) [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} (α := NonUnitalNonAssocRing R) NonAssocRing.toNonUnitalNonAssocRing
        NonAssocRing.toNonUnitalNonAssocRing)
    (h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring)
    (h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne),
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, toOne := toOne, one_mul := one_mul, mul_one := mul_one,
        toNatCast := toNatCast, natCast_zero := natCast_zero, natCast_succ := natCast_succ, toIntCast := toIntCast,
        intCast_ofNat := intCast_ofNat, intCast_negSucc := intCast_negSucc : NonAssocRing R } =
      { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing_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,
        toIntCast := toIntCast_1, intCast_ofNat := intCast_ofNat_1, intCast_negSucc := intCast_negSucc_1 }
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, toOne := toOne, one_mul := one_mul, mul_one := mul_one,
      toNatCast := toNatCast, natCast_zero := natCast_zero, natCast_succ := natCast_succ, toIntCast := toIntCast,
      intCast_ofNat := intCast_ofNat, intCast_negSucc := intCast_negSucc : NonAssocRing R } =
    inst₂

Tactic:
cases inst₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocRing : NonUnitalNonAssocRing 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
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))
toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing 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
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} (α := NonUnitalNonAssocRing R) NonAssocRing.toNonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne
mk : toOne = toOne_1
mk₁ : toNatCast = toNatCast_1
mk₂ : toIntCast = toIntCast_1
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, toOne := toOne, one_mul := one_mul, mul_one := mul_one,
      toNatCast := toNatCast, natCast_zero := natCast_zero, natCast_succ := natCast_succ, toIntCast := toIntCast,
      intCast_ofNat := intCast_ofNat, intCast_negSucc := intCast_negSucc : NonAssocRing R } =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing_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,
      toIntCast := toIntCast_1, intCast_ofNat := intCast_ofNat_1, intCast_negSucc := intCast_negSucc_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocRing : NonUnitalNonAssocRing 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
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))
toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing 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
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} (α := NonUnitalNonAssocRing R) NonAssocRing.toNonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne
⊢ toOne = toOne_1

Tactic:
injection h₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocRing : NonUnitalNonAssocRing 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
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))
toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing 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
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} (α := NonUnitalNonAssocRing R) NonAssocRing.toNonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne
⊢ toOne = toOne_1

Tactic:
solve | injection h₁ | injection h₂ | injection h₃
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocRing : NonUnitalNonAssocRing 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
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))
toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing 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
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} (α := NonUnitalNonAssocRing R) NonAssocRing.toNonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne
⊢ toNatCast = toNatCast_1

Tactic:
injection h₂
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocRing : NonUnitalNonAssocRing 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
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))
toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing 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
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} (α := NonUnitalNonAssocRing R) NonAssocRing.toNonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne
⊢ toNatCast = toNatCast_1

Tactic:
solve | injection h₁ | injection h₂ | injection h₃
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toNonUnitalNonAssocRing : NonUnitalNonAssocRing 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
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))
toNonUnitalNonAssocRing_1 : NonUnitalNonAssocRing 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
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} (α := NonUnitalNonAssocRing R) NonAssocRing.toNonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
h₃ : Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne
⊢ toIntCast = toIntCast_1

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

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

Tactic:
_
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
a₁ a₂ : NonAssocRing 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₂ : NonAssocRing 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₂ : NonAssocRing 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₂ : NonAssocRing 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₂ : Semiring 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
⊢ Eq.{u + 1} (α := AddCommMonoid R) toAddCommMonoid toAddCommMonoid

Tactic:
ext : 1
-- 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
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
assumption
-- 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
⊢ Eq.{u + 1} (α := AddCommMonoid R) toAddCommMonoid toAddCommMonoid

Tactic:
have h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid := by
    ext : 1 <;> assumption
-- 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_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul₁ : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring

Tactic:
ext : 1
-- 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
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
assumption
-- 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
⊢ Eq (α := R → R → R) HMul.hMul HMul.hMul

Tactic:
assumption
-- 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
⊢ Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring

Tactic:
have h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring := by
    ext : 1 <;> assumption
-- 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_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul₁ : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring

Tactic:
ext : 1
-- 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
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
assumption
-- 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
⊢ Eq (α := R → R → R) HMul.hMul HMul.hMul

Tactic:
assumption
-- 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
⊢ Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring

Tactic:
have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by
    ext : 1 <;> assumption
-- 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_mul₁ : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := Monoid R) MonoidWithZero.toMonoid MonoidWithZero.toMonoid

Tactic:
ext : 1
-- 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
⊢ Eq (α := R → R → R) HMul.hMul HMul.hMul

Tactic:
h_mul
-- 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
⊢ Eq (α := R → R → R) HMul.hMul HMul.hMul

Tactic:
exact h_mul
-- 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
⊢ Eq.{u + 1} (α := Monoid R) MonoidWithZero.toMonoid MonoidWithZero.toMonoid

Tactic:
have h₃ : (inst₁.toMonoidWithZero).toMonoid = (inst₂.toMonoidWithZero).toMonoid := by
    ext : 1; exact h_mul