awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
inst_5 : DecidableEq ι
i : ι
u v : LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ map (s := s) (t := t)
      (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i (u + v)) =
    map (s := s) (t := t)
        (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i u) +
      map (s := s) (t := t)
        (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i v)
have H : ∀ (x : (i : ι) → s i),
  Eq (α := ⨂[R] (i : ι), t i)
    (((map (s := s) (t := t)
                (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i
                  (u + v))).compMultilinearMap
            (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), t i)
        x :
      ⨂[R] (i : ι), t i)
    (((map (s := s) (t := t)
                  (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i u) +
                map (s := s) (t := t)
                  (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i
                    v)).compMultilinearMap
            (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), t i)
        x :
      ⨂[R] (i : ι), t i)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
inst_5 : DecidableEq ι
i : ι
c : R
u : LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ map (s := s) (t := t)
      (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i (c • u)) =
    c •
      map (s := s) (t := t)
        (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i u)
have H : ∀ (x : (i : ι) → s i),
  Eq (α := ⨂[R] (i : ι), t i)
    (((map (s := s) (t := t)
                (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i
                  (c • u))).compMultilinearMap
            (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), t i)
        x :
      ⨂[R] (i : ι), t i)
    (((c •
                map (s := s) (t := t)
                  (update (β := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) f i
                    u)).compMultilinearMap
            (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), t i)
        x :
      ⨂[R] (i : ι), t i)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ (piTensorHomMap (s := s) (t := t) : (a : ⨂[R] (i : ι), s i →ₗ[R] t i) → (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), t i)
      ((tprod R (s := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) :
          (a : (i : ι) → s i →ₗ[R] t i) → ⨂[R] (i : ι), s i →ₗ[R] t i)
        f) =
    map (s := s) (t := t) f
have H : ∀ (x : (i : ι) → s i),
  Eq (α := ⨂[R] (i : ι), t i)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ((piTensorHomMap (s := s) (t := t) :
                (a : ⨂[R] (i : ι), s i →ₗ[R] t i) → (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), t i)
              ((tprod R (s := fun (i : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)) :
                  (a : (i : ι) → s i →ₗ[R] t i) → ⨂[R] (i : ι), s i →ₗ[R] t i)
                f))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), t i)
        x :
      ⨂[R] (i : ι), t i)
    (((map (s := s) (t := t) f).compMultilinearMap (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), t i)
        x :
      ⨂[R] (i : ι), t i)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
t' : ι → Type u_12
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : (i : ι) → AddCommMonoid (t' i)
inst_11 : (i : ι) → Module.{u_4, u_12} R (t' i)
g : (i : ι) → LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)
f_1 : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
f : (i : ι) → LinearEquiv.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ Eq (α := (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t i)
    ((map (s := s) (t := t) fun (i : ι) ↦ (↑(f i) : s i →ₗ[R] t i)) ∘ₗ
      map (s := t) (t := s) fun (i : ι) ↦ (↑(f i).symm : t i →ₗ[R] s i))
    LinearMap.id
have H : ∀ (x : (i : ι) → t i),
  Eq (α := ⨂[R] (i : ι), t i)
    ((LinearMap.compMultilinearMap (M₁ := t)
            ((map (s := s) (t := t) fun (i : ι) ↦ (↑(f i) : s i →ₗ[R] t i)) ∘ₗ
              map (s := t) (t := s) fun (i : ι) ↦ (↑(f i).symm : t i →ₗ[R] s i))
            (tprod R (s := t)) :
          (a : (i : ι) → t i) → ⨂[R] (i : ι), t i)
        x :
      ⨂[R] (i : ι), t i)
    ((LinearMap.compMultilinearMap (M₁ := t) LinearMap.id (tprod R (s := t)) : (a : (i : ι) → t i) → ⨂[R] (i : ι), t i)
        x :
      ⨂[R] (i : ι), t i)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
t' : ι → Type u_12
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : (i : ι) → AddCommMonoid (t' i)
inst_11 : (i : ι) → Module.{u_4, u_12} R (t' i)
g : (i : ι) → LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)
f_1 : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
f : (i : ι) → LinearEquiv.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), s i)
    ((map (s := t) (t := s) fun (i : ι) ↦ (↑(f i).symm : t i →ₗ[R] s i)) ∘ₗ
      map (s := s) (t := t) fun (i : ι) ↦ (↑(f i) : s i →ₗ[R] t i))
    LinearMap.id
have H : ∀ (x : (i : ι) → s i),
  Eq (α := ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ((map (s := t) (t := s) fun (i : ι) ↦ (↑(f i).symm : t i →ₗ[R] s i)) ∘ₗ
              map (s := s) (t := t) fun (i : ι) ↦ (↑(f i) : s i →ₗ[R] t i))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        x :
      ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s) LinearMap.id (tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        x :
      ⨂[R] (i : ι), s i)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
e : ι ≃ ι₂
φ : MultilinearMap.{u_4, u_2, u_7, u_9} R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) E
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] E)
    ((lift (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) :
          (a : MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) E) →
            (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] E)
        φ ∘ₗ
      (↑(reindex R s e) : (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)))
    ((lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E)
      ((LinearEquiv.symm (domDomCongrLinearEquiv' R R s E e) :
          (a : MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) E) → MultilinearMap R s E)
        φ))
have H : ∀ (x : (i : ι) → s i),
  Eq.{u_9 + 1} (α := E)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ((lift (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) :
                  (a : MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) E) →
                    (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] E)
                φ ∘ₗ
              (↑(reindex R s e) : (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ((lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E)
              ((LinearEquiv.symm (domDomCongrLinearEquiv' R R s E e) :
                  (a : MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) E) → MultilinearMap R s E)
                φ))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R s E
⊢ Eq (α := (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] E)
    ((lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E) φ ∘ₗ
      (↑(LinearEquiv.symm (reindex R s e)) : (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), s i))
    ((lift (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) :
        (a : MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) E) →
          (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] E)
      ((domDomCongrLinearEquiv' R R s E e :
          (a : MultilinearMap R s E) → MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) E)
        φ))
have H : ∀ (x : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)),
  Eq.{u_9 + 1} (α := E)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
            ((lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E) φ ∘ₗ
              (↑(LinearEquiv.symm (reindex R s e)) :
                (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), s i))
            (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))) :
          (a : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)) → E)
        x :
      E)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
            ((lift (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) :
                (a : MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) E) →
                  (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] E)
              ((domDomCongrLinearEquiv' R R s E e :
                  (a : MultilinearMap R s E) → MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) E)
                φ))
            (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))) :
          (a : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)) → E)
        x :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
⊢ Eq (α := (⨂[R] (i : ι), s i) ≃ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
    (reindex R s e ≪≫ₗ reindex R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) e') (reindex R s (e.trans e'))
have a : Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
  (↑(reindex R s e ≪≫ₗ reindex R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) e') :
    (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
  (↑(reindex R s (e.trans e')) :
    (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
Tactic: apply LinearEquiv.toLinearMap_injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
    (↑(reindex R s e ≪≫ₗ reindex R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) e') :
      (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
    (↑(reindex R s (e.trans e')) :
      (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
have a : ∀ (f : (i : ι) → s i),
  Eq (α := ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
    ((LinearMap.compMultilinearMap (M₁ := s)
            (↑(reindex R s e ≪≫ₗ reindex R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) e') :
              (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
        f :
      ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
    ((LinearMap.compMultilinearMap (M₁ := s)
            (↑(reindex R s (e.trans e')) :
              (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
        f :
      ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
Tactic: ext f
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
f : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
    ((LinearMap.compMultilinearMap (M₁ := s)
            (↑(reindex R s e ≪≫ₗ reindex R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) e') :
              (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
        f :
      ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
    ((LinearMap.compMultilinearMap (M₁ := s)
            (↑(reindex R s (e.trans e')) :
              (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
        f :
      ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
have a : Eq (α := ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
  ((tprod R (s := fun (i : ι₃) ↦ s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂))) :
        (a : (i : ι₃) → s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i))) →
          ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
      fun (i : ι₃) ↦ f ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)) :
    ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
  ((((LinearEquiv.symm
                (domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₃), s (((e.trans e').symm : (a : ι₃) → ι) i)) (e.trans e')) :
              (a :
                  MultilinearMap R (fun (i : ι₃) ↦ s (((e.trans e').symm : (a : ι₃) → ι) i))
                    (⨂[R] (i : ι₃), s (((e.trans e').symm : (a : ι₃) → ι) i))) →
                MultilinearMap R s (⨂[R] (i : ι₃), s (((e.trans e').symm : (a : ι₃) → ι) i)))
            (tprod R (s := fun (i : ι₃) ↦ s (((e.trans e').symm : (a : ι₃) → ι) i))) :
          MultilinearMap R s (⨂[R] (i : ι₃), s (((e.trans e').symm : (a : ι₃) → ι) i))) :
        (a : (i : ι) → s i) → ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
      f :
    ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
Tactic: simp only [LinearEquiv.trans_apply, LinearEquiv.coe_coe, reindex_tprod,
    LinearMap.coe_compMultilinearMap, Function.comp_apply,
    reindex_comp_tprod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
M : Type u_8
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι ≃ ι₂
⊢ Eq (α := (⨂[R] (i : ι₂), M) ≃ₗ[R] ⨂[R] (i : ι), M)
    (LinearEquiv.symm (reindex R (fun (x : ι) ↦ M) e) : (⨂[R] (i : ι₂), M) ≃ₗ[R] ⨂[R] (i : ι), M)
    (reindex R (fun (x : ι₂) ↦ M) e.symm : (⨂[R] (i : ι₂), M) ≃ₗ[R] ⨂[R] (i : ι), M)
have h : ∀ (x : ⨂[R] (i : ι₂), M),
  Eq (α := ⨂[R] (i : ι), M)
    (((LinearEquiv.symm (reindex R (fun (x : ι) ↦ M) e) : (⨂[R] (i : ι₂), M) ≃ₗ[R] ⨂[R] (i : ι), M) :
          (a : ⨂[R] (i : ι₂), M) → ⨂[R] (i : ι), M)
        x :
      ⨂[R] (i : ι), M)
    ((reindex R (fun (x : ι₂) ↦ M) e.symm : (a : ⨂[R] (i : ι₂), M) → ⨂[R] (i : ι), M) x : ⨂[R] (i : ι), M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
⊢ Eq (α := (⨂[R] (i : ι), s i) ≃ₗ[R] ⨂[R] (i : ι), s (((Equiv.refl ι).symm : (a : ι) → ι) i))
    (reindex R s (Equiv.refl ι)) (LinearEquiv.refl R (⨂[R] (i : ι), s i))
have h : ∀ (x : ⨂[R] (i : ι), s i),
  Eq (α := ⨂[R] (i : ι), s (((Equiv.refl ι).symm : (a : ι) → ι) i))
    ((reindex R s (Equiv.refl ι) : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), s (((Equiv.refl ι).symm : (a : ι) → ι) i))
        x :
      ⨂[R] (i : ι), s (((Equiv.refl ι).symm : (a : ι) → ι) i))
    ((LinearEquiv.refl R (⨂[R] (i : ι), s i) :
          (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), s (((Equiv.refl ι).symm : (a : ι) → ι) i))
        x :
      ⨂[R] (i : ι), s (((Equiv.refl ι).symm : (a : ι) → ι) i))
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
e : ι ≃ ι₂
⊢ (map (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (t := fun (i : ι₂) ↦ t ((e.symm : (a : ι₂) → ι) i))
        fun (i : ι₂) ↦ f ((e.symm : (a : ι₂) → ι) i)) ∘ₗ
      (↑(reindex R s e) : (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) =
    (↑(reindex R t e) : (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i)) ∘ₗ
      map (s := s) (t := t) f
have H : ∀ (m : (i : ι) → s i),
  Eq (α := ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
    ((LinearMap.compMultilinearMap (M₁ := s)
            ((map (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (t := fun (i : ι₂) ↦
                t ((e.symm : (a : ι₂) → ι) i)) fun (i : ι₂) ↦ f ((e.symm : (a : ι₂) → ι) i)) ∘ₗ
              (↑(reindex R s e) : (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
        m :
      ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
    ((((↑(reindex R t e) : (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i)) ∘ₗ
                map (s := s) (t := t) f).compMultilinearMap
            (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
        m :
      ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
e : ι ≃ ι₂
⊢ map (s := s) (t := t) f ∘ₗ
      (↑(LinearEquiv.symm (reindex R s e)) : (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), s i) =
    (↑(LinearEquiv.symm (reindex R t e)) : (⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), t i) ∘ₗ
      map (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (t := fun (i : ι₂) ↦ t ((e.symm : (a : ι₂) → ι) i))
        fun (i : ι₂) ↦ f ((e.symm : (a : ι₂) → ι) i)
have H : ∀ (m : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)),
  Eq (α := ⨂[R] (i : ι), t i)
    (((map (s := s) (t := t) f ∘ₗ
                (↑(LinearEquiv.symm (reindex R s e)) :
                  (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), s i)).compMultilinearMap
            (M₁ := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
            (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))) :
          (a : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι), t i)
        m :
      ⨂[R] (i : ι), t i)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
            ((↑(LinearEquiv.symm (reindex R t e)) :
                (⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), t i) ∘ₗ
              map (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (t := fun (i : ι₂) ↦
                t ((e.symm : (a : ι₂) → ι) i)) fun (i : ι₂) ↦ f ((e.symm : (a : ι₂) → ι) i))
            (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))) :
          (a : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι), t i)
        m :
      ⨂[R] (i : ι), t i)
Tactic: ext m