awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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))
have 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)
Tactic: refine Fin.consInduction ?_ ?_ x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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)
⊢ 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))
have 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)))
Tactic: refine Fin.consInduction ?_ ?_ x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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)
    (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)))
have 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))
Tactic: rw [List.finRange_succ, List.map_cons, List.prod_cons, List.map_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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))
⊢ 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))
have 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))
Tactic: simp_rw [Function.comp_def, Fin.cons_zero, Fin.cons_succ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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))
⊢ 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))
have 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)))
Tactic: rw [ih, GradedMonoid.mk_mul_mk, TensorPower.tprod_mul_tprod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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 (α := ⨂[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)
have 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 sorry) :
    ⨂[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: rw [TensorPower.cast_tprod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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 (α := ⨂[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)
have 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 sorry (Fin.cast sorry 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))
Tactic: simp_rw [Fin.append_left_eq_cons, Function.comp_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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 (α := ⨁ (n : ℕ), ⨂[R]^n M)
    ((toDirectSum : (a : TensorAlgebra R M) → ⨁ (n : ℕ), ⨂[R]^n M)
        ((tprod R M n : (a : (i : Fin n) → M) → TensorAlgebra R M) x) :
      ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)
have rw : Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
  (List.prod
      (List.ofFn (n := n)
        (Function.comp (β := TensorAlgebra R M) (⇑toDirectSum : (a : TensorAlgebra R M) → ⨁ (n : ℕ), ⨂[R]^n M)
          fun (i : Fin n) ↦ (ι R : (a : M) → TensorAlgebra R M) (x i))) :
    ⨁ (n : ℕ), ⨂[R]^n M)
  (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) : (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
    ⨁ (i : ℕ), ⨂[R]^i M)
Tactic: rw [tprod_apply, map_list_prod, List.map_ofFn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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 (α := ⨁ (n : ℕ), ⨂[R]^n M)
    (List.prod
        (List.ofFn (n := n)
          (Function.comp (β := TensorAlgebra R M) (⇑toDirectSum : (a : TensorAlgebra R M) → ⨁ (n : ℕ), ⨂[R]^n M)
            fun (i : Fin n) ↦ (ι R : (a : M) → TensorAlgebra R M) (x i))) :
      ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)
have simp_rw : Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
  (List.prod
      (List.ofFn (n := n) fun (x_1 : Fin n) ↦
        ((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_2 : Fin 1) ↦ x x_1)) :
    ⨁ (n : ℕ), ⨂[R]^n M)
  (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) : (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
    ⨁ (i : ℕ), ⨂[R]^i M)
Tactic: simp_rw [Function.comp_def, toDirectSum_ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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 (α := ⨁ (n : ℕ), ⨂[R]^n M)
    (List.prod
        (List.ofFn (n := n) fun (x_1 : Fin n) ↦
          ((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_2 : Fin 1) ↦ x x_1)) :
      ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)
have rw : Eq (α := ⨁ (n : ℕ), ⨂[R]^n M)
  (((DirectSum.of (fun (n : ℕ) ↦ ⨂[R]^n M) ((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) :
          ⨂[R]^((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
        (a : ⨂[R]^((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) M) → ⨁ (i : ℕ), ⨂[R]^i M)
      ((List.finRange n).dProd (A := fun (n : ℕ) ↦ ⨂[R]^n M) (fun (x : Fin n) ↦ 1) fun (x_1 : Fin n) ↦
        (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) :
    ⨁ (i : ℕ), ⨂[R]^i M)
  (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) : (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
      ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
    ⨁ (i : ℕ), ⨂[R]^i M)
Tactic: rw [DirectSum.list_prod_ofFn_of_eq_dProd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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 (α := ⨁ (n : ℕ), ⨂[R]^n M)
    (((DirectSum.of (fun (n : ℕ) ↦ ⨂[R]^n M) ((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) :
            ⨂[R]^((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1) M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((List.finRange n).dProd (A := fun (n : ℕ) ↦ ⨂[R]^n M) (fun (x : Fin n) ↦ 1) fun (x_1 : Fin n) ↦
          (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) :
      ⨁ (i : ℕ), ⨂[R]^i M)
    (((DirectSum.of (fun (i : ℕ) ↦ ⨂[R]^i M) n : ⨂[R]^n M →+ ⨁ (i : ℕ), ⨂[R]^i M) :
          (a : ⨂[R]^n M) → ⨁ (i : ℕ), ⨂[R]^i M)
        ((PiTensorProduct.tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      ⨁ (i : ℕ), ⨂[R]^i M)
have h : Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
  (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) ((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1)
    ((List.finRange n).dProd (A := fun (n : ℕ) ↦ ⨂[R]^n M) (fun (x : Fin n) ↦ 1) fun (x_1 : Fin n) ↦
      (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))
  (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: apply DirectSum.of_eq_of_gradedMonoid_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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)
    (GradedMonoid.mk (A := fun (n : ℕ) ↦ ⨂[R]^n M) ((List.finRange n).dProdIndex fun (x : Fin n) ↦ 1)
      ((List.finRange n).dProd (A := fun (n : ℕ) ↦ ⨂[R]^n M) (fun (x : Fin n) ↦ 1) fun (x_1 : Fin n) ↦
        (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))
    (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))
have h : 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: rw [GradedMonoid.mk_list_dProd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
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))
have h : Eq (α := GradedMonoid fun (n : ℕ) ↦ ⨂[R]^n M)
  (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))
  (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: rw [TensorPower.list_prod_gradedMonoid_mk_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := (⨁ (n : ℕ), ⨂[R]^n M) →ₐ[R] ⨁ (n : ℕ), ⨂[R]^n M) (AlgHom.comp toDirectSum ofDirectSum)
    (AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M))
have h : ∀ (i : ℕ) (x : (i : Fin i) → M) (i_1 : ℕ),
  (((LinearMap.compMultilinearMap (M₁ := fun (i : Fin i) ↦ M)
                (AlgHom.toLinearMap (AlgHom.comp toDirectSum ofDirectSum) ∘ₗ
                  DirectSum.lof R ℕ (fun (i : ℕ) ↦ ⨂[R]^i M) i)
                (PiTensorProduct.tprod R (s := fun (i : Fin i) ↦ M)) :
              (a : (i : Fin i) → M) → ⨁ (n : ℕ), ⨂[R]^n M)
            x :
          ⨁ (n : ℕ), ⨂[R]^n M) :
        (a : ℕ) → ⨂[R]^a M)
      i_1 =
    (((LinearMap.compMultilinearMap (M₁ := fun (i : Fin i) ↦ M)
                (AlgHom.toLinearMap (AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)) ∘ₗ DirectSum.lof R ℕ (fun (i : ℕ) ↦ ⨂[R]^i M) i)
                (PiTensorProduct.tprod R (s := fun (i : Fin i) ↦ M)) :
              (a : (i : Fin i) → M) → ⨁ (n : ℕ), ⨂[R]^n M)
            x :
          ⨁ (n : ℕ), ⨂[R]^n M) :
        (a : ℕ) → ⨂[R]^a M)
      i_1
Tactic: ext