awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
e f : R ≃+* S
h₁ : e.toFun = f.toFun
h₂ : e.invFun = f.invFun
⊢ e = f
have mk : ∀ (toEquiv : R ≃ S) (map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
  (map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y)
  (h₁ : { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.toFun = f.toFun)
  (h₂ : { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.invFun = f.invFun),
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S } = f
Tactic: cases e
Cleared hypotheses: e, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
f : R ≃+* S
toEquiv : R ≃ S
map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y
h₁ : { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.toFun = f.toFun
h₂ : { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.invFun = f.invFun
⊢ { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S } = f
have mk : ∀ (toEquiv_1 : R ≃ S) (map_mul'_1 : ∀ (x y : R), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y)
  (map_add'_1 : ∀ (x y : R), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y)
  (h₁ :
    { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.toFun =
      { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.toFun)
  (h₂ :
    { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.invFun =
      { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.invFun),
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S } =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 }
Tactic: cases f
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
toEquiv : R ≃ S
map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y
toEquiv_1 : R ≃ S
map_mul'_1 : ∀ (x y : R), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y
map_add'_1 : ∀ (x y : R), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y
h₁ :
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.toFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.toFun
h₂ :
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.invFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.invFun
⊢ { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S } =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 }
have mk : toEquiv = toEquiv_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ NonUnitalRingHom.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) f = NonUnitalRingHom.id R
have a : ∀ (x : R),
  Eq (α := R) ((NonUnitalRingHom.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) f : (a : R) → R) x : R)
    ((NonUnitalRingHom.id R : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) = NonUnitalRingHom.id S
have a : ∀ (x : S),
  Eq (α := S) ((f.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) : (a : S) → S) x : S)
    ((NonUnitalRingHom.id S : (a : S) → S) x : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R ≃+* S
x : R
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) (-1 : S) ↔ x = -1
have rw : Eq.{u_5 + 1} (α := S) (-(f : (a : R) → S) x : S) (1 : S) ↔ x = -1
Tactic: rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R ≃+* S
x : R
rw : Eq.{u_5 + 1} (α := S) (-(f : (a : R) → S) x : S) (1 : S) ↔ x = -1
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) (-1 : S) ↔ x = -1
have rw₁ : Eq.{u_5 + 1} (α := S) (-(f : (a : R) → S) x : S) (1 : S) ↔ -x = 1
Tactic: rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R ≃+* S
x : R
rw : Eq.{u_5 + 1} (α := S) (-(f : (a : R) → S) x : S) (1 : S) ↔ x = -1
rw₁ : Eq.{u_5 + 1} (α := S) (-(f : (a : R) → S) x : S) (1 : S) ↔ -x = 1
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) (-1 : S) ↔ x = -1
have rw₂ : Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (-x) : S) (1 : S) ↔ -x = 1
Tactic: rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R ≃+* S
x : R
rw : Eq.{u_5 + 1} (α := S) (-(f : (a : R) → S) x : S) (1 : S) ↔ x = -1
rw₁ : Eq.{u_5 + 1} (α := S) (-(f : (a : R) → S) x : S) (1 : S) ↔ -x = 1
rw₂ : Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (-x) : S) (1 : S) ↔ -x = 1
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) (-1 : S) ↔ x = -1
have rw₃ : -x = 1 ↔ -x = 1
Tactic: rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_7
S : Type u_8
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ Eq (α := R →ₙ+* S) (↑f : R →ₙ+* S) (↑g : R →ₙ+* S)
have rw : Eq (α := R →ₙ+* S) (↑g : R →ₙ+* S) (↑g : R →ₙ+* S)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S
have a : ∀ (x : S),
  Eq (α := S) ((e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom : (a : S) → S) x : S)
    ((NonUnitalRingHom.id S : (a : S) → S) x : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R
have a : ∀ (x : R),
  Eq (α := R) ((e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom : (a : R) → R) x : R)
    ((NonUnitalRingHom.id R : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Equiv (goal)
Goal:
R : Type u_7
S : Type u_8
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ Eq (α := R →+* S) (↑f : R →+* S) (↑g : R →+* S)
have rw : Eq (α := R →+* S) (↑g : R →+* S) (↑g : R →+* S)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
inst₁ inst₂ : Distrib 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 : ∀ (mul add : 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) (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd)
  (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul),
  { mul := mul, add := add, left_distrib := left_distrib, right_distrib := right_distrib : Distrib 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₂ : Distrib R
mul add : 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
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ { mul := mul, add := add, left_distrib := left_distrib, right_distrib := right_distrib : Distrib R } = inst₂
have rcases : ∀ (mul_1 add_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) (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd)
  (h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul),
  { mul := mul, add := add, left_distrib := left_distrib, right_distrib := right_distrib : Distrib R } =
    { mul := mul_1, add := add_1, left_distrib := left_distrib_1, right_distrib := right_distrib_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
inst₁ inst₂ : NonUnitalNonAssocSemiring 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 : ∀ [toAddCommMonoid : AddCommMonoid 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),
  { toAddCommMonoid := toAddCommMonoid, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
      zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocSemiring 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₂ : NonUnitalNonAssocSemiring R
toAddCommMonoid : AddCommMonoid 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
⊢ { toAddCommMonoid := toAddCommMonoid, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
      zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocSemiring R } =
    inst₂
have rcases : ∀ [toAddCommMonoid_1 : AddCommMonoid 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),
  { toAddCommMonoid := toAddCommMonoid, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
      zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocSemiring R } =
    { toAddCommMonoid := toAddCommMonoid_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
toAddCommMonoid : AddCommMonoid 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
toAddCommMonoid_1 : AddCommMonoid 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
⊢ { toAddCommMonoid := toAddCommMonoid, mul := mul, left_distrib := left_distrib, right_distrib := right_distrib,
      zero_mul := zero_mul, mul_zero := mul_zero : NonUnitalNonAssocSemiring R } =
    { toAddCommMonoid := toAddCommMonoid_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_toAddCommMonoid : toAddCommMonoid = toAddCommMonoid_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : NonUnitalNonAssocSemiring R
h : Eq.{u + 1} (α := Distrib R) toDistrib toDistrib
⊢ 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₂ : NonUnitalNonAssocSemiring R
h : Eq.{u + 1} (α := Distrib R) toDistrib toDistrib
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₂ : AddMonoidWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
⊢ inst₁ = inst₂
have h_monoid : Eq.{u + 1} (α := AddMonoid R) toAddMonoid toAddMonoid
Tactic: have h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid := by ext : 1; exact h_add
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have h_zero' : Eq.{u + 1} (α := Zero R) AddMonoid.toZero AddMonoid.toZero
Tactic: have h_zero' : inst₁.toZero = inst₂.toZero := congrArg (·.toZero) h_monoid
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have h_one' : Eq.{u + 1} (α := One R) toOne toOne
Tactic: have h_one' : inst₁.toOne = inst₂.toOne :=
    congrArg One.mk h_one
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
have h : ∀ (n : ℕ), Eq.{u + 1} (α := R) ↑n ↑n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
have h : Eq.{u + 1} (α := R) 0 0
Tactic: rewrite [inst₁.natCast_zero, inst₂.natCast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ Eq.{u + 1} (α := R) ↑(n + 1) ↑(n + 1)
have h₁ : HAdd.hAdd (α := R) (↑n) 1 = HAdd.hAdd (α := R) (↑n) 1
Tactic: rw [inst₁.natCast_succ, inst₂.natCast_succ, h_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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 : ℕ
⊢ Eq.{u + 1} (α := R) ↑n ↑n
have h : Eq.{u + 1} (α := R) ↑0 ↑0
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ Eq.{u + 1} (α := R) ↑n ↑n
have h₁ : ∀ (n : ℕ) (h : Eq.{u + 1} (α := R) ↑n ↑n), Eq.{u + 1} (α := R) ↑(n + 1) ↑(n + 1)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (hypothesis)
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
⊢ inst₁ = inst₂
have h_natCast : 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
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ inst₁ = inst₂
have 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₂
Tactic: rcases inst₁ with @⟨⟨⟩⟩
Cleared hypotheses: inst₁, h_add, h_one, h_monoid, h_zero', h_one', h_natCast
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ { natCast := natCast, toAddMonoid := toAddMonoid, toOne := toOne, natCast_zero := natCast_zero,
      natCast_succ := natCast_succ : AddMonoidWithOne R } =
    inst₂
have 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 }
Tactic: rcases inst₂ with @⟨⟨⟩⟩
Cleared hypotheses: inst₂, h_add, h_one, h_monoid, h_zero', h_one', h_natCast
-- 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
⊢ inst₁ = inst₂
have h : Eq.{u + 1} (α := NonUnitalNonAssocSemiring R) toNonUnitalNonAssocSemiring toNonUnitalNonAssocSemiring
Tactic: have h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring := 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
⊢ inst₁ = inst₂
have h_zero : 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
-- 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
⊢ Eq.{u + 1} (α := One R) MulOne.toOne MulOne.toOne
have h₁ : Eq.{u + 1} (α := MulOneClass R) MulZeroOneClass.toMulOneClass MulZeroOneClass.toMulOneClass
Tactic: congr 2
-- 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
⊢ Eq.{u + 1} (α := MulOneClass R) MulZeroOneClass.toMulOneClass MulZeroOneClass.toMulOneClass
have h₁ : Eq.{u + 1} (α := R → R → R) Mul.mul Mul.mul
Tactic: ext : 1