awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.GrindInstances (goal)
Goal:
α : Type u_1
s : Semiring α
n : ℕ
⊢ (↑(n + 2 + 1) : α) = HAdd.hAdd (α := α) (↑(n + 2) : α) 1
have rw : Eq.{u_1 + 1} (α := α) (↑(n + 2 + 1) : α) ↑(n + 2 + 1)
Tactic: rw [← AddMonoidWithOne.natCast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GrindInstances (goal)
Goal:
α : Type u_1
s : Grind.CommRing α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(Int.negSucc n) : α) (-(↑(n + 1) : α))
have rw : Eq.{u_1 + 1} (α := α) (↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : α) (-(↑(n + 1) : α))
Tactic: rw [Int.negSucc_eq, Grind.Ring.intCast_neg,
        Grind.Ring.intCast_natCast_add_one, Grind.Semiring.natCast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GrindInstances (goal)
Goal:
α : Type u_1
s : Grind.CommRing α
n : ℕ
rw : Eq.{u_1 + 1} (α := α) (↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : α) (-(↑(n + 1) : α))
⊢ Eq.{u_1 + 1} (α := α) (↑(Int.negSucc n) : α) (-(↑(n + 1) : α))
have rw₁ : Eq.{u_1 + 1} (α := α) (-(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : α)) (-(↑(n + 1) : α))
Tactic: rw [Int.negSucc_eq, Grind.Ring.intCast_neg,
        Grind.Ring.intCast_natCast_add_one, Grind.Semiring.natCast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GrindInstances (goal)
Goal:
α : Type u_1
s : Grind.CommRing α
n : ℕ
rw : Eq.{u_1 + 1} (α := α) (↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : α) (-(↑(n + 1) : α))
rw₁ : Eq.{u_1 + 1} (α := α) (-(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : α)) (-(↑(n + 1) : α))
⊢ Eq.{u_1 + 1} (α := α) (↑(Int.negSucc n) : α) (-(↑(n + 1) : α))
have rw₂ : -HAdd.hAdd (α := α) (↑n : α) 1 = -(↑(n + 1) : α)
Tactic: rw [Int.negSucc_eq, Grind.Ring.intCast_neg,
        Grind.Ring.intCast_natCast_add_one, Grind.Semiring.natCast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GrindInstances (goal)
Goal:
α : Type u_1
s : Grind.CommRing α
n : ℕ
rw : Eq.{u_1 + 1} (α := α) (↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : α) (-(↑(n + 1) : α))
rw₁ : Eq.{u_1 + 1} (α := α) (-(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : α)) (-(↑(n + 1) : α))
rw₂ : -HAdd.hAdd (α := α) (↑n : α) 1 = -(↑(n + 1) : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(Int.negSucc n) : α) (-(↑(n + 1) : α))
have rw₃ : -HAdd.hAdd (α := α) (↑n : α) 1 = -HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [Int.negSucc_eq, Grind.Ring.intCast_neg,
        Grind.Ring.intCast_natCast_add_one, Grind.Semiring.natCast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
f g : α →ₙ+* β
h : Eq (α := (a : α) → β) ((fun (f : α →ₙ+* β) ↦ f.toFun) f) ((fun (f : α →ₙ+* β) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toMulHom : α →ₙ* β) (map_zero' : toMulHom.toFun 0 = 0)
  (map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
      ((fun (f : α →ₙ+* β) ↦ f.toFun) g)),
  { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' : α →ₙ+* β } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
g : α →ₙ+* β
toMulHom : α →ₙ* β
map_zero' : toMulHom.toFun 0 = 0
map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →ₙ+* β) ↦ f.toFun) g)
⊢ { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' : α →ₙ+* β } = g
have mk : ∀ (toMulHom_1 : α →ₙ* β) (map_zero'_1 : toMulHom_1.toFun 0 = 0)
  (map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
      ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })),
  { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' : α →ₙ+* β } =
    { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
toMulHom : α →ₙ* β
map_zero' : toMulHom.toFun 0 = 0
map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y
toMulHom_1 : α →ₙ* β
map_zero'_1 : toMulHom_1.toFun 0 = 0
map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
⊢ { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' : α →ₙ+* β } =
    { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }
have mk : toMulHom = toMulHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
toMulHom : α →ₙ* β
map_zero' : toMulHom.toFun 0 = 0
map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y
toMulHom_1 : α →ₙ* β
map_zero'_1 : toMulHom_1.toFun 0 = 0
map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →ₙ+* β) ↦ f.toFun) { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
⊢ toMulHom = toMulHom_1
have mk : Eq (α := (a : α) → β) (⇑toMulHom : (a : α) → β) (⇑toMulHom_1 : (a : α) → β)
Tactic: apply DFunLike.coe_injective'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
⊢ Eq (α := α →ₙ+* γ) (g.comp 0) 0
have a : ∀ (x : α), Eq.{u_4 + 1} (α := γ) ((g.comp 0 : (a : α) → γ) x : γ) ((0 : (a : α) → γ) x : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
⊢ Eq (α := α →ₙ+* γ) (comp 0 f) 0
have a : ∀ (x : α), Eq.{u_4 + 1} (α := γ) ((comp 0 f : (a : α) → γ) x : γ) ((0 : (a : α) → γ) x : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : NonUnitalNonAssocSemiring β
inst_2 : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f g : α →+* β
h :
  Eq (α := (a : α) → β) ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) f)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)
⊢ f = g
have mk : ∀ (toMonoidHom : α →* β) (map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0)
  (map_add' :
    ∀ (x_2 y : α),
      (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
        (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
        { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
      ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)),
  { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' : α →+* β } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
g : α →+* β
toMonoidHom : α →* β
map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0
map_add' :
  ∀ (x_2 y : α),
    (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)
⊢ { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' : α →+* β } = g
have mk : ∀ (toMonoidHom_1 : α →* β) (map_zero'_1 : (↑toMonoidHom_1 : OneHom α β).toFun 0 = 0)
  (map_add'_1 :
    ∀ (x_2 y : α),
      (↑toMonoidHom_1 : OneHom α β).toFun (x_2 + y) =
        (↑toMonoidHom_1 : OneHom α β).toFun x_2 + (↑toMonoidHom_1 : OneHom α β).toFun y)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
        { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
      ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
        { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })),
  { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' : α →+* β } =
    { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
toMonoidHom : α →* β
map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0
map_add' :
  ∀ (x_2 y : α),
    (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y
toMonoidHom_1 : α →* β
map_zero'_1 : (↑toMonoidHom_1 : OneHom α β).toFun 0 = 0
map_add'_1 :
  ∀ (x_2 y : α),
    (↑toMonoidHom_1 : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom_1 : OneHom α β).toFun x_2 + (↑toMonoidHom_1 : OneHom α β).toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
⊢ { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' : α →+* β } =
    { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }
have mk : toMonoidHom = toMonoidHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
toMonoidHom : α →* β
map_zero' : (↑toMonoidHom : OneHom α β).toFun 0 = 0
map_add' :
  ∀ (x_2 y : α),
    (↑toMonoidHom : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom : OneHom α β).toFun x_2 + (↑toMonoidHom : OneHom α β).toFun y
toMonoidHom_1 : α →* β
map_zero'_1 : (↑toMonoidHom_1 : OneHom α β).toFun 0 = 0
map_add'_1 :
  ∀ (x_2 y : α),
    (↑toMonoidHom_1 : OneHom α β).toFun (x_2 + y) =
      (↑toMonoidHom_1 : OneHom α β).toFun x_2 + (↑toMonoidHom_1 : OneHom α β).toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' })
    ((fun (f : α →+* β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
      { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 })
⊢ toMonoidHom = toMonoidHom_1
have mk : Eq (α := (a : α) → β) (⇑toMonoidHom : (a : α) → β) (⇑toMonoidHom_1 : (a : α) → β)
Tactic: apply DFunLike.coe_injective'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
⊢ Eq.{u_3 + 1} (α := β) 0 1 ↔ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)
have rw : Eq.{u_3 + 1} (α := β) 0 1 ↔ Eq.{u_3 + 1} (α := β) 1 0
Tactic: rw [map_one, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
rw : Eq.{u_3 + 1} (α := β) 0 1 ↔ Eq.{u_3 + 1} (α := β) 1 0
⊢ Eq.{u_3 + 1} (α := β) 0 1 ↔ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)
have rw₁ : Eq.{u_3 + 1} (α := β) 1 0 ↔ Eq.{u_3 + 1} (α := β) 1 0
Tactic: rw [map_one, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
f : α →+* β
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)
x : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) (0 : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x * 1) : β) (0 : β)
Tactic: rw [← mul_one x, map_mul, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
f : α →+* β
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)
x : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x * 1) : β) (0 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) (0 : β)
have rw₁ : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) 1 : β) = 0
Tactic: rw [← mul_one x, map_mul, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
f : α →+* β
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)
x : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x * 1) : β) (0 : β)
rw₁ : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) 1 : β) = 0
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) (0 : β)
have rw₂ : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) (0 : β) = 0
Tactic: rw [← mul_one x, map_mul, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
f : α →+* β
h : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)
x : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x * 1) : β) (0 : β)
rw₁ : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) 1 : β) = 0
rw₂ : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) (0 : β) = 0
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) (0 : β)
have rw₃ : Eq.{u_3 + 1} (α := β) 0 0
Tactic: rw [← mul_one x, map_mul, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
inst : Nontrivial β
h : Eq.{u_2 + 1} (α := α) 1 0
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
f : α →+* β
inst : Nontrivial β
h : Eq.{u_2 + 1} (α := α) 1 0
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)
have rw₁ : Eq.{u_3 + 1} (α := β) 0 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
x_2 : NonAssocSemiring γ
n : ℕ
f : α →+* α
⊢ Eq (α := α → α) (⇑f : (a : α) → α)^[n] (⇑(npowRec n f) : (a : α) → α)
have zero : Eq (α := α → α) (⇑f : (a : α) → α)^[0] (⇑(npowRec 0 f) : (a : α) → α)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x : NonAssocSemiring α
x_1 : NonAssocSemiring β
x_2 : NonAssocSemiring γ
n : ℕ
f : α →+* α
zero : Eq (α := α → α) (⇑f : (a : α) → α)^[0] (⇑(npowRec 0 f) : (a : α) → α)
⊢ Eq (α := α → α) (⇑f : (a : α) → α)^[n] (⇑(npowRec n f) : (a : α) → α)
have succ : ∀ (n : ℕ),
  Eq (α := α → α) (⇑f : (a : α) → α)^[n] (⇑(npowRec n f) : (a : α) → α) →
    Eq (α := α → α) (⇑f : (a : α) → α)^[n + 1] (⇑(npowRec (n + 1) f) : (a : α) → α)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
x_3 : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
x_3 : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
x_3 : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (hypothesis)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommRing α
inst_1 : IsDomain α
inst_2 : CommRing β
f : β →+ α
h :
  ∀ (x : β), (f : (a : β) → α) (x * x) = HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) x : α)
h_two : Ne.{u_2 + 1} (α := α) 2 0
h_one : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) 1 : α) (1 : α)
x y : β
⊢ (↑f : ZeroHom β α).toFun (x * y) = (↑f : ZeroHom β α).toFun x * (↑f : ZeroHom β α).toFun y
have hxy : (f : (a : β) → α) ((x + y) * (x + y)) =
  HMul.hMul (α := α) (β := α) ((f : (a : β) → α) (x + y) : α) ((f : (a : β) → α) (x + y) : α)
Tactic: have hxy := h (x + y)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (hypothesis)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommRing α
inst_1 : IsDomain α
inst_2 : CommRing β
f : β →+ α
h :
  ∀ (x : β), (f : (a : β) → α) (x * x) = HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) x : α)
h_two : Ne.{u_2 + 1} (α := α) 2 0
h_one : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) 1 : α) (1 : α)
x y : β
hxy :
  (f : (a : β) → α) ((x + y) * (x + y)) =
    HMul.hMul (α := α) (β := α) ((f : (a : β) → α) (x + y) : α) ((f : (a : β) → α) (x + y) : α)
⊢ (↑f : ZeroHom β α).toFun (x * y) = (↑f : ZeroHom β α).toFun x * (↑f : ZeroHom β α).toFun y
have hxy₁ : HAdd.hAdd (α := α) ((f : (a : β) → α) (x * y) : α)
              (HMul.hMul (α := α) (β := α) ((f : (a : β) → α) y : α) ((f : (a : β) → α) y : α)) +
            HAdd.hAdd (β := α) (HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) x : α))
              ((f : (a : β) → α) (x * y) : α) -
          HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) x : α) -
        HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) -
      HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) -
    HMul.hMul (α := α) (β := α) ((f : (a : β) → α) y : α) ((f : (a : β) → α) y : α) =
  0
Tactic: rw [mul_add, add_mul, add_mul, f.map_add, f.map_add, f.map_add, f.map_add, h x, h y, add_mul,
        mul_add, mul_add, ← sub_eq_zero, add_comm (f x * f x + f (y * x)), ← sub_sub, ← sub_sub,
        ← sub_sub, mul_comm y x, mul_comm (f y) (f x)] at hxy
Cleared hypotheses: hxy