awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
rw :
  Eq (α := TensorAlgebra R M)
    ((toTensorAlgebra : (a : ⨂[R]^0 M) → TensorAlgebra R M) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) : TensorAlgebra R M)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
rw₁ :
  Eq (α := TensorAlgebra R M)
    ((toTensorAlgebra : (a : ⨂[R]^0 M) → TensorAlgebra R M)
        (HSMul.hSMul (β := ⨂[R]^0 M) r
          (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)) :
      TensorAlgebra R M)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
rw₂ :
  HSMul.hSMul (β := TensorAlgebra R M) r
      ((toTensorAlgebra : (a : ⨂[R]^0 M) → TensorAlgebra R M)
          (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
        TensorAlgebra R M) =
    (algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r
rw₃ : HSMul.hSMul (β := TensorAlgebra R M) r 1 = (algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r
rw₄ rw₅ : HSMul.hSMul (β := TensorAlgebra R M) r 1 = HSMul.hSMul (β := TensorAlgebra R M) r 1
⊢ Eq (α := TensorAlgebra R M)
    ((toTensorAlgebra : (a : ⨂[R]^0 M) → TensorAlgebra R M)
        (((@DirectSum.GAlgebra.toFun _ R (fun (n : ℕ) ↦ ⨂[R]^n M) inst
                (fun (i : ℕ) ↦ PiTensorProduct.instAddCommMonoid fun (x : Fin i) ↦ M)
                (fun (i : ℕ) ↦ PiTensorProduct.instModule (s := fun (x : Fin i) ↦ M)) Nat.instAddMonoid gsemiring _ :
              R →+ ⨂[R]^0 M) :
            (a : R) → ⨂[R]^0 M)
          r) :
      TensorAlgebra R M)
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)

Tactic:
rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, map_smul,
    TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]

Premises used: TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, Algebra.algebraMap_eq_smul_one, TensorPower.toTensorAlgebra_gOne, map_smul
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
⊢ Eq (α := TensorAlgebra R M)
    ((ofDirectSum : (a : ⨁ (n : ℕ), ⨂[R]^n M) → TensorAlgebra R M)
        (((DirectSum.of (fun (n : ℕ) ↦ ⨂[R]^n M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
            (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
          ((PiTensorProduct.tprod R (s := fun (a : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x)) :
      TensorAlgebra R M)
    ((tprod R M n : (a : (i : Fin n) → M) → TensorAlgebra R M) x : TensorAlgebra R M)

Tactic:
(DirectSum.toAddMonoid_of
    (fun _ ↦ LinearMap.toAddMonoidHom TensorPower.toTensorAlgebra) _ _).trans
  (TensorPower.toTensorAlgebra_tprod _)

Premises used: LinearMap.toAddMonoidHom, Multiset.sum, Multiset.foldr, Function.update, addConGen, Quotient.liftOn', AddCon.liftOn, List.map, TensorPower.toTensorAlgebra, Pi.single, dite, Quotient, PiTensorProduct, AddCon.Quotient, List.foldr, DirectSum.toAddMonoid_of, Finset.sum, FreeAddMonoid, TensorPower.toTensorAlgebra_tprod, Eq.trans, Trunc.lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
    ((toDirectSum : (a : TensorAlgebra R M) → ⨁ (n : ℕ), ⨂[R]^n M) ((ι R : (a : M) → TensorAlgebra R M) x) :
      ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (n : ℕ) ↦ ⨂[R]^n M) 1 : ⨂[R]^1 M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^1 M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
          fun (x_1 : Fin 1) ↦ x) :
      ⨁ (i : ℕ), ⨂[R]^i M)

Tactic:
simp [toDirectSum, TensorAlgebra.lift_ι_apply, DirectSum.lof_eq_of]

Premises used: TensorAlgebra.toDirectSum, TensorAlgebra.lift_ι_apply, DirectSum.lof_eq_of
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
w :
  ∀ (x : M),
    Eq (α := TensorAlgebra R M)
      ((AlgHom.toLinearMap (AlgHom.comp ofDirectSum toDirectSum) ∘ₗ ι R : (a : M) → TensorAlgebra R M) x :
        TensorAlgebra R M)
      ((AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M)) ∘ₗ ι R : (a : M) → TensorAlgebra R M) x :
        TensorAlgebra R M)
⊢ Eq (α := TensorAlgebra R M →ₐ[R] TensorAlgebra R M) (AlgHom.comp ofDirectSum toDirectSum)
    (AlgHom.id R (TensorAlgebra R M))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := TensorAlgebra R M)
    ((AlgHom.toLinearMap (AlgHom.comp ofDirectSum toDirectSum) ∘ₗ ι R : (a : M) → TensorAlgebra R M) x :
      TensorAlgebra R M)
    ((AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M)) ∘ₗ ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)

Tactic:
simp [tprod_apply]

Premises used: TensorAlgebra.tprod_apply
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : TensorAlgebra R M
⊢ (ofDirectSum : (a : ⨁ (n : ℕ), ⨂[R]^n M) → TensorAlgebra R M)
      ((toDirectSum : (a : TensorAlgebra R M) → ⨁ (n : ℕ), ⨂[R]^n M) x) =
    x

Tactic:
AlgHom.congr_fun ofDirectSum_comp_toDirectSum x

Premises used: AlgHom.congr_fun, TensorAlgebra.ofDirectSum_comp_toDirectSum, Trunc.lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n m : ℕ
h : n = m
x : ⨂[R]^n M
⊢ Eq (α := GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M)
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) m
      ((PiTensorProduct.reindex R (fun (x : Fin n) ↦ M) (Equiv.cast ⋯) :
          (a : ⨂[R] (i : Fin n), M) → ⨂[R] (i : Fin m), M)
        x))
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) n x)

Tactic:
Eq.symm (PiTensorProduct.gradedMonoid_eq_of_reindex_cast h rfl)

Premises used: PiTensorProduct.gradedMonoid_eq_of_reindex_cast, Eq.symm, rfl
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n m : ℕ
h : n = m
x : ⨂[R]^n M
rw :
  Eq (α := GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M)
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) m
      ((PiTensorProduct.reindex R (fun (x : Fin n) ↦ M) (Equiv.cast ⋯) :
          (a : ⨂[R] (i : Fin n), M) → ⨂[R] (i : Fin m), M)
        x))
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) n x)
rw₁ rw₂ :
  Eq (α := GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M) (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) n x)
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) n x)
⊢ Eq (α := GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M)
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) m
      ((PiTensorProduct.reindex R (fun (x : Fin n) ↦ M) (finCongr h) : (a : ⨂[R] (i : Fin n), M) → ⨂[R] (i : Fin m), M)
        x))
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) n x)

Tactic:
rw [finCongr_eq_equivCast, mk_reindex_cast h]

Premises used: finCongr_eq_equivCast, TensorAlgebra.mk_reindex_cast
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
⊢ Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))

Tactic:
Fin.consInduction ?_ ?_ x

Premises used: Fin.consInduction
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : Fin n → M
refine_1 :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
        (List.map
          (fun (a : Fin 0) ↦
            GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
              ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
                fun (x : Fin 1) ↦ a.elim0))
          (List.finRange 0)) :
      GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 0
        ((PiTensorProduct.tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0) :
      GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
refine_2 :
  ∀ {n : ℕ} (x₀ : M) (x : Fin n → M),
    Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
        (List.prod
          (List.map
            (fun (a : Fin n) ↦
              GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
                ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
                  fun (x_1 : Fin 1) ↦ x a))
            (List.finRange n)))
        (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
          ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x)) →
      Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
        (List.prod
          (List.map
            (fun (a : Fin (n + 1)) ↦
              GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
                ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
                  fun (x_1 : Fin 1) ↦ Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x a))
            (List.finRange (n + 1))))
        (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
          ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
              (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
            (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x)))
⊢ Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))

Tactic:
refine Fin.consInduction ?_ ?_ x
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
⊢ Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M) (1 : GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 0
        ((PiTensorProduct.tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0) :
      GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n_1 n : ℕ
x₀ : M
x : Fin n → M
ih :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
refine_2 :
  HMul.hMul (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
      (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
        ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
          fun (x_1 : Fin 1) ↦ Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x 0))
      (List.prod
        (List.map
          ((fun (a : Fin (n + 1)) ↦
              GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
                ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
                  fun (x_1 : Fin 1) ↦ Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x a)) ∘
            Fin.succ)
          (List.finRange n))) =
    GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
      ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))
⊢ Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin (n + 1)) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x a))
        (List.finRange (n + 1))))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
      ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x)))

Tactic:
rw [List.finRange_succ, List.map_cons, List.prod_cons, List.map_map]

Premises used: List.map_cons, List.finRange_succ, List.map_map, List.prod_cons
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n_1 n : ℕ
x₀ : M
x : Fin n → M
ih :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
refine_2 :
  HMul.hMul (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
      (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
        ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
          fun (x : Fin 1) ↦ x₀))
      (List.prod
        (List.map
          (fun (x_1 : Fin n) ↦
            GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
              ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
                fun (x_2 : Fin 1) ↦ x x_1))
          (List.finRange n))) =
    GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
      ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))
⊢ HMul.hMul (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
      (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
        ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
          fun (x_1 : Fin 1) ↦ Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x 0))
      (List.prod
        (List.map
          ((fun (a : Fin (n + 1)) ↦
              GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
                ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
                  fun (x_1 : Fin 1) ↦ Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x a)) ∘
            Fin.succ)
          (List.finRange n))) =
    GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
      ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))

Tactic:
simp_rw [Function.comp_def, Fin.cons_zero, Fin.cons_succ]

Premises used: Fin.cons_succ, Function.comp_def, Fin.cons_zero
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n_1 n : ℕ
x₀ : M
x : Fin n → M
ih :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
refine_2 :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (1 + n)
      ((PiTensorProduct.tprod R (s := fun (a : Fin (1 + n)) ↦ M) :
          (a : (i : Fin (1 + n)) → M) → ⨂[R] (i : Fin (1 + n)), M)
        (Fin.append (fun (x : Fin 1) ↦ x₀) x)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
      ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x)))
⊢ HMul.hMul (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
      (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
        ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
          fun (x : Fin 1) ↦ x₀))
      (List.prod
        (List.map
          (fun (x_1 : Fin n) ↦
            GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
              ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
                fun (x_2 : Fin 1) ↦ x x_1))
          (List.finRange n))) =
    GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
      ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))

Tactic:
rw [ih, GradedMonoid.mk_mul_mk, TensorPower.tprod_mul_tprod]

Premises used: GradedMonoid.mk_mul_mk, TensorPower.tprod_mul_tprod
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n_1 n : ℕ
x₀ : M
x : Fin n → M
ih :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
⊢ Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (1 + n)
      ((PiTensorProduct.tprod R (s := fun (a : Fin (1 + n)) ↦ M) :
          (a : (i : Fin (1 + n)) → M) → ⨂[R] (i : Fin (1 + n)), M)
        (Fin.append (fun (x : Fin 1) ↦ x₀) x)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) (n + 1)
      ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x)))

Tactic:
TensorPower.gradedMonoid_eq_of_cast (add_comm _ _) ?_

Premises used: add_comm, TensorPower.gradedMonoid_eq_of_cast
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n_1 n : ℕ
x₀ : M
x : Fin n → M
ih :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
refine_2 :
  Eq (α := ⨂[R]^(n + 1) M)
    ((PiTensorProduct.tprod R (s := fun (a : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.append (fun (x : Fin 1) ↦ x₀) x ∘ Fin.cast ⋯) :
      ⨂[R] (i : Fin (n + 1)), M)
    ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x) :
      ⨂[R] (i : Fin (n + 1)), M)
⊢ Eq (α := ⨂[R]^(n + 1) M)
    ((TensorPower.cast R M ⋯ : (a : ⨂[R]^(1 + n) M) → ⨂[R]^(n + 1) M)
        ((PiTensorProduct.tprod R (s := fun (a : Fin (1 + n)) ↦ M) :
            (a : (i : Fin (1 + n)) → M) → ⨂[R] (i : Fin (1 + n)), M)
          (Fin.append (fun (x : Fin 1) ↦ x₀) x)) :
      ⨂[R]^(n + 1) M)
    ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x) :
      ⨂[R] (i : Fin (n + 1)), M)

Tactic:
rw [TensorPower.cast_tprod]

Premises used: TensorPower.cast_tprod
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n_1 n : ℕ
x₀ : M
x : Fin n → M
ih :
  Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
    (List.prod
      (List.map
        (fun (a : Fin n) ↦
          GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) 1
            ((PiTensorProduct.tprod R (s := fun (x : Fin 1) ↦ M) : (a : (i : Fin 1) → M) → ⨂[R] (i : Fin 1), M)
              fun (x_1 : Fin 1) ↦ x a))
        (List.finRange n)))
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) n
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x))
refine_2 :
  Eq (α := ⨂[R]^(n + 1) M)
    ((PiTensorProduct.tprod R (s := fun (a : Fin (n + 1)) ↦ M) :
        (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
      fun (x_1 : Fin (n + 1)) ↦ Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x (Fin.cast ⋯ (Fin.cast ⋯ x_1)))
    ((PiTensorProduct.tprod R (s := fun (a : Fin (n + 1)) ↦ M) :
        (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x))
⊢ Eq (α := ⨂[R]^(n + 1) M)
    ((PiTensorProduct.tprod R (s := fun (a : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.append (fun (x : Fin 1) ↦ x₀) x ∘ Fin.cast ⋯) :
      ⨂[R] (i : Fin (n + 1)), M)
    ((PiTensorProduct.tprod R (s := fun (i : Fin (n + 1)) ↦ M) :
          (a : (i : Fin (n + 1)) → M) → ⨂[R] (i : Fin (n + 1)), M)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x₀ x) :
      ⨂[R] (i : Fin (n + 1)), M)

Tactic:
simp_rw [Fin.append_left_eq_cons, Function.comp_def]

Premises used: Fin.append_left_eq_cons, Function.comp_def