awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
x y : TensorAlgebra R M
hx : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) x)
hy : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) y)
⊢ motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) (x * y))
have mul₁ : motive
  (HMul.hMul (α := SymmetricAlgebra R M) (β := SymmetricAlgebra R M)
    ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
    ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) y : SymmetricAlgebra R M))
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
x y : TensorAlgebra R M
hx : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) x)
hy : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) y)
⊢ motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) (x + y))
have add₁ : motive
  (HAdd.hAdd (α := SymmetricAlgebra R M) (β := SymmetricAlgebra R M)
    ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
    ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) y : SymmetricAlgebra R M))
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
a : TensorAlgebra R M
⊢ motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) a)
have algebraMap₁ : ∀ (r : R),
  motive
    ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
      ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r))
Tactic: induction a using TensorAlgebra.induction with
  | algebraMap r => rw [AlgHom.commutes]; exact algebraMap r
  | ι x => exact ι x
  | mul x y hx hy => rw [map_mul]; exact mul _ _ hx hy
  | add x y hx hy => rw [map_add]; exact add _ _ hx hy
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
a : TensorAlgebra R M
algebraMap₁ :
  ∀ (r : R),
    motive
      ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
        ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r))
⊢ motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) a)
have ι₁ : ∀ (x : M),
  motive
    ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x))
Tactic: induction a using TensorAlgebra.induction with
  | algebraMap r => rw [AlgHom.commutes]; exact algebraMap r
  | ι x => exact ι x
  | mul x y hx hy => rw [map_mul]; exact mul _ _ hx hy
  | add x y hx hy => rw [map_add]; exact add _ _ hx hy
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
a : TensorAlgebra R M
algebraMap₁ :
  ∀ (r : R),
    motive
      ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
        ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r))
ι₁ :
  ∀ (x : M),
    motive
      ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
        ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x))
⊢ motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) a)
have mul₁ : ∀ (x y : TensorAlgebra R M) (hx : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) x))
  (hy : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) y)),
  motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) (x * y))
Tactic: induction a using TensorAlgebra.induction with
  | algebraMap r => rw [AlgHom.commutes]; exact algebraMap r
  | ι x => exact ι x
  | mul x y hx hy => rw [map_mul]; exact mul _ _ hx hy
  | add x y hx hy => rw [map_add]; exact add _ _ hx hy
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
a : TensorAlgebra R M
algebraMap₁ :
  ∀ (r : R),
    motive
      ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
        ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r))
ι₁ :
  ∀ (x : M),
    motive
      ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
        ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x))
mul₁ :
  ∀ (x y : TensorAlgebra R M) (hx : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) x))
    (hy : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) y)),
    motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) (x * y))
⊢ motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) a)
have add₁ : ∀ (x y : TensorAlgebra R M) (hx : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) x))
  (hy : motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) y)),
  motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) (x + y))
Tactic: induction a using TensorAlgebra.induction with
  | algebraMap r => rw [AlgHom.commutes]; exact algebraMap r
  | ι x => exact ι x
  | mul x y hx hy => rw [map_mul]; exact mul _ _ hx hy
  | add x y hx hy => rw [map_add]; exact add _ _ hx hy
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : SymmetricAlgebra R M
x : M
⊢ Commute a ((ι R M : (a : M) → SymmetricAlgebra R M) x)
have ι : ∀ (r : R),
  Commute (S := SymmetricAlgebra R M)
    ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r : SymmetricAlgebra R M)
    ((ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
Tactic: induction a using SymmetricAlgebra.induction with
      | algebraMap r => exact Algebra.commute_algebraMap_left _ _
      | ι y => simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]
      | mul a b ha hb => exact ha.mul_left hb
      | add a b ha hb => exact ha.add_left hb
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : SymmetricAlgebra R M
x : M
ι :
  ∀ (r : R),
    Commute (S := SymmetricAlgebra R M)
      ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r : SymmetricAlgebra R M)
      ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
⊢ Commute a ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
have ι₁ : ∀ (y : M),
  Commute (S := SymmetricAlgebra R M)
    ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) y : SymmetricAlgebra R M)
    ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
Tactic: induction a using SymmetricAlgebra.induction with
      | algebraMap r => exact Algebra.commute_algebraMap_left _ _
      | ι y => simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]
      | mul a b ha hb => exact ha.mul_left hb
      | add a b ha hb => exact ha.add_left hb
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : SymmetricAlgebra R M
x : M
ι :
  ∀ (r : R),
    Commute (S := SymmetricAlgebra R M)
      ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r : SymmetricAlgebra R M)
      ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
ι₁ :
  ∀ (y : M),
    Commute (S := SymmetricAlgebra R M)
      ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) y : SymmetricAlgebra R M)
      ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
⊢ Commute a ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
have ι₂ : ∀ (a b : SymmetricAlgebra R M) (ha : Commute a ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x))
  (hb : Commute b ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)),
  Commute (a * b) ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
Tactic: induction a using SymmetricAlgebra.induction with
      | algebraMap r => exact Algebra.commute_algebraMap_left _ _
      | ι y => simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]
      | mul a b ha hb => exact ha.mul_left hb
      | add a b ha hb => exact ha.add_left hb
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : SymmetricAlgebra R M
x : M
ι :
  ∀ (r : R),
    Commute (S := SymmetricAlgebra R M)
      ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r : SymmetricAlgebra R M)
      ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
ι₁ :
  ∀ (y : M),
    Commute (S := SymmetricAlgebra R M)
      ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) y : SymmetricAlgebra R M)
      ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)
ι₂ :
  ∀ (a b : SymmetricAlgebra R M) (ha : Commute a ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x))
    (hb : Commute b ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)),
    Commute (a * b) ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
⊢ Commute a ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
have ι₃ : ∀ (a b : SymmetricAlgebra R M) (ha : Commute a ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x))
  (hb : Commute b ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)),
  Commute (a + b) ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
Tactic: induction a using SymmetricAlgebra.induction with
      | algebraMap r => exact Algebra.commute_algebraMap_left _ _
      | ι y => simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]
      | mul a b ha hb => exact ha.mul_left hb
      | add a b ha hb => exact ha.add_left hb
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : SymmetricAlgebra R M
⊢ Commute a b
have algebraMap : ∀ (r : R), Commute a ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
Tactic: induction b using SymmetricAlgebra.induction with
    | algebraMap r => exact Algebra.commute_algebraMap_right _ _
    | ι x => induction a using SymmetricAlgebra.induction with
      | algebraMap r => exact Algebra.commute_algebraMap_left _ _
      | ι y => simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]
      | mul a b ha hb => exact ha.mul_left hb
      | add a b ha hb => exact ha.add_left hb
    | mul b c hb hc => exact hb.mul_right hc
    | add b c hb hc => exact hb.add_right hc
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : SymmetricAlgebra R M
algebraMap : ∀ (r : R), Commute a ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
⊢ Commute a b
have ι : ∀ (x : M), Commute a ((ι R M : (a : M) → SymmetricAlgebra R M) x)
Tactic: induction b using SymmetricAlgebra.induction with
    | algebraMap r => exact Algebra.commute_algebraMap_right _ _
    | ι x => induction a using SymmetricAlgebra.induction with
      | algebraMap r => exact Algebra.commute_algebraMap_left _ _
      | ι y => simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]
      | mul a b ha hb => exact ha.mul_left hb
      | add a b ha hb => exact ha.add_left hb
    | mul b c hb hc => exact hb.mul_right hc
    | add b c hb hc => exact hb.add_right hc
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : SymmetricAlgebra R M
algebraMap : ∀ (r : R), Commute a ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
ι : ∀ (x : M), Commute a ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
⊢ Commute a b
have mul : ∀ (b c : SymmetricAlgebra R M) (hb : Commute a b) (hc : Commute a c), Commute a (b * c)
Tactic: induction b using SymmetricAlgebra.induction with
    | algebraMap r => exact Algebra.commute_algebraMap_right _ _
    | ι x => induction a using SymmetricAlgebra.induction with
      | algebraMap r => exact Algebra.commute_algebraMap_left _ _
      | ι y => simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]
      | mul a b ha hb => exact ha.mul_left hb
      | add a b ha hb => exact ha.add_left hb
    | mul b c hb hc => exact hb.mul_right hc
    | add b c hb hc => exact hb.add_right hc
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : SymmetricAlgebra R M
algebraMap : ∀ (r : R), Commute a ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
ι : ∀ (x : M), Commute a ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
mul : ∀ (b c : SymmetricAlgebra R M) (hb : Commute a b) (hc : Commute a c), Commute a (b * c)
⊢ Commute a b
have add : ∀ (b c : SymmetricAlgebra R M) (hb : Commute a b) (hc : Commute a c), Commute a (b + c)
Tactic: induction b using SymmetricAlgebra.induction with
    | algebraMap r => exact Algebra.commute_algebraMap_right _ _
    | ι x => induction a using SymmetricAlgebra.induction with
      | algebraMap r => exact Algebra.commute_algebraMap_left _ _
      | ι y => simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]
      | mul a b ha hb => exact ha.mul_left hb
      | add a b ha hb => exact ha.add_left hb
    | mul b c hb hc => exact hb.mul_right hc
    | add b c hb hc => exact hb.add_right hc
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
⊢ (TensorAlgebra R M →ₐ[R] A) ≃
    { f : TensorAlgebra R M →ₐ[R] A //
      ∀ {x y : TensorAlgebra R M},
        SymRel R M x y →
          Eq.{u_3 + 1} (α := A) ((f : (a : TensorAlgebra R M) → A) x : A) ((f : (a : TensorAlgebra R M) → A) y : A) }
have refine : ∀ (h : TensorAlgebra R M →ₐ[R] A) (x x_1 : TensorAlgebra R M) (h' : SymRel R M x x_1),
  Eq.{u_3 + 1} (α := A) ((h : (a : TensorAlgebra R M) → A) x : A) ((h : (a : TensorAlgebra R M) → A) x_1 : A)
Tactic: refine (Equiv.subtypeUnivEquiv fun h _ _ h' ↦ ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
h : TensorAlgebra R M →ₐ[R] A
x_1 x_2 : TensorAlgebra R M
x y : M
⊢ Eq.{u_3 + 1} (α := A)
    ((h : (a : TensorAlgebra R M) → A)
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)) :
      A)
    ((h : (a : TensorAlgebra R M) → A)
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)) :
      A)
have mul_comm : HMul.hMul (α := A) (β := A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) : A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) : A) =
  (h : (a : TensorAlgebra R M) → A)
    (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M))
Tactic: rw [map_mul, map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
h : TensorAlgebra R M →ₐ[R] A
x_1 x_2 : TensorAlgebra R M
x y : M
mul_comm :
  HMul.hMul (α := A) (β := A)
      ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) : A)
      ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) :
        A) =
    (h : (a : TensorAlgebra R M) → A)
      (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
        ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)
        ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M))
⊢ Eq.{u_3 + 1} (α := A)
    ((h : (a : TensorAlgebra R M) → A)
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)) :
      A)
    ((h : (a : TensorAlgebra R M) → A)
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)) :
      A)
have mul_comm₁ : HMul.hMul (α := A) (β := A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) : A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) : A) =
  HMul.hMul (α := A) (β := A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) : A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) : A)
Tactic: rw [map_mul, map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
h : TensorAlgebra R M →ₐ[R] A
x_1 x_2 : TensorAlgebra R M
x y : M
mul_comm :
  HMul.hMul (α := A) (β := A)
      ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) : A)
      ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) :
        A) =
    (h : (a : TensorAlgebra R M) → A)
      (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
        ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)
        ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M))
mul_comm₁ :
  HMul.hMul (α := A) (β := A)
      ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) : A)
      ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) :
        A) =
    HMul.hMul (α := A) (β := A)
      ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) : A)
      ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((h : (a : TensorAlgebra R M) → A)
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)) :
      A)
    ((h : (a : TensorAlgebra R M) → A)
        (HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M)
          ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)) :
      A)
have mul_comm₂ : HMul.hMul (α := A) (β := A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) : A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) : A) =
  HMul.hMul (α := A) (β := A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) : A)
    ((h : (a : TensorAlgebra R M) → A) ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) : A)
Tactic: rw [map_mul, map_mul, mul_comm]