awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
commute_half_left :
  ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
⊢ (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α) +
          HMul.hMul (α := α) (β := α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α)
            ((unsym : (a : αˢʸᵐ) → α) a : α))) =
    a * (b * (a * a))
have calc_3 : HMul.hMul (β := αˢʸᵐ) a
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))) :
      αˢʸᵐ) =
  a * (b * (a * a))
Tactic: rw [← mul_def, ← mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
commute_half_left :
  ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
calc_3 :
  HMul.hMul (β := αˢʸᵐ) a
      ((sym : (a : α) → αˢʸᵐ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))) :
        αˢʸᵐ) =
    a * (b * (a * a))
⊢ (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α) +
          HMul.hMul (α := α) (β := α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α)
            ((unsym : (a : αˢʸᵐ) → α) a : α))) =
    a * (b * (a * a))
have calc_3₁ : a * (b * (a * a)) = a * (b * (a * a))
Tactic: rw [← mul_def, ← mul_def]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r₁ r₂ : R
⊢ 0 = r₁ •> 0 + 0 <• r₂
have rw : 0 = 0 + 0 <• r₂
Tactic: rw [smul_zero, zero_add, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r₁ r₂ : R
rw : 0 = 0 + 0 <• r₂
⊢ 0 = r₁ •> 0 + 0 <• r₂
have rw₁ : 0 = 0 <• r₂
Tactic: rw [smul_zero, zero_add, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r₁ r₂ : R
rw : 0 = 0 + 0 <• r₂
rw₁ : 0 = 0 <• r₂
⊢ 0 = r₁ •> 0 + 0 <• r₂
have rw₂ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [smul_zero, zero_add, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
m₁ m₂ : M
⊢ 0 •> m₂ + m₁ <• 0 = 0
have rw : 0 + m₁ <• 0 = 0
Tactic: rw [zero_smul, zero_add, op_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
m₁ m₂ : M
rw : 0 + m₁ <• 0 = 0
⊢ 0 •> m₂ + m₁ <• 0 = 0
have rw₁ : m₁ <• 0 = 0
Tactic: rw [zero_smul, zero_add, op_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
m₁ m₂ : M
rw : 0 + m₁ <• 0 = 0
rw₁ : m₁ <• 0 = 0
⊢ 0 •> m₂ + m₁ <• 0 = 0
have rw₂ : 0 •> m₁ = 0
Tactic: rw [zero_smul, zero_add, op_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
m₁ m₂ : M
rw : 0 + m₁ <• 0 = 0
rw₁ : m₁ <• 0 = 0
rw₂ : 0 •> m₁ = 0
⊢ 0 •> m₂ + m₁ <• 0 = 0
have rw₃ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [zero_smul, zero_add, op_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : MonoidWithZero R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
m : M
⊢ r •> m + 0 •> 0 = r •> m
have rw : r •> m + 0 = r •> m
Tactic: rw [smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : MonoidWithZero R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
m : M
rw : r •> m + 0 = r •> m
⊢ r •> m + 0 •> 0 = r •> m
have rw₁ : r •> m = r •> m
Tactic: rw [smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : MonoidWithZero R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
m : M
⊢ 0 •> 0 + m <• r = m <• r
have rw : 0 + m <• r = m <• r
Tactic: rw [smul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : MonoidWithZero R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
m : M
rw : 0 + m <• r = m <• r
⊢ 0 •> 0 + m <• r = m <• r
have rw₁ : m <• r = m <• r
Tactic: rw [smul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ (inl r * x).snd = (r •> x).snd
have dsimp : r •> x.snd + 0 <• x.fst = r •> x.snd
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ r •> x.snd + 0 <• x.fst = r •> x.snd
have rw : r •> x.snd + 0 = r •> x.snd
Tactic: rw [smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
r : R
x : tsze R M
rw : r •> x.snd + 0 = r •> x.snd
⊢ r •> x.snd + 0 <• x.fst = r •> x.snd
have rw₁ : r •> x.snd = r •> x.snd
Tactic: rw [smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
r : R
⊢ (x * inl r).snd = (x <• r).snd
have dsimp : x.fst •> 0 + x.snd <• r = x.snd <• r
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
r : R
⊢ x.fst •> 0 + x.snd <• r = x.snd <• r
have rw : 0 + x.snd <• r = x.snd <• r
Tactic: rw [smul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
r : R
rw : 0 + x.snd <• r = x.snd <• r
⊢ x.fst •> 0 + x.snd <• r = x.snd <• r
have rw₁ : x.snd <• r = x.snd <• r
Tactic: rw [smul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
⊢ 1 •> x.2 + 0 <• x.1 = x.2
have rw : x.2 + 0 <• x.1 = x.2
Tactic: rw [one_smul, smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : x.2 + 0 <• x.1 = x.2
⊢ 1 •> x.2 + 0 <• x.1 = x.2
have rw₁ : x.2 + 0 = x.2
Tactic: rw [one_smul, smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : x.2 + 0 <• x.1 = x.2
rw₁ : x.2 + 0 = x.2
⊢ 1 •> x.2 + 0 <• x.1 = x.2
have rw₂ : x.2 = x.2
Tactic: rw [one_smul, smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
⊢ x.1 •> 0 + x.2 <• 1 = x.2
have rw : 0 + x.2 <• 1 = x.2
Tactic: rw [smul_zero, zero_add, op_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + x.2 <• 1 = x.2
⊢ x.1 •> 0 + x.2 <• 1 = x.2
have rw₁ : x.2 <• 1 = x.2
Tactic: rw [smul_zero, zero_add, op_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + x.2 <• 1 = x.2
rw₁ : x.2 <• 1 = x.2
⊢ x.1 •> 0 + x.2 <• 1 = x.2
have rw₂ : 1 •> x.2 = x.2
Tactic: rw [smul_zero, zero_add, op_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + x.2 <• 1 = x.2
rw₁ : x.2 <• 1 = x.2
rw₂ : 1 •> x.2 = x.2
⊢ x.1 •> 0 + x.2 <• 1 = x.2
have rw₃ : x.2 = x.2
Tactic: rw [smul_zero, zero_add, op_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddMonoidWithOne R
inst_1 : AddMonoid M
x : ℕ
⊢ inl (↑(x + 1) : R) = HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1
have h1 : fst.{u, v} (M := M) (inl (↑(x + 1) : R)) = (HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1).fst
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : AddMonoidWithOne R
inst_1 : AddMonoid M
x : ℕ
h1 : fst.{u, v} (M := M) (inl (↑(x + 1) : R)) = (HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1).fst
⊢ inl (↑(x + 1) : R) = HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1
have h2 : snd.{u, v} (R := R) (inl (↑(x + 1) : R)) = (HAdd.hAdd (α := tsze R M) (inl (↑x : R)) 1).snd
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x₁ x₂ x₃ : tsze R M
⊢ x₁.1 •> (x₂.2 + x₃.2) + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
have simp_rw : x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
Tactic: simp_rw [smul_add, MulOpposite.op_add, add_smul, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x₁ x₂ x₃ : tsze R M
simp_rw :
  x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
⊢ x₁.1 •> (x₂.2 + x₃.2) + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
have simp_rw₁ : x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + (op x₂.1 + op x₃.1) •> x₁.2 = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
Tactic: simp_rw [smul_add, MulOpposite.op_add, add_smul, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x₁ x₂ x₃ : tsze R M
simp_rw :
  x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
simp_rw₁ :
  x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + (op x₂.1 + op x₃.1) •> x₁.2 =
    x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
⊢ x₁.1 •> (x₂.2 + x₃.2) + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
have simp_rw₂ : x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + (x₁.2 <• x₂.1 + x₁.2 <• x₃.1) =
  x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
Tactic: simp_rw [smul_add, MulOpposite.op_add, add_smul, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x₁ x₂ x₃ : tsze R M
⊢ (x₁.1 + x₂.1) •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
have simp_rw : x₁.1 •> x₃.2 + x₂.1 •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
Tactic: simp_rw [add_smul, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x₁ x₂ x₃ : tsze R M
simp_rw :
  x₁.1 •> x₃.2 + x₂.1 •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
⊢ (x₁.1 + x₂.1) •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
have simp_rw₁ : x₁.1 •> x₃.2 + x₂.1 •> x₃.2 + (x₁.2 <• x₃.1 + x₂.2 <• x₃.1) =
  x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
Tactic: simp_rw [add_smul, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x : tsze R M
⊢ 0 •> x.2 + 0 <• x.1 = 0
have rw : 0 + 0 <• x.1 = 0
Tactic: rw [zero_smul, zero_add, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + 0 <• x.1 = 0
⊢ 0 •> x.2 + 0 <• x.1 = 0
have rw₁ : 0 <• x.1 = 0
Tactic: rw [zero_smul, zero_add, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + 0 <• x.1 = 0
rw₁ : 0 <• x.1 = 0
⊢ 0 •> x.2 + 0 <• x.1 = 0
have rw₂ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [zero_smul, zero_add, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x : tsze R M
⊢ x.1 •> 0 + 0 •> x.2 = 0
have rw : 0 + 0 •> x.2 = 0
Tactic: rw [smul_zero, zero_add, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + 0 •> x.2 = 0
⊢ x.1 •> 0 + 0 •> x.2 = 0
have rw₁ : 0 •> x.2 = 0
Tactic: rw [smul_zero, zero_add, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + 0 •> x.2 = 0
rw₁ : 0 •> x.2 = 0
⊢ x.1 •> 0 + 0 •> x.2 = 0
have rw₂ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [smul_zero, zero_add, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd
have succ : x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd
Tactic: rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
succ : x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd
have succ₁ : (op x.fst * op (x.fst ^ n)) •> x.snd = (x.fst ^ n * x.fst) •> x.snd
Tactic: rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
succ : x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd
succ₁ : (op x.fst * op (x.fst ^ n)) •> x.snd = (x.fst ^ n * x.fst) •> x.snd
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd
have succ₂ : x.snd <• x.fst ^ n <• x.fst = (x.fst ^ n * x.fst) •> x.snd
Tactic: rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
succ : x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd
succ₁ : (op x.fst * op (x.fst ^ n)) •> x.snd = (x.fst ^ n * x.fst) •> x.snd
succ₂ : x.snd <• x.fst ^ n <• x.fst = (x.fst ^ n * x.fst) •> x.snd
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd
have succ₃ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> x.fst •> x.snd
Tactic: rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
succ : x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd
succ₁ : (op x.fst * op (x.fst ^ n)) •> x.snd = (x.fst ^ n * x.fst) •> x.snd
succ₂ : x.snd <• x.fst ^ n <• x.fst = (x.fst ^ n * x.fst) •> x.snd
succ₃ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> x.fst •> x.snd
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd
have succ₄ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> (x.snd <• x.fst)
Tactic: rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
succ : x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd
succ₁ : (op x.fst * op (x.fst ^ n)) •> x.snd = (x.fst ^ n * x.fst) •> x.snd
succ₂ : x.snd <• x.fst ^ n <• x.fst = (x.fst ^ n * x.fst) •> x.snd
succ₃ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> x.fst •> x.snd
succ₄ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> (x.snd <• x.fst)
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd
have succ₅ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> x.snd <• x.fst
Tactic: rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
succ : x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd
succ₁ : (op x.fst * op (x.fst ^ n)) •> x.snd = (x.fst ^ n * x.fst) •> x.snd
succ₂ : x.snd <• x.fst ^ n <• x.fst = (x.fst ^ n * x.fst) •> x.snd
succ₃ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> x.fst •> x.snd
succ₄ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> (x.snd <• x.fst)
succ₅ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> x.snd <• x.fst
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd
have succ₆ : x.fst ^ n •> x.snd <• x.fst = x.fst ^ n •> x.snd <• x.fst
Tactic: rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
have zero : x.snd <• HPow.hPow (β := ℕ) x.fst 0 = HPow.hPow (β := ℕ) x.fst 0 •> x.snd
Tactic: induction n with
    | zero => simp
    | succ n ih =>
      rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
Cleared hypotheses: n