awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ℕ
x : ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)
obtain :
  ∀ (x : TensorAlgebra R M) (hx : x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i),
    Eq (α := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
      ((((lift R : (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
                (GradedAlgebra.ι R M) :
              TensorAlgebra R M →ₐ[R]
                ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
            (a : TensorAlgebra R M) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
          (↑(Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
                x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) x hx) :
            TensorAlgebra R M) :
        ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
      (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) i :
              ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) →+
                ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
            (a : ↥((ι R).range ^ i)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
          (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
            x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) x hx) :
        ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
⊢ Eq (α := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    ((((lift R : (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
              (GradedAlgebra.ι R M) :
            TensorAlgebra R M →ₐ[R]
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : TensorAlgebra R M) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (↑x : TensorAlgebra R M) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) i :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ i)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        x :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ℕ
x : TensorAlgebra R M
hx : x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i
dsimp :
  Eq (α := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    ((((lift R : (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
              (GradedAlgebra.ι R M) :
            TensorAlgebra R M →ₐ[R]
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : TensorAlgebra R M) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        x :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) i :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ i)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) x hx) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
⊢ Eq (α := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    ((((lift R : (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
              (GradedAlgebra.ι R M) :
            TensorAlgebra R M →ₐ[R]
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : TensorAlgebra R M) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (↑(Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
              x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) x hx) :
          TensorAlgebra R M) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) i :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ i)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i) x hx) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))

Tactic:
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]

Premises used: Subtype.coe_mk, DirectSum.lof_eq_of
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ℕ
x : TensorAlgebra R M
r : R
⊢ Eq (α := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) 0 :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ 0)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (((@DirectSum.GAlgebra.toFun _ R
                (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) inst
                (fun (i : ℕ) ↦
                  (HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i).addCommMonoid)
                (fun (i : ℕ) ↦ (HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i).module)
                Nat.instAddMonoid
                (SetLike.gsemiring fun (x : ℕ) ↦
                  HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x)
                _ :
              R →+ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0)) :
            (a : R) → ↥((ι R).range ^ 0))
          r) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) 0 :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ 0)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 0)
          ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r) ⋯) :
      ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))

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 : ℕ
x : Fin n → M
⊢ Eq (α := TensorAlgebra R M)
    ((toTensorAlgebra : (a : ⨂[R]^n M) → TensorAlgebra R M)
        ((PiTensorProduct.tprod R (s := fun (a : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) x) :
      TensorAlgebra R M)
    ((TensorAlgebra.tprod R M n : (a : (i : Fin n) → M) → TensorAlgebra R M) x : TensorAlgebra R M)

Tactic:
PiTensorProduct.lift.tprod _

Premises used: PiTensorProduct.lift.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
⊢ Eq (α := TensorAlgebra R M)
    ((toTensorAlgebra : (a : ⨂[R]^0 M) → TensorAlgebra R M)
        (@GradedMonoid.GOne.one _ (fun (n : ℕ) ↦ ⨂[R]^n M) MulZeroClass.toZero _) :
      TensorAlgebra R M)
    (1 : TensorAlgebra R M)

Tactic:
simp [GradedMonoid.GOne.one, TensorPower.toTensorAlgebra_tprod]

Premises used: GradedMonoid.GOne.one, TensorPower.toTensorAlgebra_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
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
rw :
  Eq (α := TensorAlgebra R 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 :
                (a : ⨂[R]^i M) → ⨂[R]^j M →ₗ[R] TensorAlgebra R M)
              a :
            ⨂[R]^j M →ₗ[R] TensorAlgebra R M) :
          (a : ⨂[R]^j M) → TensorAlgebra R M)
        b :
      TensorAlgebra R M)
    ((((LinearMap.compl₂ (LinearMap.mul R (TensorAlgebra R M)) toTensorAlgebra ∘ₗ toTensorAlgebra :
                (a : ⨂[R]^i M) → ⨂[R]^j M →ₗ[R] TensorAlgebra R M)
              a :
            ⨂[R]^j M →ₗ[R] TensorAlgebra R M) :
          (a : ⨂[R]^j M) → TensorAlgebra R M)
        b :
      TensorAlgebra R M)
⊢ (toTensorAlgebra : (a : ⨂[R]^(i + j) M) → TensorAlgebra R M)
      (@GradedMonoid.GMul.mul _ (fun (n : ℕ) ↦ ⨂[R]^n M) instAddNat _ _ _ a b) =
    HMul.hMul (α := TensorAlgebra R M) (β := TensorAlgebra R M)
      ((toTensorAlgebra : (a : ⨂[R]^i M) → TensorAlgebra R M) a : TensorAlgebra R M)
      ((toTensorAlgebra : (a : ⨂[R]^j M) → TensorAlgebra R M) b : TensorAlgebra R M)

Tactic:
rw [TensorPower.gMul_eq_coe_linearMap, ← LinearMap.compr₂_apply, ← @LinearMap.mul_apply' R, ←
    LinearMap.compl₂_apply, ← LinearMap.comp_apply]

Premises used: LinearMap.compl₂_apply, TensorPower.gMul_eq_coe_linearMap, LinearMap.mul_apply', LinearMap.comp_apply, LinearMap.compr₂_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
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ Eq (α := TensorAlgebra R 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 :
                (a : ⨂[R]^i M) → ⨂[R]^j M →ₗ[R] TensorAlgebra R M)
              a :
            ⨂[R]^j M →ₗ[R] TensorAlgebra R M) :
          (a : ⨂[R]^j M) → TensorAlgebra R M)
        b :
      TensorAlgebra R M)
    ((((LinearMap.compl₂ (LinearMap.mul R (TensorAlgebra R M)) toTensorAlgebra ∘ₗ toTensorAlgebra :
                (a : ⨂[R]^i M) → ⨂[R]^j M →ₗ[R] TensorAlgebra R M)
              a :
            ⨂[R]^j M →ₗ[R] TensorAlgebra R M) :
          (a : ⨂[R]^j M) → TensorAlgebra R M)
        b :
      TensorAlgebra R M)

Tactic:
LinearMap.congr_fun (LinearMap.congr_fun ?_ a) b

Premises used: LinearMap.congr_fun
-- 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
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
refine :
  Eq (α := ⨂[R]^i M →ₗ[R] ⨂[R]^j M →ₗ[R] TensorAlgebra R 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)
    (LinearMap.compl₂ (LinearMap.mul R (TensorAlgebra R M)) toTensorAlgebra ∘ₗ toTensorAlgebra)
⊢ Eq (α := TensorAlgebra R 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 :
                (a : ⨂[R]^i M) → ⨂[R]^j M →ₗ[R] TensorAlgebra R M)
              a :
            ⨂[R]^j M →ₗ[R] TensorAlgebra R M) :
          (a : ⨂[R]^j M) → TensorAlgebra R M)
        b :
      TensorAlgebra R M)
    ((((LinearMap.compl₂ (LinearMap.mul R (TensorAlgebra R M)) toTensorAlgebra ∘ₗ toTensorAlgebra :
                (a : ⨂[R]^i M) → ⨂[R]^j M →ₗ[R] TensorAlgebra R M)
              a :
            ⨂[R]^j M →ₗ[R] TensorAlgebra R M) :
          (a : ⨂[R]^j M) → TensorAlgebra R M)
        b :
      TensorAlgebra R M)

Tactic:
refine LinearMap.congr_fun (LinearMap.congr_fun ?_ a) b

Premises used: LinearMap.congr_fun
-- 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
i j : ℕ
H :
  ∀ (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)
⊢ Eq (α := ⨂[R]^i M →ₗ[R] ⨂[R]^j M →ₗ[R] TensorAlgebra R 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)
    (LinearMap.compl₂ (LinearMap.mul R (TensorAlgebra R M)) toTensorAlgebra ∘ₗ toTensorAlgebra)

Tactic:
ext (a b)
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
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))))
⊢ 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)

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]

Premises used: LinearMap.compl₂_apply, TensorProduct.mk_apply, LinearMap.comp_apply, LinearMap.compr₂_apply, TensorPower.tprod_mul_tprod, TensorPower.gMul_def, TensorAlgebra.tprod_apply, LinearMap.compMultilinearMap_apply, TensorPower.toTensorAlgebra_tprod, LinearEquiv.coe_coe
-- 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
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))))

Tactic:
Eq.trans ?_ List.prod_append

Premises used: List.prod_append, Eq.trans
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
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
⊢ 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:
refine Eq.trans ?_ List.prod_append

Premises used: List.prod_append, Eq.trans
-- 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
i j : ℕ
a : (i : Fin i) → M
b : (i : Fin j) → M
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))
⊢ 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:
congr
-- 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
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))
H₄ 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))
⊢ (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:
rw [List.ofFn_comp' _ (TensorAlgebra.ι R), List.ofFn_comp' _ (TensorAlgebra.ι R),
    List.ofFn_comp' _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]

Premises used: List.ofFn_fin_append, List.ofFn_comp', TensorAlgebra.ι, List.map_append, DFunLike.coe