awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb nc : ℕ
a : ⨂[R]^na M
b : ⨂[R]^nb M
c : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun (n m : ℕ) ↦
    LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M))
      (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M)
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
        (a : ⨂[R]^(na + nb) M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) →
          (⨂[R]^nb M →ₗ[R] ⨂[R]^(na + nb) M) →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
      (LinearMap.compr₂ (mul (na + nb) nc) (↑e : ⨂[R]^(na + nb + nc) M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ∘ₗ
    mul na nb
⊢ Eq (α := ⨂[R]^(na + (nb + nc)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(na + nb + nc) M) → ⨂[R]^(na + (nb + nc)) M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (na + nb) _
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ _ a b) c) :
      ⨂[R]^(na + (nb + nc)) M)
    (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ (nb + nc) a
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ _ b c) :
      ⨂[R]^(na + (nb + nc)) M)
have lhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
  Eq (α := ⨂[R]^(na + (nb + nc)) M)
    ((((((lhs : (a : ⨂[R]^na M) → ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) a :
                  ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
                (a : ⨂[R]^nb M) → ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
              b :
            ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) :
          (a : ⨂[R]^nc M) → ⨂[R]^(na + (nb + nc)) M)
        c :
      ⨂[R]^(na + (nb + nc)) M)
    ((e : (a : ⨂[R]^(na + nb + nc) M) → ⨂[R]^(na + (nb + nc)) M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (na + nb) _
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ _ a b) c) :
      ⨂[R]^(na + (nb + nc)) M)
Tactic: have lhs_eq : ∀ a b c, lhs a b c = e (a ₜ* b ₜ* c) := fun _ _ _ => rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _ ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) a) =
    r • a
have rw : (cast R M sorry : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
    ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
              (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
            ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) :
          ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
        (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
      a) =
  r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂, map_smul,
    ← gMul_eq_coe_linearMap, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _ ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) a) =
    r • a
have rw₁ : (cast R M sorry : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
    ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
              (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
            (HSMul.hSMul (β := ⨂[R]^0 M) r
              (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)) :
          ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
        (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
      a) =
  r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂, map_smul,
    ← gMul_eq_coe_linearMap, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
rw₁ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              (HSMul.hSMul (β := ⨂[R]^0 M) r
                (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _ ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) a) =
    r • a
have rw₂ : (cast R M sorry : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
    (HSMul.hSMul (β := ⨂[R]^(0 + n) M) r
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                    (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                  (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
                (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
              ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
            (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
          a :
        ⨂[R]^(0 + n) M)) =
  r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂, map_smul,
    ← gMul_eq_coe_linearMap, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
rw₁ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              (HSMul.hSMul (β := ⨂[R]^0 M) r
                (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
rw₂ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (HSMul.hSMul (β := ⨂[R]^(0 + n) M) r
        ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                      (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                    (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
                  (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
                ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
              (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            a :
          ⨂[R]^(0 + n) M)) =
    r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _ ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) a) =
    r • a
have rw₃ : HSMul.hSMul (β := ⨂[R]^n M) r
    ((cast R M sorry : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
        ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                    (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                  (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
                (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
              ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
            (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
          a) :
      ⨂[R]^n M) =
  r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂, map_smul,
    ← gMul_eq_coe_linearMap, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
rw₁ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              (HSMul.hSMul (β := ⨂[R]^0 M) r
                (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
rw₂ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (HSMul.hSMul (β := ⨂[R]^(0 + n) M) r
        ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                      (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                    (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
                  (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
                ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
              (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            a :
          ⨂[R]^(0 + n) M)) =
    r • a
rw₃ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                      (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                    (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
                  (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
                ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
              (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            a) :
        ⨂[R]^n M) =
    r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _ ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) a) =
    r • a
have rw₄ : HSMul.hSMul (β := ⨂[R]^n M) r
    ((cast R M sorry : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _
          (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) a) :
      ⨂[R]^n M) =
  r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂, map_smul,
    ← gMul_eq_coe_linearMap, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
rw₁ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                  (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
              (HSMul.hSMul (β := ⨂[R]^0 M) r
                (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M)) :
            ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
          (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        a) =
    r • a
rw₂ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (HSMul.hSMul (β := ⨂[R]^(0 + n) M) r
        ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                      (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                    (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
                  (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
                ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
              (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            a :
          ⨂[R]^(0 + n) M)) =
    r • a
rw₃ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M))
                      (↑mulEquiv : ⨂[R]^0 M ⊗[R] ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
                    (a : ⨂[R]^0 M) → ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M)
                  (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
                ⨂[R]^n M →ₗ[R] ⨂[R]^(0 + n) M) :
              (a : ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            a) :
        ⨂[R]^n M) =
    r • a
rw₄ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _
            (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) a) :
        ⨂[R]^n M) =
    r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _ ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) a) =
    r • a
have rw₅ : r • a = r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂, map_smul,
    ← gMul_eq_coe_linearMap, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
⊢ (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ 0 a ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
    r • a
have rw : (cast R M sorry : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
    ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
              (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
            a :
          ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
        (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
      ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
  r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, map_smul, map_smul, ← gMul_eq_coe_linearMap,
    mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                  (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
              a :
            ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
          (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
    r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ 0 a ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
    r • a
have rw₁ : (cast R M sorry : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
    ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
              (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
            a :
          ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
        (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
      (HSMul.hSMul (β := ⨂[R]^0 M) r
        (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M))) =
  r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, map_smul, map_smul, ← gMul_eq_coe_linearMap,
    mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                  (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
              a :
            ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
          (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
    r • a
rw₁ :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                  (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
              a :
            ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
          (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        (HSMul.hSMul (β := ⨂[R]^0 M) r
          (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M))) =
    r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ 0 a ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
    r • a
have rw₂ : (cast R M sorry : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
    (HSMul.hSMul (β := ⨂[R]^(n + 0) M) r
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                    (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                  (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
                a :
              ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
            (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
          (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
        ⨂[R]^(n + 0) M)) =
  r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, map_smul, map_smul, ← gMul_eq_coe_linearMap,
    mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                  (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
              a :
            ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
          (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
    r • a
rw₁ :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                  (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
              a :
            ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
          (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        (HSMul.hSMul (β := ⨂[R]^0 M) r
          (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _ : ⨂[R]^0 M))) =
    r • a
rw₂ :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      (HSMul.hSMul (β := ⨂[R]^(n + 0) M) r
        ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                      (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                    (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
                  a :
                ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
              (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) :
          ⨂[R]^(n + 0) M)) =
    r • a
⊢ (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ 0 a ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) =
    r • a
have rw₃ : HSMul.hSMul (β := ⨂[R]^n M) r
    ((cast R M sorry : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
        ((((LinearMap.compr₂ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^0 M))
                    (↑mulEquiv : ⨂[R]^n M ⊗[R] ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
                  (a : ⨂[R]^n M) → ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M)
                a :
              ⨂[R]^0 M →ₗ[R] ⨂[R]^(n + 0) M) :
            (a : ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
          (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _)) :
      ⨂[R]^n M) =
  r • a
Tactic: rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, map_smul, map_smul, ← gMul_eq_coe_linearMap,
    mul_one]