awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + a * (a * b) = a
rw₁ : a * a + a * b + a * (a * b) = a
rw₂ : a + a * b + a * (a * b) = a
rw₃ : a + a * b + a * a * b = a
rw₄ : a + a * b + a * b = a
⊢ a * (a + b + a * b) = a
have rw₅ : a + (a * b + a * b) = a
Tactic: rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + a * (a * b) = a
rw₁ : a * a + a * b + a * (a * b) = a
rw₂ : a + a * b + a * (a * b) = a
rw₃ : a + a * b + a * a * b = a
rw₄ : a + a * b + a * b = a
rw₅ : a + (a * b + a * b) = a
⊢ a * (a + b + a * b) = a
have rw₆ : a + 0 = a
Tactic: rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + a * (a * b) = a
rw₁ : a * a + a * b + a * (a * b) = a
rw₂ : a + a * b + a * (a * b) = a
rw₃ : a + a * b + a * a * b = a
rw₄ : a + a * b + a * b = a
rw₅ : a + (a * b + a * b) = a
rw₆ : a + 0 = a
⊢ a * (a + b + a * b) = a
have rw₇ : a = a
Tactic: rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c
have dsimp : (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
    (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
  a + b * c + a * (b * c)
Tactic: dsimp only [(· ⊔ ·), (· ⊓ ·)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
have rw : a + b * c + a * (b * c) + (a + b * c + a * (b * c)) + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) =
  a + b * c + a * (b * c)
Tactic: rw [le_sup_inf_aux, add_self, mul_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
rw :
  a + b * c + a * (b * c) + (a + b * c + a * (b * c)) + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
have rw₁ : 0 + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) = a + b * c + a * (b * c)
Tactic: rw [le_sup_inf_aux, add_self, mul_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
rw :
  a + b * c + a * (b * c) + (a + b * c + a * (b * c)) + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
rw₁ : 0 + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) = a + b * c + a * (b * c)
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
have rw₂ : 0 + (a + b * c + a * (b * c)) = a + b * c + a * (b * c)
Tactic: rw [le_sup_inf_aux, add_self, mul_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
rw :
  a + b * c + a * (b * c) + (a + b * c + a * (b * c)) + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
rw₁ : 0 + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) = a + b * c + a * (b * c)
rw₂ : 0 + (a + b * c + a * (b * c)) = a + b * c + a * (b * c)
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
have rw₃ : a + b * c + a * (b * c) = a + b * c + a * (b * c)
Tactic: rw [le_sup_inf_aux, add_self, mul_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
⊢ 1 ≤ a ⊔ (1 + a)
have a₁ : 1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) = a + (1 + a) + a * (1 + a)
Tactic: change
        1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) =
          a + (1 + a) + a * (1 + a)
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
⊢ 1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) = a + (1 + a) + a * (1 + a)
have simp : 1 + (a + (1 + a)) = 0
Tactic: simp [mul_add, mul_self, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
⊢ 1 + (a + (1 + a)) = 0
have rw : 1 + a + (1 + a) = 0
Tactic: rw [← add_assoc, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : 1 + a + (1 + a) = 0
⊢ 1 + (a + (1 + a)) = 0
have rw₁ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [← add_assoc, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
⊢ a + 1 + a * 1 = 1
have rw : a + 1 + a = 1
Tactic: rw [mul_one, add_comm a 1,
                                                     add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : a + 1 + a = 1
⊢ a + 1 + a * 1 = 1
have rw₁ : 1 + a + a = 1
Tactic: rw [mul_one, add_comm a 1,
                                                     add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : a + 1 + a = 1
rw₁ : 1 + a + a = 1
⊢ a + 1 + a * 1 = 1
have rw₂ : 1 + (a + a) = 1
Tactic: rw [mul_one, add_comm a 1,
                                                     add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : a + 1 + a = 1
rw₁ : 1 + a + a = 1
rw₂ : 1 + (a + a) = 1
⊢ a + 1 + a * 1 = 1
have rw₃ : HAdd.hAdd (α := α) 1 0 = 1
Tactic: rw [mul_one, add_comm a 1,
                                                     add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : a + 1 + a = 1
rw₁ : 1 + a + a = 1
rw₂ : 1 + (a + a) = 1
rw₃ : HAdd.hAdd (α := α) 1 0 = 1
⊢ a + 1 + a * 1 = 1
have rw₄ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [mul_one, add_comm a 1,
                                                     add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
⊢ 0 + a + 0 * a = a
have rw : 0 + a + 0 = a
Tactic: rw [zero_mul, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : 0 + a + 0 = a
⊢ 0 + a + 0 * a = a
have rw₁ : a + 0 = a
Tactic: rw [zero_mul, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
a : α
rw : 0 + a + 0 = a
rw₁ : a + 0 = a
⊢ 0 + a + 0 * a = a
have rw₂ : a = a
Tactic: rw [zero_mul, zero_add, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : AsBoolAlg α
⊢ (ofBoolAlg : (a : AsBoolAlg α) → α) (a ∆ b) =
    HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)
have rw : (ofBoolAlg : (a : AsBoolAlg α) → α) ((a ⊔ b) \ (a ⊓ b)) =
  HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)
Tactic: rw [symmDiff_eq_sup_sdiff_inf]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
⊢ Eq.{u_2 + 1} (α := AsBoolAlg β)
    (Function.comp (β := β) (⇑toBoolAlg : (a : β) → AsBoolAlg β)
      (Function.comp (β := α) (⇑f : (a : α) → β) (⇑ofBoolAlg : (a : AsBoolAlg α) → α)) (a ⊔ b))
    (Function.comp (β := β) (⇑toBoolAlg : (a : β) → AsBoolAlg β)
        (Function.comp (β := α) (⇑f : (a : α) → β) (⇑ofBoolAlg : (a : AsBoolAlg α) → α)) a ⊔
      Function.comp (β := β) (⇑toBoolAlg : (a : β) → AsBoolAlg β)
        (Function.comp (β := α) (⇑f : (a : α) → β) (⇑ofBoolAlg : (a : AsBoolAlg α) → α)) b)
have dsimp : Eq.{u_2 + 1} (α := AsBoolAlg β)
  ((toBoolAlg : (a : β) → AsBoolAlg β)
      ((f : (a : α) → β)
          (HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
              ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) +
            HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
              ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)) :
        β) :
    AsBoolAlg β)
  ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
      (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
    AsBoolAlg β)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
⊢ Eq.{u_2 + 1} (α := AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β)
        ((f : (a : α) → β)
            (HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) +
              HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)) :
          β) :
      AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
        (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
      AsBoolAlg β)
have simp_rw : Eq (α := AsBoolAlg β)
  ((toBoolAlg : (a : β) → AsBoolAlg β)
      (HAdd.hAdd (β := β)
        (HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β)
          ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β))
        ((f : (a : α) → β)
            (HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
              ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)) :
          β)) :
    AsBoolAlg β)
  ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
      (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
    AsBoolAlg β)
Tactic: simp_rw [map_add f, map_mul f, toBoolAlg_add_add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
inst_1 : BooleanRing β
inst_2 : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
simp_rw :
  Eq (α := AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β)
        (HAdd.hAdd (β := β)
          (HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β)
            ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β))
          ((f : (a : α) → β)
              (HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)) :
            β)) :
      AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
        (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
      AsBoolAlg β)
⊢ Eq.{u_2 + 1} (α := AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β)
        ((f : (a : α) → β)
            (HAdd.hAdd (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) +
              HMul.hMul (α := α) (β := α) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α)
                ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α)) :
          β) :
      AsBoolAlg β)
    ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
        (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
      AsBoolAlg β)
have simp_rw₁ : Eq (α := AsBoolAlg β)
  ((toBoolAlg : (a : β) → AsBoolAlg β)
      (HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β)
          ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) +
        HMul.hMul (α := β) (β := β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β)
          ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β)) :
    AsBoolAlg β)
  ((toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) a : α) : β) ⊔
      (toBoolAlg : (a : β) → AsBoolAlg β) ((f : (a : α) → β) ((ofBoolAlg : (a : AsBoolAlg α) → α) b : α) : β) :
    AsBoolAlg β)
Tactic: simp_rw [map_add f, map_mul f, toBoolAlg_add_add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a : Bool
⊢ a * 0 = 0
have false : false * 0 = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a : Bool
false : Bool.false * 0 = 0
⊢ a * 0 = 0
have true : true * 0 = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
x : M
⊢ Commute (↑n : M) x
have rw : (↑n : M) * x = x * (↑n : M)
Tactic: rw [commute_iff_eq, Nat.commute_cast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
x : M
rw : (↑n : M) * x = x * (↑n : M)
⊢ Commute (↑n : M) x
have rw₁ : (↑n : M) * x = (↑n : M) * x
Tactic: rw [commute_iff_eq, Nat.commute_cast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
⊢ (↑0 : M) * (x * x_1) = (↑0 : M) * x * x_1
have zero : 0 * (x * x_1) = 0 * x * x_1
Tactic: rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
zero : 0 * (x * x_1) = 0 * x * x_1
⊢ (↑0 : M) * (x * x_1) = (↑0 : M) * x * x_1
have zero₁ : 0 = 0 * x * x_1
Tactic: rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
zero : 0 * (x * x_1) = 0 * x * x_1
zero₁ : 0 = 0 * x * x_1
⊢ (↑0 : M) * (x * x_1) = (↑0 : M) * x * x_1
have zero₂ : 0 = 0 * x_1
Tactic: rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
zero : 0 * (x * x_1) = 0 * x * x_1
zero₁ : 0 = 0 * x * x_1
zero₂ : 0 = 0 * x_1
⊢ (↑0 : M) * (x * x_1) = (↑0 : M) * x * x_1
have zero₃ : Eq.{u_1 + 1} (α := M) 0 0
Tactic: rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
⊢ (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1
have succ : HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
Tactic: rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
succ : HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
⊢ (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1
have succ₁ : (↑n : M) * (x * x_1) + 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
Tactic: rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
succ : HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₁ : (↑n : M) * (x * x_1) + 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
⊢ (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1
have succ₂ : (↑n : M) * (x * x_1) + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
Tactic: rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
succ : HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₁ : (↑n : M) * (x * x_1) + 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₂ : (↑n : M) * (x * x_1) + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
⊢ (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1
have succ₃ : (↑n : M) * x * x_1 + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
Tactic: rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
succ : HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₁ : (↑n : M) * (x * x_1) + 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₂ : (↑n : M) * (x * x_1) + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₃ : (↑n : M) * x * x_1 + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
⊢ (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1
have succ₄ : (↑n : M) * x * x_1 + x * x_1 = ((↑n : M) * x + 1 * x) * x_1
Tactic: rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
succ : HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₁ : (↑n : M) * (x * x_1) + 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₂ : (↑n : M) * (x * x_1) + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₃ : (↑n : M) * x * x_1 + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₄ : (↑n : M) * x * x_1 + x * x_1 = ((↑n : M) * x + 1 * x) * x_1
⊢ (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1
have succ₅ : (↑n : M) * x * x_1 + x * x_1 = (↑n : M) * x * x_1 + 1 * x * x_1
Tactic: rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
succ : HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₁ : (↑n : M) * (x * x_1) + 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₂ : (↑n : M) * (x * x_1) + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₃ : (↑n : M) * x * x_1 + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₄ : (↑n : M) * x * x_1 + x * x_1 = ((↑n : M) * x + 1 * x) * x_1
succ₅ : (↑n : M) * x * x_1 + x * x_1 = (↑n : M) * x * x_1 + 1 * x * x_1
⊢ (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1
have succ₆ : (↑n : M) * x * x_1 + x * x_1 = (↑n : M) * x * x_1 + x * x_1
Tactic: rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
x x_1 : M
⊢ (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
have zero : (↑0 : M) * (x * x_1) = (↑0 : M) * x * x_1
Tactic: induction n with
    | zero => rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
    | succ n ihn => rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
x x_1 : M
zero : (↑0 : M) * (x * x_1) = (↑0 : M) * x * x_1
⊢ (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
have succ : ∀ (n : ℕ) (ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1), (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1
Tactic: induction n with
    | zero => rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
    | succ n ihn => rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
⊢ x * x_1 * (↑0 : M) = x * (x_1 * (↑0 : M))
have zero : x * x_1 * 0 = x * (x_1 * 0)
Tactic: rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
zero : x * x_1 * 0 = x * (x_1 * 0)
⊢ x * x_1 * (↑0 : M) = x * (x_1 * (↑0 : M))
have zero₁ : 0 = x * (x_1 * 0)
Tactic: rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
zero : x * x_1 * 0 = x * (x_1 * 0)
zero₁ : 0 = x * (x_1 * 0)
⊢ x * x_1 * (↑0 : M) = x * (x_1 * (↑0 : M))
have zero₂ : 0 = x * 0
Tactic: rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
zero : x * x_1 * 0 = x * (x_1 * 0)
zero₁ : 0 = x * (x_1 * 0)
zero₂ : 0 = x * 0
⊢ x * x_1 * (↑0 : M) = x * (x_1 * (↑0 : M))
have zero₃ : Eq.{u_1 + 1} (α := M) 0 0
Tactic: rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
⊢ x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))
have succ : x * x_1 * HAdd.hAdd (α := M) (↑n : M) 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
Tactic: rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
succ : x * x_1 * HAdd.hAdd (α := M) (↑n : M) 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
⊢ x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))
have succ₁ : x * x_1 * (↑n : M) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
Tactic: rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
succ : x * x_1 * HAdd.hAdd (α := M) (↑n : M) 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₁ : x * x_1 * (↑n : M) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
⊢ x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))
have succ₂ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
Tactic: rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]