awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₃ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((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)
            (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _)) :
        ⨂[R]^n 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)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ 0 a
          (@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]
-- 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
rw₃ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((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)
            (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _)) :
        ⨂[R]^n M) =
    r • a
rw₄ :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
          (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ 0 a
            (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _)) :
        ⨂[R]^n 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₅ : r • a = 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
r s : R
⊢ Eq (α := ⨂[R]^0 M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) :
      ⨂[R]^0 M)
    ((algebraMap₀ : (a : R) → ⨂[R]^0 M) (r * s) : ⨂[R]^0 M)
have rw : (cast R M sorry : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
    (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
      ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) =
  HSMul.hSMul (β := ⨂[R]^0 M) r ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s : ⨂[R]^0 M)
Tactic: rw [← smul_eq_mul, map_smul]
-- 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
r s : R
⊢ Eq (α :=
    ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))
      M)
    (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
        (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
          ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))) :
      ⨂[R] (x :
        Fin
          (Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))),
        M)
    ((LinearEquiv.symm (cast R M ⋯) :
          (a :
              ⨂[R]^(GradedMonoid.mk (0 + 0)
                      (GradedMonoid.GMul.mul (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)
                        (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) s))).fst
                M) →
            ⨂[R]^(GradedMonoid.mk 0
                    (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) (r * s))).fst
              M)
        (Sigma.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
          (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) (HAdd.hAdd (α := ℕ) 0 0)
            (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) AddSemigroup.toAdd _ 0 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) s)))) :
      ⨂[R]^(Sigma.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
            (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) (r * s))))
        M)
have this : Eq (α := ⨂[R]^0 M)
  ((cast R M sorry : (a : ⨂[R]^(0 + 0) M) → ⨂[R]^0 M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 0 ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) s)) :
    ⨂[R]^0 M)
  ((algebraMap₀ : (a : R) → ⨂[R]^0 M) (r * s) : ⨂[R]^0 M)
Tactic: have := algebraMap₀_mul_algebraMap₀ (M := M) r s
-- 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
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
⊢ (cast R M ⋯ :
        (a :
            ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
              M) →
          ⨂[R]^(x * GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)).fst
            M)
      ((GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
            x).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    (x *
          GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
have this : Eq (α := ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
  ((cast R M sorry : (a : ⨂[R]^(0 + x.fst) M) → ⨂[R]^x.fst M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
        ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M))) :
    ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
  ((cast R M sorry : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^x.fst M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
        (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
    ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
Tactic: have := (algebraMap₀_mul r x.snd).trans (mul_algebraMap₀ r x.snd).symm
-- 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
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
this :
  Eq (α := ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + x.fst) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M))) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
          (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
⊢ (cast R M ⋯ :
        (a :
            ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
              M) →
          ⨂[R]^(x * GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)).fst
            M)
      ((GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
            x).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    (x *
          GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
have rw : (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
          ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
        x).snd
    (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) =
  (cast R M sorry :
      (a :
          ⨂[R]^(x * GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)).fst
            M) →
        ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst M)
    ((x *
          GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))
Tactic: rw [← LinearEquiv.eq_symm_apply, cast_symm]
-- 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
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
this :
  Eq (α := ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(0 + x.fst) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
          ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M))) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
    ((cast R M ⋯ : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^x.fst M)
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
          (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
      ⨂[R]^(x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
⊢ (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
          x).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) =
    (cast R M ⋯ :
        (a :
            ⨂[R]^(x * GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r)).fst
              M) →
          ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
            M)
      ((x *
            GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
              ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r)).snd
        (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))
have this₁ : Eq (α := ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
  (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M))
      ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r) (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) :
    ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
  ((cast R M sorry : (a : ⨂[R]^(x.fst + 0) M) → ⨂[R]^(0 + x.fst) M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ (x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) 0
        (x.snd (β := fun (i : ℕ) ↦ ⨂[R]^i M)) ((algebraMap₀ : (a : R) → ⨂[R]^0 M) r)) :
    ⨂[R]^(0 + x.fst (β := fun (i : ℕ) ↦ ⨂[R]^i M)) M)
Tactic: rw [← LinearEquiv.eq_symm_apply, cast_symm, cast_cast] at this
Cleared hypotheses: this
-- 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
r : R
x : GradedMonoid fun (i : ℕ) ↦ ⨂[R]^i M
⊢ (cast R M ⋯ :
        (a : ⨂[R]^(r • x).fst M) →
          ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
            M)
      ((r • x).snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    (GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
          x).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
have rw : (r • x).snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) =
  (cast R M sorry :
      (a :
          ⨂[R]^(GradedMonoid.mk 0 (((↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M).toAddMonoidHom : (a : R) → ⨂[R]^0 M) r) * x).fst
            M) →
        ⨂[R]^(r • x).fst M)
    ((GradedMonoid.mk (A := fun (i : ℕ) ↦ ⨂[R]^i M) 0
            ((LinearMap.toAddMonoidHom (↑algebraMap₀ : R →ₗ[R] ⨂[R]^0 M) : (a : R) → ⨂[R]^0 M) r) *
          x).snd
      (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))
Tactic: rw [← LinearEquiv.eq_symm_apply, cast_symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
⊢ Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
        ((φ : (a : M) → R) (v i)) j :
      R)
have pos : ∀ (h : j = i),
  Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
        ((φ : (a : M) → R) (v i)) j :
      R)
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
pos :
  ∀ (h : j = i),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
⊢ Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
        ((φ : (a : M) → R) (v i)) j :
      R)
have neg : ∀ (h : ¬j = i),
  Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
        ((φ : (a : M) → R) (v i)) j :
      R)
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : j = i
⊢ Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
    (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
        ((φ : (a : M) → R) (v i)) j :
      R)
have pos : Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f j φ j : (a : M) → R) (v j) : R)
  (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) j ((φ : (a : M) → R) (v j))
      j :
    R)
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
this :
  ∀ (x : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
inst_3 : DecidableEq (Fin n)
f : (i : Fin n) → Module.Dual R M
i : Fin n
a : R
φ : Module.Dual R M
⊢ (PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
        (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
      (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
        (MultilinearMap.mkPiRing R (Fin n) 1) (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i (a • φ))) =
    HSMul.hSMul (β := Module.Dual R (⨂[R]^n M)) a
      ((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
            (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
          (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
            (MultilinearMap.mkPiRing R (Fin n) 1) (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ)) :
        (⨂[R] (i : Fin n), M) →ₗ[R] R)
have H : ∀ (v : (i : Fin n) → M),
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin n) ↦ M)
            ((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
              (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                (MultilinearMap.mkPiRing R (Fin n) 1)
                (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i (a • φ))))
            (tprod R (s := fun (i : Fin n) ↦ M)) :
          (a : (i : Fin n) → M) → R)
        v :
      R)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin n) ↦ M)
            (HSMul.hSMul (β := Module.Dual R (⨂[R]^n M)) a
              ((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                    (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
                  (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                    (MultilinearMap.mkPiRing R (Fin n) 1)
                    (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ)) :
                (⨂[R] (i : Fin n), M) →ₗ[R] R))
            (tprod R (s := fun (i : Fin n) ↦ M)) :
          (a : (i : Fin n) → M) → R)
        v :
      R)
Tactic: ext v