awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
a : ⨂[R]^n M
smul_tprod :
  ∀ (r : R) (a : (i : Fin n) → M),
    (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
        ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
          (HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
              ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a :
                ⨂[R] (i : Fin n), M) ⊗ₜ[R]
            (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
      HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
        ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a : ⨂[R] (i : Fin n), M)
add :
  ∀ (x y : ⨂[R] (i : Fin n), M)
    (hx :
      (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (x ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
        x)
    (hy :
      (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (y ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
        y),
    (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
        ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
          ((x + y) ⊗ₜ[R]
            (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
      x + y
⊢ (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        (a ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
    a

Tactic:
induction a using PiTensorProduct.induction_on with
  | smul_tprod r a =>
    rw [← TensorProduct.smul_tmul', map_smul, map_smul, ← gMul_def, tprod_mul_tprod R a _,
      cast_tprod]
    simp
  | add x y hx hy =>
    rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]

Premises used: map_add, TensorPower.tprod_mul_tprod, TensorPower.gMul_def, TensorProduct.smul_tmul', TensorPower.cast_tprod, TensorProduct.add_tmul, map_smul
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb nc : ℕ
a : ⨂[R]^na M
b : ⨂[R]^nb M
c : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun (n m : ℕ) ↦
    LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M))
      (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M)
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
        (a : ⨂[R]^(na + nb) M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →
          (⨂[R]^nb M →ₗ[R] ⨂[R]^(na + nb) M) →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
      (LinearMap.compr₂ (mul (na + nb) nc) (↑e : ⨂[R]^(na + nb + nc) M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ∘ₗ
    mul na nb
⊢ ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    Eq (α := ⨂[R]^(na + (nb + nc)) M)
      ((((((lhs : (a : ⨂[R]^na M) → ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) a :
                    ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
                  (a : ⨂[R]^nb M) → ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
                b :
              ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
            (a : ⨂[R]^nc M) → ⨂[R]^(na + (nb + nc)) M)
          c :
        ⨂[R]^(na + (nb + nc)) M)
      ((e : (a : ⨂[R]^(na + nb + nc) M) → ⨂[R]^(na + (nb + nc)) M)
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (na + nb) _
            (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ _ a b) c) :
        ⨂[R]^(na + (nb + nc)) M)

Tactic:
have lhs_eq : ∀ a b c, lhs a b c = e (a ₜ* b ₜ* c) := fun _ _ _ => rfl
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
⊢ HSMul.hSMul (β := ⨂[R] (i : Fin 0), M) r
      ((tprod R (s := fun (x : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M)
        (isEmptyElim (p := fun (x : Fin 0) ↦ M))) =
    HSMul.hSMul (β := ⨂[R]^0 M) r (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := ⨂[R]^0 M) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) 1 : ⨂[R]^0 M)
    (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)

Tactic:
(algebraMap₀_eq_smul_one 1).trans (one_smul _ _)

Premises used: TensorPower.algebraMap₀_eq_smul_one, one_smul, OfNat.ofNat, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
rw₁ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              (HSMul.hSMul (β := ⨂[R]^0 M) r
                (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
rw₂ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (HSMul.hSMul (β := ⨂[R]^(0 + n) M) r
        ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                      (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                    (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
                  (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
                ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
              (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            a :
          ⨂[R]^(0 + n) M)) =
    r • a
rw₃ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                      (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                    (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
                  (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
                ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
              (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            a) :
        ⨂[R]^n M) =
    r • a
rw₄ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _
            (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) a) :
        ⨂[R]^n M) =
    r • a
rw₅ rw₆ : r • a = r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _ ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) a) =
    r • a

Tactic:
rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂, map_smul,
    ← gMul_eq_coe_linearMap, one_mul]

Premises used: TensorPower.gMul_eq_coe_linearMap, TensorPower.algebraMap₀_eq_smul_one, LinearMap.map_smul₂, TensorPower.one_mul, map_smul
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                  (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
              a :
            ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
          (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
    r • a
rw₁ :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                  (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
              a :
            ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
          (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        (HSMul.hSMul (β := ⨂[R]^0 M) r
          (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M))) =
    r • a
rw₂ :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      (HSMul.hSMul (β := ⨂[R]^(n + 0) M) r
        ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                      (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                    (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
                  a :
                ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
              (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
          ⨂[R]^(n + 0) M)) =
    r • a
rw₃ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
          ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                      (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                    (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
                  a :
                ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
              (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _)) :
        ⨂[R]^n M) =
    r • a
rw₄ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ 0 a
            (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _)) :
        ⨂[R]^n M) =
    r • a
rw₅ rw₆ : r • a = r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ 0 a ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
    r • a

Tactic:
rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, map_smul, map_smul, ← gMul_eq_coe_linearMap,
    mul_one]

Premises used: TensorPower.gMul_eq_coe_linearMap, TensorPower.algebraMap₀_eq_smul_one, TensorPower.mul_one, map_smul
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
rw :
  (cast R M ⋯ : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) =
    HSMul.hSMul (β := ⨂[R]^0 M) r ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s : ⨂[R]^0 M)
⊢ Eq (α := ⨂[R]^0 M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) :
      ⨂[R]^0 M)
    ((algebraMap₀ : (a : R) → ⨂[R]^0 M) (r * s) : ⨂[R]^0 M)

Tactic:
rw [← smul_eq_mul, map_smul]

Premises used: smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) =
    HSMul.hSMul (β := ⨂[R]^0 M) r ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s : ⨂[R]^0 M)

Tactic:
algebraMap₀_mul r (@algebraMap₀ R M _ _ _ s)

Premises used: TensorPower.algebraMap₀_mul, TensorPower.algebraMap₀, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) =
    HSMul.hSMul (β := ⨂[R]^0 M) r ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s : ⨂[R]^0 M)

Tactic:
exact algebraMap₀_mul r (@algebraMap₀ R M _ _ _ s)

Premises used: TensorPower.algebraMap₀_mul, TensorPower.algebraMap₀, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := ⨂[R]^0 M) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) (↑0 : R)) 0

Tactic:
simp only [Nat.cast_zero, map_zero]

Premises used: map_zero, Nat.cast_zero
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
⊢ (algebraMap₀ : (a : R) → ⨂[R]^0 M) (↑(n + 1) : R) =
    HAdd.hAdd (α := ⨂[R]^0 M) (β := ⨂[R]^0 M) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) (↑n : R) : ⨂[R]^0 M)
      (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) AddZero.toZero _ : ⨂[R]^0 M)

Tactic:
simp only [Nat.cast_succ, map_add, algebraMap₀_one]

Premises used: Nat.cast_succ, TensorPower.algebraMap₀_one, map_add
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Semiring (⨁ (n : ℕ), ⨂[R]^n M)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
⊢ Eq (α := ⨂[R]^0 M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) :
      ⨂[R]^0 M)
    ((algebraMap₀ : (a : R) → ⨂[R]^0 M) (r * s) : ⨂[R]^0 M)

Tactic:
have := algebraMap₀_mul_algebraMap₀ (M := M) r s
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
this :
  Eq (α := ⨂[R]^0 M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) :
      ⨂[R]^0 M)
    ((algebraMap₀ : (a : R) → ⨂[R]^0 M) (r * s) : ⨂[R]^0 M)
⊢ Eq (α :=
    ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))
      M)
    (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
        (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
          ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))) :
      ⨂[R] (x :
        Fin
          (Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))),
        M)
    ((LinearEquiv.symm (cast R M ⋯) :
          (a :
              ⨂[R]^(GradedMonoid.mk (0 + 0)
                      (GradedMonoid.GMul.mul (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)
                        (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) s))).fst
                M) →
            ⨂[R]^(GradedMonoid.mk 0
                    (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) (r * s))).fst
              M)
        (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) (HAdd.hAdd (α := ℕ) 0 0)
            (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) AddSemigroup.toAdd _ 0 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) s)))) :
      ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))
        M)

Tactic:
this.symm

Premises used: Fin.natAdd, Quotient.liftOn', AddCon.liftOn, List.foldl, PiTensorProduct.tprodCoeff, Eq.symm, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
this :
  Eq (α := ⨂[R]^0 M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) :
      ⨂[R]^0 M)
    ((algebraMap₀ : (a : R) → ⨂[R]^0 M) (r * s) : ⨂[R]^0 M)
⊢ Eq (α :=
    ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))
      M)
    (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
        (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
          ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))) :
      ⨂[R] (x :
        Fin
          (Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))),
        M)
    ((LinearEquiv.symm (cast R M ⋯) :
          (a :
              ⨂[R]^(GradedMonoid.mk (0 + 0)
                      (GradedMonoid.GMul.mul (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)
                        (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) s))).fst
                M) →
            ⨂[R]^(GradedMonoid.mk 0
                    (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) (r * s))).fst
              M)
        (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) (HAdd.hAdd (α := ℕ) 0 0)
            (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) AddSemigroup.toAdd _ 0 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) s)))) :
      ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))
        M)

Tactic:
exact this.symm

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
⊢ Eq (α := ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + x.fst) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M))) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
          (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)

Tactic:
have := (algebraMap₀_mul r x.snd).trans (mul_algebraMap₀ r x.snd).symm
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
this :
  Eq (α := ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + x.fst) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M))) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
          (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
rw :
  (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
          x).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) =
    (cast R M ⋯ :
        (a :
            ⨂[R]^(x * GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)).fst
              M) →
          ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
            M)
      ((x *
            GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))
⊢ (cast R M ⋯ :
        (a :
            ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
              M) →
          ⨂[R]^(x * GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)).fst
            M)
      ((GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
            x).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    (x *
          GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)

Tactic:
rw [← LinearEquiv.eq_symm_apply, cast_symm]

Premises used: LinearEquiv.eq_symm_apply, TensorPower.cast_symm