awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
have rw : Module.rank R (FreeAlgebra R κ) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
Tactic: rw [(equivFreeAlgebra b).toLinearEquiv.rank_eq, FreeAlgebra.rank_eq, mk_list_eq_sum_pow,
    Basis.mk_eq_rank'' b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
rw : Module.rank R (FreeAlgebra R κ) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
have rw₁ : Cardinal.lift.{uR, uM} #(List κ) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
Tactic: rw [(equivFreeAlgebra b).toLinearEquiv.rank_eq, FreeAlgebra.rank_eq, mk_list_eq_sum_pow,
    Basis.mk_eq_rank'' b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
rw : Module.rank R (FreeAlgebra R κ) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
rw₁ : Cardinal.lift.{uR, uM} #(List κ) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
have rw₂ : Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ #κ ^ n) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
Tactic: rw [(equivFreeAlgebra b).toLinearEquiv.rank_eq, FreeAlgebra.rank_eq, mk_list_eq_sum_pow,
    Basis.mk_eq_rank'' b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
rw : Module.rank R (FreeAlgebra R κ) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
rw₁ : Cardinal.lift.{uR, uM} #(List κ) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
rw₂ : Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ #κ ^ n) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
have rw₃ : Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n) =
  Cardinal.lift.{uR, uM} (sum fun (n : ℕ) ↦ Module.rank R M ^ n)
Tactic: rw [(equivFreeAlgebra b).toLinearEquiv.rank_eq, FreeAlgebra.rank_eq, mk_list_eq_sum_pow,
    Basis.mk_eq_rank'' b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Grading (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 (B := ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
      (DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x)
      ((lift R : (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (GradedAlgebra.ι R M)))
    (AlgHom.id R (TensorAlgebra R M))
have w : ∀ (m : M),
  Eq (α := TensorAlgebra R M)
    ((AlgHom.toLinearMap
              (AlgHom.comp (B :=
                ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
                (DirectSum.coeAlgHom fun (x : ℕ) ↦
                  HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x)
                ((lift R :
                    (a : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i))
                  (GradedAlgebra.ι R M))) ∘ₗ
            ι R :
          (a : M) → TensorAlgebra R M)
        m :
      TensorAlgebra R M)
    ((AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M)) ∘ₗ ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        ((((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))
          ((ι R : (a : M) → TensorAlgebra R M) m)) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
have w : Eq (α := TensorAlgebra R M)
  ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
        (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
      ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥((ι R).range ^ i)) m) :
    TensorAlgebra R M)
  ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
w :
  Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥((ι R).range ^ i)) m) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
⊢ Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        ((((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))
          ((ι R : (a : M) → TensorAlgebra R M) m)) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
have w₁ : Eq (α := TensorAlgebra R M)
  ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
        (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
      (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) 1 :
            ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1) →+
              ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
          (a : ↥((ι R).range ^ 1)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
        (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1)
          ((ι R : (a : M) → TensorAlgebra R M) m) sorry)) :
    TensorAlgebra R M)
  ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
w :
  Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥((ι R).range ^ i)) m) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
w₁ :
  Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
                1 :
              ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1) →+
                ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
            (a : ↥((ι R).range ^ 1)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
          (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
            x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1)
            ((ι R : (a : M) → TensorAlgebra R M) m) ⋯)) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
⊢ Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        ((((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))
          ((ι R : (a : M) → TensorAlgebra R M) m)) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
have w₂ : Eq (α := TensorAlgebra R M)
  ((↑(Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
          x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1)
          ((ι R : (a : M) → TensorAlgebra R M) m) sorry) :
      TensorAlgebra R M) :
    TensorAlgebra R M)
  ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
w :
  Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥((ι R).range ^ i)) m) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
w₁ :
  Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        (((DirectSum.of (fun (i : ℕ) ↦ ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i))
                1 :
              ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1) →+
                ⨁ (i : ℕ), ↥(HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) i)) :
            (a : ↥((ι R).range ^ 1)) → ⨁ (i : ℕ), ↥((ι R).range ^ i))
          (Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
            x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1)
            ((ι R : (a : M) → TensorAlgebra R M) m) ⋯)) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
w₂ :
  Eq (α := TensorAlgebra R M)
    ((↑(Subtype.mk (p := fun (x : TensorAlgebra R M) ↦
            x ∈ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (β := ℕ) (LinearMap.range (ι R)) 1)
            ((ι R : (a : M) → TensorAlgebra R M) m) ⋯) :
        TensorAlgebra R M) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
⊢ Eq (α := TensorAlgebra R M)
    ((DirectSum.coeAlgHom fun (x : ℕ) ↦ HPow.hPow (α := Submodule R (TensorAlgebra R M)) (LinearMap.range (ι R)) x :
          (a : ⨁ (i : ℕ), ↥((ι R).range ^ i)) → TensorAlgebra R M)
        ((((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))
          ((ι R : (a : M) → TensorAlgebra R M) m)) :
      TensorAlgebra R M)
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
have w₃ : Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
  ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Grading (goal)
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)
⊢ 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))
have 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))
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Grading (goal)
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
⊢ 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))
have 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))
Tactic: dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
-- 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 : ⨂[R]^i M
b : ⨂[R]^j 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)
have 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)
Tactic: rw [TensorPower.gMul_eq_coe_linearMap, ← LinearMap.compr₂_apply, ← @LinearMap.mul_apply' R, ←
    LinearMap.compl₂_apply, ← LinearMap.comp_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 : ⨂[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)
have 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)
Tactic: refine LinearMap.congr_fun (LinearMap.congr_fun ?_ a) b
-- 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 : ℕ
⊢ 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)
have 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)
Tactic: ext (a b)