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
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)
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:
simp
-- 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)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearEquiv.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
m : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι), t i)
    ((congr (s := s) (t := t) f : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), t i)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) m) :
      ⨂[R] (i : ι), t i)
    (⨂ₜ[R] (i : ι), (f i : (a : s i) → t i) (m i) : ⨂[R] (i : ι), t i)

Tactic:
simp only [congr, LinearEquiv.ofLinear_apply, map_tprod, LinearEquiv.coe_coe]

Premises used: PiTensorProduct.map_tprod, PiTensorProduct.congr, LinearEquiv.coe_coe, LinearEquiv.ofLinear_apply
-- 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)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearEquiv.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
p : (i : ι) → t i
⊢ Eq (α := ⨂[R] (i : ι), s i)
    (((congr (s := s) (t := t) f).symm : (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι), s i)
        ((tprod R (s := t) : (a : (i : ι) → t i) → ⨂[R] (i : ι), t i) p) :
      ⨂[R] (i : ι), s i)
    (⨂ₜ[R] (i : ι), ((f i).symm : (a : t i) → s i) (p i) : ⨂[R] (i : ι), s i)

Tactic:
simp only [congr, LinearEquiv.ofLinear_symm_apply, map_tprod, LinearEquiv.coe_coe]

Premises used: PiTensorProduct.map_tprod, PiTensorProduct.congr, LinearEquiv.ofLinear_symm_apply, LinearEquiv.coe_coe
-- 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)
t : ι → Type u_11
t' : ι → Type u_12
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_5 : (i : ι) → AddCommMonoid (t' i)
inst_6 : (i : ι) → Module.{u_4, u_12} R (t' i)
f : (i : ι) → s i →ₗ[R] LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)
x : (i : ι) → s i
y : (i : ι) → t i
⊢ Eq (α := ⨂[R] (i : ι), t' i)
    ((((map₂ (s := s) (t := t) (t' := t') f : (a : ⨂[R] (i : ι), s i) → (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)
              ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) x) :
            (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i) :
          (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι), t' i)
        ((tprod R (s := t) : (a : (i : ι) → t i) → ⨂[R] (i : ι), t i) y) :
      ⨂[R] (i : ι), t' i)
    (⨂ₜ[R] (i : ι),
        (((f i : (a : s i) → t i →ₗ[R] t' i) (x i) : LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)) :
            (a : t i) → t' i)
          (y i) :
      ⨂[R] (i : ι), t' i)

Tactic:
simp [map₂]

Premises used: PiTensorProduct.map₂
-- 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)
t : ι → Type u_11
t' : ι → Type u_12
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_5 : (i : ι) → AddCommMonoid (t' i)
inst_6 : (i : ι) → Module.{u_4, u_12} R (t' i)
f : (i : ι) → s i →ₗ[R] LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)
a : (i : ι) → s i
b : (i : ι) → t i
⊢ Eq (α := ⨂[R] (i : ι), t' i)
    ((((((piTensorHomMap₂ (s := s) (t := t) (t' := t') :
                      (a : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i) →
                        (⨂[R] (i : ι), s i) →ₗ[R] (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)
                    ((tprod R (s := fun (i : ι) ↦
                          s i →ₗ[R] LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)) :
                        (a : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i) → ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i)
                      f) :
                  (⨂[R] (i : ι), s i) →ₗ[R] (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i) :
                (a : ⨂[R] (i : ι), s i) → (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i)
              ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) a) :
            (⨂[R] (i : ι), t i) →ₗ[R] ⨂[R] (i : ι), t' i) :
          (a : ⨂[R] (i : ι), t i) → ⨂[R] (i : ι), t' i)
        ((tprod R (s := t) : (a : (i : ι) → t i) → ⨂[R] (i : ι), t i) b) :
      ⨂[R] (i : ι), t' i)
    (⨂ₜ[R] (i : ι),
        (((f i : (a : s i) → t i →ₗ[R] t' i) (a i) : LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)) :
            (a : t i) → t' i)
          (b i) :
      ⨂[R] (i : ι), t' i)

Tactic:
simp [piTensorHomMapFun₂, piTensorHomMap₂]

Premises used: PiTensorProduct.piTensorHomMap₂, PiTensorProduct.piTensorHomMapFun₂
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
e : ι ≃ ι₂
f : MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) ≃ₗ[R]
  MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) :=
  domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) e
g : MultilinearMap R s (⨂[R] (i : ι), s i) ≃ₗ[R]
  MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (⨂[R] (i : ι), s i) :=
  domDomCongrLinearEquiv' R R s (⨂[R] (i : ι), s i) e
⊢ Eq (α := (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))
    ((lift (s := s) :
          (a : MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))) →
            (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))
        ((f.symm :
            (a :
                MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
                  (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))) →
              MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)))
          (tprod R (s := 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)) (⨂[R] (i : ι), s i)) →
            (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), s i)
        ((g :
            (a : MultilinearMap R s (⨂[R] (i : ι), s i)) →
              MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (⨂[R] (i : ι), s i))
          (tprod R (s := s))))
    LinearMap.id

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
e : ι ≃ ι₂
f : MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) ≃ₗ[R]
  MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) :=
  domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) e
g : MultilinearMap R s (⨂[R] (i : ι), s i) ≃ₗ[R]
  MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (⨂[R] (i : ι), s i) :=
  domDomCongrLinearEquiv' R R s (⨂[R] (i : ι), s i) e
⊢ Eq (α := (⨂[R] (i : ι), s 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)) (⨂[R] (i : ι), s i)) →
            (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] ⨂[R] (i : ι), s i)
        ((g :
            (a : MultilinearMap R s (⨂[R] (i : ι), s i)) →
              MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)) (⨂[R] (i : ι), s i))
          (tprod R (s := s))) ∘ₗ
      (lift (s := s) :
          (a : MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))) →
            (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))
        ((f.symm :
            (a :
                MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
                  (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))) →
              MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)))
          (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i)))))
    LinearMap.id

Tactic:
aesop
-- 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)
e : ι ≃ ι₂
f : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))
    ((((lift (s := s) :
                (a : MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))) →
                  (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))
              (MultilinearMap.mk (M₁ := s)
                (comp (β := (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 : ι₂), s ((e.symm : (a : ι₂) → ι) i))
                  (⇑(Equiv.piCongrLeft' s e) : (a : (a : ι) → s a) → (b : ι₂) → s ((e.symm : (a : ι₂) → ι) b)))
                ⋯ ⋯) :
            (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) :
          (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f) :
      ⨂[R] (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 : ι₂), s ((e.symm : (a : ι₂) → ι) i))
        fun (i : ι₂) ↦ f ((e.symm : (a : ι₂) → ι) i) :
      ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))

Tactic:
liftAux_tprod _ f

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, PiTensorProduct.liftAux_tprod, PiTensorProduct.tprodCoeff, AddCon.toQuotient, FreeAddMonoid.sumAux
-- 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)
e : ι ≃ ι₂
f : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))
    ((((lift (s := s) :
                (a : MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))) →
                  (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))
              (MultilinearMap.mk (M₁ := s)
                (comp (β := (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 : ι₂), s ((e.symm : (a : ι₂) → ι) i))
                  (⇑(Equiv.piCongrLeft' s e) : (a : (a : ι) → s a) → (b : ι₂) → s ((e.symm : (a : ι₂) → ι) b)))
                ⋯ ⋯) :
            (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) :
          (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f) :
      ⨂[R] (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 : ι₂), s ((e.symm : (a : ι₂) → ι) i))
        fun (i : ι₂) ↦ f ((e.symm : (a : ι₂) → ι) i) :
      ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))

Tactic:
exact liftAux_tprod _ f

Premises used: PiTensorProduct.liftAux_tprod
-- 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)
e : ι ≃ ι₂
⊢ Eq (α := MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)))
    (LinearMap.compMultilinearMap (M₁ := s)
      (↑(reindex R s e) : (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) (tprod R (s := s)))
    ((LinearEquiv.symm (domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) e) :
        (a :
            MultilinearMap R (fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))
              (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i))) →
          MultilinearMap R s (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)))
      (tprod R (s := fun (i : ι₂) ↦ s ((e.symm : (a : ι₂) → ι) i))))

Tactic:
MultilinearMap.ext <| reindex_tprod e

Premises used: PiTensorProduct.reindex_tprod, MultilinearMap.ext
-- 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)
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
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)
⊢ 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)
        φ))

Tactic:
ext
-- 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)
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
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:
simp [reindex]

Premises used: PiTensorProduct.reindex
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R s E
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)
⊢ 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)
        φ))

Tactic:
ext
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R s E
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:
simp [reindex]

Premises used: PiTensorProduct.reindex
-- 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)
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
x : ⨂[R] (i : ι), s i
⊢ Eq.{u_9 + 1} (α := 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)
              φ :
            (⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) →ₗ[R] E) :
          (a : ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) → E)
        ((reindex R s e : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) x :
          ⨂[R] (i : ι₂), s ((e.symm : (a : ι₂) → ι) i)) :
      E)
    ((((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)
                φ) :
            (⨂[R] (i : ι), s i) →ₗ[R] E) :
          (a : ⨂[R] (i : ι), s i) → E)
        x :
      E)

Tactic:
LinearMap.congr_fun (lift_comp_reindex e φ) x

Premises used: Quotient.liftOn', AddCon.liftOn, PiTensorProduct.lift_comp_reindex, LinearMap.congr_fun