awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
g : (i : ι) → LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
x : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι), t' i)
    ((LinearMap.compMultilinearMap (M₁ := s) (map (s := s) (t := t') fun (i : ι) ↦ g i ∘ₗ f i) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), t' i)
        x :
      ⨂[R] (i : ι), t' i)
    (((map (s := t) (t := t') g ∘ₗ 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:
simp only [LinearMap.compMultilinearMap_apply, map_tprod, LinearMap.coe_comp, Function.comp_apply]

Premises used: PiTensorProduct.map_tprod, LinearMap.coe_comp, Function.comp_apply, LinearMap.compMultilinearMap_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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
t : ι → Type u_11
inst_5 : (i : ι) → AddCommMonoid (t i)
inst_6 : (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)
h : MultilinearMap R t E
H :
  ∀ (x : (i : ι) → s i),
    Eq.{u_9 + 1} (α := E)
      ((LinearMap.compMultilinearMap (M₁ := s)
              ((lift (s := t) : (a : MultilinearMap R t E) → (⨂[R] (i : ι), t i) →ₗ[R] E) h ∘ₗ map (s := s) (t := t) f)
              (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)
                (h.compLinearMap (M₁ := s) (M₁' := t) f))
              (tprod R (s := s)) :
            (a : (i : ι) → s i) → E)
          x :
        E)
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] E)
    ((lift (s := t) : (a : MultilinearMap R t E) → (⨂[R] (i : ι), t i) →ₗ[R] E) h ∘ₗ map (s := s) (t := t) f)
    ((lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E)
      (h.compLinearMap (M₁ := s) (M₁' := t) f))

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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
t : ι → Type u_11
inst_5 : (i : ι) → AddCommMonoid (t i)
inst_6 : (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)
h : MultilinearMap R t E
x : (i : ι) → s i
⊢ Eq.{u_9 + 1} (α := E)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ((lift (s := t) : (a : MultilinearMap R t E) → (⨂[R] (i : ι), t i) →ₗ[R] E) h ∘ₗ map (s := s) (t := t) f)
            (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)
              (h.compLinearMap (M₁ := s) (M₁' := t) f))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)

Tactic:
simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, Function.comp_apply,
    map_tprod, lift.tprod, MultilinearMap.compLinearMap_apply]

Premises used: PiTensorProduct.lift.tprod, PiTensorProduct.map_tprod, LinearMap.coe_comp, Function.comp_apply, MultilinearMap.compLinearMap_apply, LinearMap.compMultilinearMap_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)
H :
  ∀ (x : (i : ι) → s i),
    Eq (α := ⨂[R] (i : ι), s i)
      ((LinearMap.compMultilinearMap (M₁ := s) (map (s := s) (t := s) fun (i : ι) ↦ LinearMap.id) (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)
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), s i) (map (s := s) (t := s) fun (i : ι) ↦ LinearMap.id) LinearMap.id

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 : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s) (map (s := s) (t := s) fun (i : ι) ↦ LinearMap.id) (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 only [LinearMap.compMultilinearMap_apply, map_tprod, LinearMap.id_coe, id_eq]

Premises used: LinearMap.id_coe, PiTensorProduct.map_tprod, LinearMap.compMultilinearMap_apply, id_eq
-- 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)
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), s i) (map (s := s) (t := s) fun (i : ι) ↦ 1) 1

Tactic:
map_id

Premises used: PiTensorProduct.map_id
-- 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)
f₁ f₂ : (i : ι) → s i →ₗ[R] s i
⊢ (map (s := s) (t := s) fun (i : ι) ↦ f₁ i * f₂ i) = map (s := s) (t := s) f₁ * map (s := s) (t := s) f₂

Tactic:
map_comp f₁ f₂

Premises used: PiTensorProduct.map_comp
-- 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)
f : (i : ι) → s i →ₗ[R] s i
n : ℕ
⊢ map (s := s) (t := s) (f ^ n) = map (s := s) (t := s) f ^ n

Tactic:
map_pow mapMonoidHom _ _

Premises used: PiTensorProduct.map, map_pow, PiTensorProduct.mapMonoidHom
-- 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 : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
inst_5 : DecidableEq ι
i : ι
x : (i : ι) → s i
u : LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
h :
  ∀ (j : ι),
    Eq.{u_11 + 1} (α := t j)
      ((update (β := fun (a : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s a) (t a)) f i u j :
            (a : s j) → t j)
          (x j) :
        t j)
      (update (β := t) (fun (j : ι) ↦ (f j : (a : s j) → t j) (x j)) i ((u : (a : s i) → t i) (x i)) j : t j)
⊢ Eq (α := (j : ι) → t j)
    (fun (j : ι) ↦
      (update (β := fun (a : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s a) (t a)) f i u j : (a : s j) → t j)
        (x j))
    (update (β := t) (fun (j : ι) ↦ (f j : (a : s j) → t j) (x j)) i ((u : (a : s i) → t i) (x i)))

Tactic:
ext j
-- 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 : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
inst_5 : DecidableEq ι
i : ι
x : (i : ι) → s i
u : LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
j : ι
⊢ Eq.{u_11 + 1} (α := t j)
    ((update (β := fun (a : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s a) (t a)) f i u j : (a : s j) → t j)
        (x j) :
      t j)
    (update (β := t) (fun (j : ι) ↦ (f j : (a : s j) → t j) (x j)) i ((u : (a : s i) → t i) (x i)) j : t j)

Tactic:
apply_update (fun i F => F (x i)) f i u j

Premises used: Function.apply_update
-- 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 : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
inst_5 : DecidableEq ι
i : ι
x : (i : ι) → s i
u : LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
j : ι
⊢ Eq.{u_11 + 1} (α := t j)
    ((update (β := fun (a : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s a) (t a)) f i u j : (a : s j) → t j)
        (x j) :
      t j)
    (update (β := t) (fun (j : ι) ↦ (f j : (a : s j) → t j) (x j)) i ((u : (a : s i) → t i) (x i)) j : t j)

Tactic:
exact apply_update (fun i F => F (x i)) f i u j

Premises used: Function.apply_update
-- 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 : ι) → 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)
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)
⊢ 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)

Tactic:
ext x
-- 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 : ι) → 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)
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:
simp only [LinearMap.compMultilinearMap_apply, map_tprod, map_add_smul_aux, LinearMap.add_apply,
    MultilinearMap.map_update_add]

Premises used: MultilinearMap.map_update_add, LinearMap.add_apply, PiTensorProduct.map_tprod, _private.0.PiTensorProduct.map_add_smul_aux, LinearMap.compMultilinearMap_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 : ι) → 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)
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)
⊢ 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)

Tactic:
ext x
-- 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 : ι) → 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)
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:
simp only [LinearMap.compMultilinearMap_apply, map_tprod, map_add_smul_aux, LinearMap.smul_apply,
    MultilinearMap.map_update_smul]

Premises used: MultilinearMap.map_update_smul, LinearMap.smul_apply, PiTensorProduct.map_tprod, _private.0.PiTensorProduct.map_add_smul_aux, LinearMap.compMultilinearMap_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 : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
x : (i : ι) → s i
⊢ Eq (α := ⨂[R] (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) :
            (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), t i) :
          (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), t i)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) x) :
      ⨂[R] (i : ι), t i)
    (⨂ₜ[R] (i : ι), (f i : (a : s i) → t i) (x i) : ⨂[R] (i : ι), t i)

Tactic:
simp [piTensorHomMap]

Premises used: PiTensorProduct.piTensorHomMap
-- 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 : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
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)
⊢ (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

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)
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)
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:
simp
-- 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)
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)
⊢ 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

Tactic:
ext
-- 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 : ι) → 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:
simp
-- 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)
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)
⊢ 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

Tactic:
ext