awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
x x_1 : N
⊢ (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
      (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) (x + x_1) ∘ₗ proj (φ := M) i) =
    HAdd.hAdd (α := ((i : ι) → M i) →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
      (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
        (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x ∘ₗ proj (φ := M) i)
      (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
        (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x_1 ∘ₗ proj (φ := M) i)
have h : ∀ (x_2 : (i : ι) → M i) (x_3 : ι),
  Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M x_3))
    ((pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
            (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) (x + x_1) ∘ₗ proj (φ := M) i :
          (a : (i : ι) → M i) → (i : ι) → N ⊗[R] M i)
        x_2 x_3 :
      TensorProduct.{u_1, u_3, u_5} R N (M x_3))
    ((HAdd.hAdd (α := ((i : ι) → M i) →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
            (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
              (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x ∘ₗ proj (φ := M) i)
            (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
              (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x_1 ∘ₗ proj (φ := M) i) :
          (a : (i : ι) → M i) → (i : ι) → N ⊗[R] M i)
        x_2 x_3 :
      TensorProduct.{u_1, u_3, u_5} R N (M x_3))
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ Eq (α := N ⊗[R] ((i : ι) → M i))
    (((piRightInv R S N M : ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) :
        (a : (i : ι) → N ⊗[R] M i) → N ⊗[R] ((i : ι) → M i))
      fun (i : ι) ↦ x ⊗ₜ[R] m i)
    (x ⊗ₜ[R] m)
have simp : Eq (α := N ⊗[R] ((i : ι) → M i)) (∑ x_1 : ι, x ⊗ₜ[R] Pi.single (M := M) x_1 (m x_1)) (x ⊗ₜ[R] m)
Tactic: simp only [piRightInv, lsum_apply, coe_sum, coe_comp, coe_proj, Finset.sum_apply,
    Function.comp_apply, Function.eval, AlgebraTensorModule.map_tmul, id_coe, id_eq, coe_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ Eq (α := N ⊗[R] ((i : ι) → M i)) (∑ x_1 : ι, x ⊗ₜ[R] Pi.single (M := M) x_1 (m x_1)) (x ⊗ₜ[R] m)
have rw : Eq (α := N ⊗[R] ((i : ι) → M i)) (x ⊗ₜ[R] ∑ a : ι, Pi.single (M := M) a (m a)) (x ⊗ₜ[R] m)
Tactic: rw [← tmul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ Eq (α := N ⊗[R] ((i : ι) → M i)) (x ⊗ₜ[R] ∑ a : ι, Pi.single (M := M) a (m a)) (x ⊗ₜ[R] m)
have e_n : ∑ a : ι, Pi.single (M := M) a (m a) = m
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ ∑ a : ι, Pi.single (M := M) a (m a) = m
have e_n : ∀ (j : ι), (∑ a : ι, Pi.single (M := M) a (m a)) j = m j
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
i : ι
m : M i
⊢ Eq (α := (j : ι) → TensorProduct.{u_1, u_3, u_5} R N (M j))
    (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i (x ⊗ₜ[R] m)) fun (j : ι) ↦
    x ⊗ₜ[R] Pi.single (M := M) i m j
have h : ∀ (j : ι),
  Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M j))
    (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i
        (x ⊗ₜ[R] m : TensorProduct.{u_1, u_3, u_5} R N (M i)) j :
      TensorProduct.{u_1, u_3, u_5} R N (M j))
    (x ⊗ₜ[R] Pi.single (M := M) i m j : TensorProduct.{u_1, u_3, u_5} R N (M j))
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
i : ι
m : M i
j : ι
⊢ Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M j))
    (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i
        (x ⊗ₜ[R] m : TensorProduct.{u_1, u_3, u_5} R N (M i)) j :
      TensorProduct.{u_1, u_3, u_5} R N (M j))
    (x ⊗ₜ[R] Pi.single (M := M) i m j : TensorProduct.{u_1, u_3, u_5} R N (M j))
have h : Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M j)) (x ⊗ₜ[R] Pi.single (M := M) i m j) (x ⊗ₜ[R] Pi.single (M := M) i m j)
Tactic: rw [← tmul_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
i : ι
m : M i
⊢ Eq (α := N ⊗[R] ((i : ι) → M i))
    (((piRightInv R S N M : ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) :
          (a : (i : ι) → N ⊗[R] M i) → N ⊗[R] ((i : ι) → M i))
        (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) i (x ⊗ₜ[R] m)) :
      N ⊗[R] ((i : ι) → M i))
    (x ⊗ₜ[R] Pi.single (M := M) i m : N ⊗[R] ((j : ι) → M j))
have this : Eq (α := (j : ι) → TensorProduct.{u_1, u_3, u_5} R N (M j))
  (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i (x ⊗ₜ[R] m)) fun (j : ι) ↦
  x ⊗ₜ[R] Pi.single (M := M) i m j
Tactic: have : Pi.single i (x ⊗ₜ m) = fun j ↦ x ⊗ₜ[R] (Pi.single i m j) := by
    ext j
    rw [← tmul_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
i : ι
m : M i
this :
  Eq (α := (j : ι) → TensorProduct.{u_1, u_3, u_5} R N (M j))
    (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i (x ⊗ₜ[R] m)) fun (j : ι) ↦
    x ⊗ₜ[R] Pi.single (M := M) i m j
⊢ Eq (α := N ⊗[R] ((i : ι) → M i))
    (((piRightInv R S N M : ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) :
          (a : (i : ι) → N ⊗[R] M i) → N ⊗[R] ((i : ι) → M i))
        (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) i (x ⊗ₜ[R] m)) :
      N ⊗[R] ((i : ι) → M i))
    (x ⊗ₜ[R] Pi.single (M := M) i m : N ⊗[R] ((j : ι) → M j))
have rw : Eq (α := N ⊗[R] ((i : ι) → M i))
  (((piRightInv R S N M : ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) :
      (a : (i : ι) → N ⊗[R] M i) → N ⊗[R] ((i : ι) → M i))
    fun (j : ι) ↦ x ⊗ₜ[R] Pi.single (M := M) i m j)
  (x ⊗ₜ[R] Pi.single (M := M) i m)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
⊢ Eq (α := ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
    ((piRightHom R S N M : N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ∘ₗ
        (piRightInv R S N M : ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) :
      ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
    (LinearMap.id :
      ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
have h : ∀ (i : ι) (x : N) (m : M i) (j : ι),
  Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M j))
    (((((AlgebraTensorModule.curry
                    (((piRightHom R S N M :
                            N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ∘ₗ
                          (piRightInv R S N M :
                            ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) :
                        ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S]
                          (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ∘ₗ
                      (single S (fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) i :
                        TensorProduct.{u_1, u_3, u_5} R N (M i) →ₗ[S]
                          (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))) :
                  N →ₗ[S] M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
                (a : N) → M i →ₗ[R] (i : ι) → N ⊗[R] M i)
              x :
            M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
          (a : M i) → (i : ι) → N ⊗[R] M i)
        m j :
      TensorProduct.{u_1, u_3, u_5} R N (M j))
    (((((AlgebraTensorModule.curry
                    (LinearMap.id ∘ₗ single S (fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) i) :
                  N →ₗ[S] M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
                (a : N) → M i →ₗ[R] (i : ι) → N ⊗[R] M i)
              x :
            M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
          (a : M i) → (i : ι) → N ⊗[R] M i)
        m j :
      TensorProduct.{u_1, u_3, u_5} R N (M j))
Tactic: ext i x m j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
⊢ Eq (α := N ⊗[R] ((i : ι) → M i) →ₗ[S] N ⊗[R] ((i : ι) → M i))
    ((piRightInv R S N M : ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) ∘ₗ
        (piRightHom R S N M : N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
      N ⊗[R] ((i : ι) → M i) →ₗ[S] N ⊗[R] ((i : ι) → M i))
    (LinearMap.id : N ⊗[R] ((i : ι) → M i) →ₗ[S] N ⊗[R] ((i : ι) → M i))
have a : ∀ (x : N) (j : ι) (m : M j),
  Eq (α := N ⊗[R] ((i : ι) → M i))
    ((((AlgebraTensorModule.curry
                    ((piRightInv R S N M :
                        ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) ∘ₗ
                      (piRightHom R S N M :
                        N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))) :
                  N →ₗ[S] ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i)) :
                (a : N) → ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i))
              x ∘ₗ
            single R M j :
          (a : M j) → N ⊗[R] ((i : ι) → M i))
        m :
      N ⊗[R] ((i : ι) → M i))
    ((((AlgebraTensorModule.curry LinearMap.id : N →ₗ[S] ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i)) :
                (a : N) → ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i))
              x ∘ₗ
            single R M j :
          (a : M j) → N ⊗[R] ((i : ι) → M i))
        m :
      N ⊗[R] ((i : ι) → M i))
Tactic: ext x j m
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
x y : N
⊢ LinearMap.compLeft (toSpanSingleton R N (x + y)) ι =
    HAdd.hAdd (α := (ι → R) →ₗ[R] ι → N) (LinearMap.compLeft (toSpanSingleton R N x) ι)
      (LinearMap.compLeft (toSpanSingleton R N y) ι)
have h : ∀ (i : ι → R) (j : ι),
  Eq.{u_3 + 1} (α := N) ((LinearMap.compLeft (toSpanSingleton R N (x + y)) ι : (a : ι → R) → ι → N) i j : N)
    ((HAdd.hAdd (α := (ι → R) →ₗ[R] ι → N) (LinearMap.compLeft (toSpanSingleton R N x) ι)
            (LinearMap.compLeft (toSpanSingleton R N y) ι) :
          (a : ι → R) → ι → N)
        i j :
      N)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
s : S
x : N
⊢ LinearMap.compLeft (toSpanSingleton R N (s • x)) ι =
    HSMul.hSMul (α := S) (β := (ι → R) →ₗ[R] ι → N) ((RingHom.id S : (a : S) → S) s : S)
      (LinearMap.compLeft (toSpanSingleton R N x) ι)
have h : ∀ (i : ι → R) (j : ι),
  Eq.{u_3 + 1} (α := N) ((LinearMap.compLeft (toSpanSingleton R N (s • x)) ι : (a : ι → R) → ι → N) i j : N)
    ((HSMul.hSMul (α := S) (β := (ι → R) →ₗ[R] ι → N) ((RingHom.id S : (a : S) → S) s : S)
            (LinearMap.compLeft (toSpanSingleton R N x) ι) :
          (a : ι → R) → ι → N)
        i j :
      N)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ Eq.{u_3 + 1} (α := N) ((LinearMap.compLeft (toSpanSingleton R N (s • x)) ι : (a : ι → R) → ι → N) i j : N)
    ((HSMul.hSMul (α := S) (β := (ι → R) →ₗ[R] ι → N) ((RingHom.id S : (a : S) → S) s : S)
            (LinearMap.compLeft (toSpanSingleton R N x) ι) :
          (a : ι → R) → ι → N)
        i j :
      N)
have h : i j • s • x = s • i j • x
Tactic: dsimp only [coe_comp, coe_single, Function.comp_apply, compLeft_apply, toSpanSingleton_apply,
      RingHom.id_apply, smul_apply, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ i j • s • x = s • i j • x
have h : s • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) (i j) : S) x = s • i j • x
Tactic: rw [← IsScalarTower.smul_assoc, _root_.Algebra.smul_def, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
x : N
f : ι → R
⊢ Eq (α := ι → N)
    (((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) : (a : N ⊗[R] (ι → R)) → ι → N) (x ⊗ₜ[R] f) : ι → N)
    fun (j : ι) ↦ f j • x
have h : ∀ (j : ι),
  ((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) : (a : N ⊗[R] (ι → R)) → ι → N) (x ⊗ₜ[R] f) j = f j • x
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
⊢ Eq (α := (ι → N) →ₗ[S] ι → N)
    ((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) ∘ₗ
      (piScalarRightInv R S N ι : (ι → N) →ₗ[S] N ⊗[R] (ι → R)))
    LinearMap.id
have h : ∀ (i : ι) (x : N) (j : ι),
  Eq.{u_3 + 1} (α := N)
    ((((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) ∘ₗ
              (piScalarRightInv R S N ι : (ι → N) →ₗ[S] N ⊗[R] (ι → R))) ∘ₗ
            single.{u_2, u_4, u_3} S (fun (i : ι) ↦ N) i :
          (a : N) → ι → N)
        x j :
      N)
    (((LinearMap.id ∘ₗ single.{u_2, u_4, u_3} S (fun (i : ι) ↦ N) i : N →ₗ[S] ι → N) : (a : N) → ι → N) x j : N)
Tactic: ext i x j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Pi (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
⊢ Eq (α := N ⊗[R] (ι → R) →ₗ[S] N ⊗[R] (ι → R))
    (piScalarRightInv R S N ι ∘ₗ piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] N ⊗[R] (ι → R))
    (LinearMap.id : N ⊗[R] (ι → R) →ₗ[S] N ⊗[R] (ι → R))
have a : ∀ (x : N) (i : ι),
  Eq (α := N ⊗[R] (ι → R))
    (((((AlgebraTensorModule.curry (piScalarRightInv R S N ι ∘ₗ piScalarRightHom R S N ι) :
                  N →ₗ[S] (ι → R) →ₗ[R] N ⊗[R] (ι → R)) :
                (a : N) → (ι → R) →ₗ[R] N ⊗[R] (ι → R))
              x ∘ₗ
            single R (fun (i : ι) ↦ R) i :
          R →ₗ[R] N ⊗[R] (ι → R)) :
        (a : R) → N ⊗[R] (ι → R))
      1)
    (((((AlgebraTensorModule.curry LinearMap.id : N →ₗ[S] (ι → R) →ₗ[R] N ⊗[R] (ι → R)) :
                (a : N) → (ι → R) →ₗ[R] N ⊗[R] (ι → R))
              x ∘ₗ
            single R (fun (i : ι) ↦ R) i :
          R →ₗ[R] N ⊗[R] (ι → R)) :
        (a : R) → N ⊗[R] (ι → R))
      1)
Tactic: ext x i
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Prod (goal)
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
⊢ Eq (α := M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
    ((AlgebraTensorModule.lift
          (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
            LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃)) :
        M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) ∘ₗ
      (LinearMap.coprod
          (((AlgebraTensorModule.lTensor S M₁ : (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
              (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
            (LinearMap.inl R M₂ M₃))
          (((AlgebraTensorModule.lTensor S M₁ : (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
              (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
            (LinearMap.inr R M₂ M₃)) :
        M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)))
    LinearMap.id
have hl : ∀ (x : M₁) (x_1 : M₂),
  Eq (α := M₁ ⊗[R] M₂)
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.lift
                            (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                              LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃)) :
                          M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) ∘ₗ
                        (LinearMap.coprod
                            (((AlgebraTensorModule.lTensor S M₁ :
                                  (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                              (LinearMap.inl R M₂ M₃))
                            (((AlgebraTensorModule.lTensor S M₁ :
                                  (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                              (LinearMap.inr R M₂ M₃)) :
                          M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))) ∘ₗ
                      LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).1
    (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).1
Tactic: ext