awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have h_one' : 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
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have h_one : 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'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have this : Eq.{u + 1} (α := AddCommMonoidWithOne R) toAddCommMonoidWithOne toAddCommMonoidWithOne
Tactic: have : inst₁.toAddCommMonoidWithOne = inst₂.toAddCommMonoidWithOne := by
    ext : 1 <;> assumption
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have this₁ : Eq.{u + 1} (α := NatCast R) toNatCast toNatCast
Tactic: have : inst₁.toNatCast = inst₂.toNatCast :=
    congrArg (·.toNatCast) this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ inst₁ = inst₂
have 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₂
Tactic: cases inst₁
Cleared hypotheses: inst₁, h_add, h_mul, h, h_zero, h_one', h_one, this_1, this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ { 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₂
have 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 }
Tactic: cases inst₂
Cleared hypotheses: inst₂, h_add, h_mul, h, h_zero, h_one', h_one, this_1, this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : NonAssocSemiring R
h : Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
⊢ a₁ = a₂
have h_add : ∀ (x x_1 : R), x + x_1 = x + x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ a₁ = a₂
have h_mul : ∀ (x x_1 : R), x * x_1 = x * x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ inst₁ = inst₂
have 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₂
Tactic: rcases inst₁ with @⟨_, ⟨⟩⟩
Cleared hypotheses: inst₁, h_add, h_mul
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ { toAddCommGroup := toAddCommGroup, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
      zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocRing R } =
    inst₂
have 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 }
Tactic: rcases inst₂ with @⟨_, ⟨⟩⟩
Cleared hypotheses: inst₂, h_add, h_mul
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ { 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 }
have e_toAddCommGroup : toAddCommGroup = toAddCommGroup_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : NonUnitalNonAssocRing R
h : Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
⊢ a₁ = a₂
have h_add : ∀ (x y : R), x + y = x + y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ a₁ = a₂
have h_mul : ∀ (x y : R), x * y = x * y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have this : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
Tactic: have : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by
    ext : 1 <;> assumption
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ inst₁ = inst₂
have 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₂
Tactic: cases inst₁
Cleared hypotheses: inst₁, h_add, h_mul, this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, mul_assoc := mul_assoc : NonUnitalRing R } = inst₂
have 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 }
Tactic: cases inst₂
Cleared hypotheses: inst₂, h_add, h_mul, this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : NonUnitalRing R
h : Eq.{u + 1} (α := NonUnitalSemiring R) toNonUnitalSemiring toNonUnitalSemiring
⊢ a₁ = a₂
have h_add : ∀ (x y : R), x + y = x + y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ a₁ = a₂
have h_mul : ∀ (x y : R), x * y = x * y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : NonUnitalRing R
h : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
⊢ a₁ = a₂
have h_add : ∀ (x x_1 : R), x + x_1 = x + x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ a₁ = a₂
have h_mul : ∀ (x x_1 : R), x * x_1 = x * x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have this : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
Tactic: have : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne :=
    AddMonoidWithOne.ext h_add h_one
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have this₁ : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
Tactic: have : inst₁.toNatCast = inst₂.toNatCast := congrArg (·.toNatCast) this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have h_group : Eq.{u + 1} (α := AddGroup R) toAddGroup toAddGroup
Tactic: have h_group : inst₁.toAddGroup = inst₂.toAddGroup := by ext : 1; exact h_add
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have h_group₁ : Eq.{u + 1} (α := SubNegMonoid R)
  { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, sub_eq_add_neg := sorry,
    zsmul := AddGroupWithOne.zsmul, zsmul_zero' := sorry, zsmul_succ' := sorry, zsmul_neg' := sorry }
  { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, sub_eq_add_neg := sorry,
    zsmul := AddGroupWithOne.zsmul, zsmul_zero' := sorry, zsmul_succ' := sorry, zsmul_neg' := sorry }
Tactic: injection h_group with h_group
Cleared hypotheses: h_group
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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' := ⋯ }
⊢ inst₁ = inst₂
have toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
Tactic: injection h_group
Cleared hypotheses: h_group
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
Tactic: injection h_group
Cleared hypotheses: h_group
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
Tactic: injection h_group
Cleared hypotheses: h_group
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
Tactic: injection h_group
Cleared hypotheses: h_group
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ Eq.{u + 1} (α := ℤ → R) IntCast.intCast IntCast.intCast
have h : ∀ (n : ℤ), Eq.{u + 1} (α := R) (IntCast.intCast n) (IntCast.intCast n)
Tactic: funext n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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) (IntCast.intCast (Int.ofNat n)) (IntCast.intCast (Int.ofNat n))
have h : Eq.{u + 1} (α := R) (↑n : R) (↑n : R)
Tactic: rewrite [Int.ofNat_eq_natCast, inst₁.intCast_ofNat, inst₂.intCast_ofNat]