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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
⊢ Eq (α := TensorAlgebra R M)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin j) ↦ M)
            ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin i) ↦ M)
                  (LinearMap.compr₂
                    (LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M))
                      (↑mulEquiv : ⨂[R]^i M ⊗[R] ⨂[R]^j M →ₗ[R] ⨂[R]^(i + j) M))
                    toTensorAlgebra)
                  (PiTensorProduct.tprod R (s := fun (i : Fin i) ↦ M)) :
                (a : (i : Fin i) → M) → ⨂[R]^j M →ₗ[R] TensorAlgebra R M)
              a)
            (PiTensorProduct.tprod R (s := fun (i : Fin j) ↦ M)) :
          (a : (i : Fin j) → M) → TensorAlgebra R M)
        b :
      TensorAlgebra R M)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin j) ↦ M)
            ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin i) ↦ M)
                  (LinearMap.compl₂ (LinearMap.mul R (TensorAlgebra R M)) toTensorAlgebra ∘ₗ toTensorAlgebra)
                  (PiTensorProduct.tprod R (s := fun (i : Fin i) ↦ M)) :
                (a : (i : Fin i) → M) → ⨂[R]^j M →ₗ[R] TensorAlgebra R M)
              a)
            (PiTensorProduct.tprod R (s := fun (i : Fin j) ↦ M)) :
          (a : (i : Fin j) → M) → TensorAlgebra R M)
        b :
      TensorAlgebra R M)
have H : Eq (α := TensorAlgebra R M)
  (List.prod
    (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
      (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)))
  (((LinearMap.mul R (TensorAlgebra R M) : (a : TensorAlgebra R M) → TensorAlgebra R M →ₗ[R] TensorAlgebra R M)
        (List.prod (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))) :
      (a : TensorAlgebra R M) → TensorAlgebra R M)
    (List.prod (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))))
Tactic: simp only [LinearMap.compMultilinearMap_apply, LinearMap.compr₂_apply, ← gMul_def,
    TensorProduct.mk_apply, LinearEquiv.coe_coe, tprod_mul_tprod, toTensorAlgebra_tprod,
    TensorAlgebra.tprod_apply, LinearMap.comp_apply, LinearMap.compl₂_apply]
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
⊢ Eq (α := TensorAlgebra R M)
    (List.prod
      (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
        (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)))
    (((LinearMap.mul R (TensorAlgebra R M) : (a : TensorAlgebra R M) → TensorAlgebra R M →ₗ[R] TensorAlgebra R M)
          (List.prod (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))) :
        (a : TensorAlgebra R M) → TensorAlgebra R M)
      (List.prod (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))))
have H : List.prod
    (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
      (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)) =
  (HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))).prod
Tactic: refine Eq.trans ?_ List.prod_append
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
⊢ List.prod
      (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
        (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)) =
    (HAppend.hAppend (α := List (TensorAlgebra R M))
        (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
        (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))).prod
have H : (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
    (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)) =
  HAppend.hAppend (α := List (TensorAlgebra R M))
    (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
    (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
Tactic: congr
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
⊢ (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
      (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
have H : List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
  HAppend.hAppend (α := List (TensorAlgebra R M))
    (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
    (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
Tactic: rw [List.ofFn_comp' _ (TensorAlgebra.ι R), List.ofFn_comp' _ (TensorAlgebra.ι R),
    List.ofFn_comp' _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
H :
  List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
⊢ (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
      (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
have H₁ : List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
  HAppend.hAppend (α := List (TensorAlgebra R M))
    (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a))
    (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
Tactic: rw [List.ofFn_comp' _ (TensorAlgebra.ι R), List.ofFn_comp' _ (TensorAlgebra.ι R),
    List.ofFn_comp' _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
H :
  List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
H₁ :
  List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
⊢ (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
      (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
have H₂ : List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
  HAppend.hAppend (α := List (TensorAlgebra R M))
    (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a))
    (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn b))
Tactic: rw [List.ofFn_comp' _ (TensorAlgebra.ι R), List.ofFn_comp' _ (TensorAlgebra.ι R),
    List.ofFn_comp' _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
H :
  List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
H₁ :
  List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
H₂ :
  List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a))
      (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn b))
⊢ (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
      (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
have H₃ : Eq (α := List (TensorAlgebra R M))
  (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)))
  (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a ++ List.ofFn b))
Tactic: rw [List.ofFn_comp' _ (TensorAlgebra.ι R), List.ofFn_comp' _ (TensorAlgebra.ι R),
    List.ofFn_comp' _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
H :
  List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
H₁ :
  List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
H₂ :
  List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a))
      (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn b))
H₃ :
  Eq (α := List (TensorAlgebra R M))
    (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn (Fin.append a b)))
    (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a ++ List.ofFn b))
⊢ (List.ofFn (n := i + j) fun (i_1 : Fin (i + j)) ↦
      (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (Fin.append a b i_1)) =
    HAppend.hAppend (α := List (TensorAlgebra R M))
      (List.ofFn (n := i) fun (i : Fin i) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (a i))
      (List.ofFn (n := j) fun (i : Fin j) ↦ (TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) (b i))
have H₄ : Eq (α := List (TensorAlgebra R M))
  (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a ++ List.ofFn b))
  (List.map (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M) (List.ofFn a ++ List.ofFn b))
Tactic: rw [List.ofFn_comp' _ (TensorAlgebra.ι R), List.ofFn_comp' _ (TensorAlgebra.ι R),
    List.ofFn_comp' _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]
-- 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
r : R
⊢ 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)
have 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)
Tactic: rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, map_smul,
    TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, map_smul,
    TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]
-- 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
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)
⊢ 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)
have 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
Tactic: rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, map_smul,
    TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]
-- 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
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
⊢ 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)
have rw₃ : HSMul.hSMul (β := TensorAlgebra R M) r 1 = (algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r
Tactic: rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, map_smul,
    TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]
-- 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
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
⊢ 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)
have rw₄ : HSMul.hSMul (β := TensorAlgebra R M) r 1 = HSMul.hSMul (β := TensorAlgebra R M) r 1
Tactic: rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, map_smul,
    TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]
-- 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 (α := TensorAlgebra R M →ₐ[R] TensorAlgebra R M) (AlgHom.comp ofDirectSum toDirectSum)
    (AlgHom.id R (TensorAlgebra R M))
have 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)
Tactic: ext
-- 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 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) (finCongr h) : (a : ⨂[R] (i : Fin n), M) → ⨂[R] (i : Fin m), M)
        x))
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) n x)
have 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 sorry) : (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]
-- 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 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)
⊢ 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)
have 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)
Tactic: rw [finCongr_eq_equivCast, mk_reindex_cast h]