awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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)
r : R
algebraMap₁ : motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) 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:
rw [AlgHom.commutes]

Premises used: AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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)
r : R
⊢ motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)

Tactic:
algebraMap r
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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)
r : R
⊢ motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)

Tactic:
exact algebraMap r
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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 : M
⊢ motive
    ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x))

Tactic:
ι x
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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 : M
⊢ motive
    ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x))

Tactic:
exact ι x
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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)
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))
⊢ motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) (x * y))

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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
    (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:
mul _ _ hx hy
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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
    (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:
exact mul _ _ hx hy
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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)
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))
⊢ motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) (x + y))

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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
    (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:
add _ _ hx hy
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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
    (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:
exact add _ _ hx hy
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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))
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))
⊢ motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) a)

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

Premises used: map_add, map_mul, AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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
r : R
⊢ Commute a ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)

Tactic:
Algebra.commute_algebraMap_right _ _

Premises used: Algebra.commute_algebraMap_right
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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
r : R
⊢ Commute a ((algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)

Tactic:
exact Algebra.commute_algebraMap_right _ _

Premises used: Algebra.commute_algebraMap_right
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module 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)
    ((ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)

Tactic:
Algebra.commute_algebraMap_left _ _

Premises used: Algebra.commute_algebraMap_left
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module 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)
    ((ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)

Tactic:
exact Algebra.commute_algebraMap_left _ _

Premises used: Algebra.commute_algebraMap_left
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
⊢ Commute (S := SymmetricAlgebra R M) ((ι R M : (a : M) → SymmetricAlgebra R M) y : SymmetricAlgebra R M)
    ((ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M)

Tactic:
simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]

Premises used: TensorAlgebra.SymRel.mul_comm, commute_iff_eq, SymmetricAlgebra.ι, map_mul, RingQuot.mkAlgHom_rel
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
a b : SymmetricAlgebra R M
ha : Commute a ((ι R M : (a : M) → SymmetricAlgebra R M) x)
hb : Commute b ((ι R M : (a : M) → SymmetricAlgebra R M) x)
⊢ Commute (a * b) ((ι R M : (a : M) → SymmetricAlgebra R M) x)

Tactic:
ha.mul_left hb

Premises used: Commute.mul_left
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
a b : SymmetricAlgebra R M
ha : Commute a ((ι R M : (a : M) → SymmetricAlgebra R M) x)
hb : Commute b ((ι R M : (a : M) → SymmetricAlgebra R M) x)
⊢ Commute (a * b) ((ι R M : (a : M) → SymmetricAlgebra R M) x)

Tactic:
exact ha.mul_left hb

Premises used: Commute.mul_left
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
a b : SymmetricAlgebra R M
ha : Commute a ((ι R M : (a : M) → SymmetricAlgebra R M) x)
hb : Commute b ((ι R M : (a : M) → SymmetricAlgebra R M) x)
⊢ Commute (a + b) ((ι R M : (a : M) → SymmetricAlgebra R M) x)

Tactic:
ha.add_left hb

Premises used: Commute.add_left
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
a b : SymmetricAlgebra R M
ha : Commute a ((ι R M : (a : M) → SymmetricAlgebra R M) x)
hb : Commute b ((ι R M : (a : M) → SymmetricAlgebra R M) x)
⊢ Commute (a + b) ((ι R M : (a : M) → SymmetricAlgebra R M) x)

Tactic:
exact ha.add_left hb

Premises used: Commute.add_left
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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)
ι₃ :
  ∀ (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)

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

Premises used: Algebra.algebraMap, commute_iff_eq, SymmetricAlgebra.ι, map_mul, Algebra.commute_algebraMap_left
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b c : SymmetricAlgebra R M
hb : Commute a b
hc : Commute a c
⊢ Commute a (b * c)

Tactic:
hb.mul_right hc

Premises used: Commute.mul_right
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b c : SymmetricAlgebra R M
hb : Commute a b
hc : Commute a c
⊢ Commute a (b * c)

Tactic:
exact hb.mul_right hc

Premises used: Commute.mul_right
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b c : SymmetricAlgebra R M
hb : Commute a b
hc : Commute a c
⊢ Commute a (b + c)

Tactic:
hb.add_right hc

Premises used: Commute.add_right
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b c : SymmetricAlgebra R M
hb : Commute a b
hc : Commute a c
⊢ Commute a (b + c)

Tactic:
exact hb.add_right hc

Premises used: Commute.add_right
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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)
add : ∀ (b c : SymmetricAlgebra R M) (hb : Commute a b) (hc : Commute a c), Commute a (b + c)
⊢ Commute a b

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

Premises used: Algebra.algebraMap, commute_iff_eq, SymmetricAlgebra.ι, map_mul, Algebra.commute_algebraMap_left, Algebra.commute_algebraMap_right
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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
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)
⊢ (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) }

Tactic:
refine (Equiv.subtypeUnivEquiv fun h _ _ h' ↦ ?_).symm

Premises used: Equiv.subtypeUnivEquiv, Equiv.symm
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
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)
mul_comm₂ 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)
⊢ 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)

Tactic:
rw [map_mul, map_mul, mul_comm]

Premises used: map_mul, mul_comm