awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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' : ι₂ ≃ ι₃
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)))
⊢ 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'))

Tactic:
apply LinearEquiv.toLinearMap_injective

Premises used: LinearEquiv.toLinearMap_injective
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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' : ι₂ ≃ ι₃
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 : ι₂)))
⊢ 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:
ext f
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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 : ι₂)))
⊢ 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:
simp only [LinearEquiv.trans_apply, LinearEquiv.coe_coe, reindex_tprod,
    LinearMap.coe_compMultilinearMap, Function.comp_apply,
    reindex_comp_tprod]

Premises used: PiTensorProduct.reindex_comp_tprod, PiTensorProduct.reindex_tprod, LinearEquiv.trans_apply, LinearMap.coe_compMultilinearMap, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ι₂)))
    ((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:
congr
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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' : ι₂ ≃ ι₃
x : ⨂[R] (i : ι), s i
⊢ Eq (α := ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
    ((reindex R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) e' :
          (a : ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →
            ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i)))
        ((reindex R s e : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) x) :
      ⨂[R] (i : ι₃), s ((e.symm : (a : ι₂) → ι) ((e'.symm : (a : ι₃) → ι₂) i : ι₂)))
    ((reindex R s (e.trans e') : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι₃), s (((e.trans e').symm : (a : ι₃) → ι) i)) x :
      ⨂[R] (i : ι₃), s (((e.trans e').symm : (a : ι₃) → ι) i))

Tactic:
LinearEquiv.congr_fun (reindex_trans e e' : _ = reindex R s (e.trans e')) x

Premises used: Quotient.liftOn', AddCon.liftOn, PiTensorProduct.reindex_trans, LinearEquiv.congr_fun
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ι ≃ ι₂
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)
⊢ 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)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ι ≃ ι₂
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:
simp [reindex]

Premises used: PiTensorProduct.reindex
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
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))
⊢ 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))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
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:
simp [reindex, domDomCongrLinearEquiv']

Premises used: PiTensorProduct.reindex, MultilinearMap.domDomCongrLinearEquiv'
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ι ≃ ι₂
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))
⊢ (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

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ι ≃ ι₂
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:
simp only [LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe,
    LinearMap.comp_apply, reindex_tprod, map_tprod]

Premises used: LinearMap.comp_apply, PiTensorProduct.reindex_tprod, PiTensorProduct.map_tprod, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ι ≃ ι₂
x : ⨂[R] (i : ι), s i
⊢ Eq (α := ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) 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) :
          (a : ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
        ((reindex R s e : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) x) :
      ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
    ((reindex R t e : (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
        ((map (s := s) (t := t) f : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), t i) x) :
      ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))

Tactic:
DFunLike.congr_fun (map_comp_reindex_eq _ _) _

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, PiTensorProduct.map_comp_reindex_eq
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ι ≃ ι₂
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)
⊢ 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)

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ι ≃ ι₂
m : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)
H :
  Eq (α := ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
    ((reindex R t e : (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) 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 ((e.symm : (a : ι₂) → ι) i))
    ((reindex R t e : (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) 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 ((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:
apply LinearEquiv.injective (reindex R t e)

Premises used: PiTensorProduct.reindex, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ι ≃ ι₂
m : (i : ι₂) → s ((e.symm : (a : ι₂) → ι) i)
⊢ Eq (α := ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) i))
    ((reindex R t e : (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) 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 ((e.symm : (a : ι₂) → ι) i))
    ((reindex R t e : (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι₂), t ((e.symm : (a : ι₂) → ι) 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 ((e.symm : (a : ι₂) → ι) i))

Tactic:
simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
    comp_apply, ← map_reindex, LinearEquiv.apply_symm_apply, map_tprod]

Premises used: PiTensorProduct.map_tprod, LinearMap.coe_comp, LinearEquiv.apply_symm_apply, Function.comp_apply, PiTensorProduct.map_reindex, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe