awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
H :
  ∀ (x : (i : ι) → E i),
    Eq (α := ⨂[𝕜] (i : ι), E' i)
      (((↑(mapL (E := E) (E' := E') f) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E' i).compMultilinearMap (M₁ := E)
              (tprod 𝕜 (s := E)) :
            (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E' i)
          x :
        ⨂[𝕜] (i : ι), E' i)
      ((LinearMap.compMultilinearMap (M₁ := E) (map (s := E) (t := E') fun (i : ι) ↦ (↑(f i) : E i →ₗ[𝕜] E' i))
              (tprod 𝕜 (s := E)) :
            (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E' i)
          x :
        ⨂[𝕜] (i : ι), E' i)
⊢ (↑(mapL (E := E) (E' := E') f) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E' i) =
    map (s := E) (t := E') fun (i : ι) ↦ (↑(f i) : E i →ₗ[𝕜] E' i)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
x : (i : ι) → E i
⊢ Eq (α := ⨂[𝕜] (i : ι), E' i)
    (((↑(mapL (E := E) (E' := E') f) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E' i).compMultilinearMap (M₁ := E)
            (tprod 𝕜 (s := E)) :
          (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E' i)
        x :
      ⨂[𝕜] (i : ι), E' i)
    ((LinearMap.compMultilinearMap (M₁ := E) (map (s := E) (t := E') fun (i : ι) ↦ (↑(f i) : E i →ₗ[𝕜] E' i))
            (tprod 𝕜 (s := E)) :
          (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E' i)
        x :
      ⨂[𝕜] (i : ι), E' i)

Tactic:
simp [mapL]

Premises used: PiTensorProduct.mapL
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
x : ⨂[𝕜] (i : ι), E i
⊢ Eq (α := ⨂[𝕜] (i : ι), E' i)
    ((mapL (E := E) (E' := E') f : (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i) x : ⨂[𝕜] (i : ι), E' i)
    ((map (s := E) (t := E') fun (i : ι) ↦ (↑(f i) : E i →ₗ[𝕜] E' i) : (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i) x :
      ⨂[𝕜] (i : ι), E' i)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
E'' : ι → Type u_2
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
inst_6 : (i : ι) → SeminormedAddCommGroup (E'' i)
inst_7 : (i : ι) → NormedSpace.{u𝕜, u_2} 𝕜 (E'' i)
g : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, u_1, u_2} (RingHom.id 𝕜) (E' i) (E'' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
a :
  (↑(mapL (E := E) (E' := E'') fun (i : ι) ↦ g i ∘SL f i) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E'' i) =
    (↑(mapL (E := E') (E' := E'') g ∘SL mapL (E := E) (E' := E') f) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E'' i)
⊢ Eq (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E'' i) (mapL (E := E) (E' := E'') fun (i : ι) ↦ g i ∘SL f i)
    (mapL (E := E') (E' := E'') g ∘SL mapL (E := E) (E' := E') f)

Tactic:
apply ContinuousLinearMap.coe_injective

Premises used: ContinuousLinearMap.coe_injective
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
E'' : ι → Type u_2
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
inst_6 : (i : ι) → SeminormedAddCommGroup (E'' i)
inst_7 : (i : ι) → NormedSpace.{u𝕜, u_2} 𝕜 (E'' i)
g : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, u_1, u_2} (RingHom.id 𝕜) (E' i) (E'' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
a :
  ∀ (x : (i : ι) → E i),
    Eq (α := ⨂[𝕜] (i : ι), E'' i)
      ((LinearMap.compMultilinearMap (M₁ := E)
              (↑(mapL (E := E) (E' := E'') fun (i : ι) ↦ g i ∘SL f i) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E'' i)
              (tprod 𝕜 (s := E)) :
            (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E'' i)
          x :
        ⨂[𝕜] (i : ι), E'' i)
      (((↑(mapL (E := E') (E' := E'') g ∘SL mapL (E := E) (E' := E') f) :
                  (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E'' i).compMultilinearMap
              (M₁ := E) (tprod 𝕜 (s := E)) :
            (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E'' i)
          x :
        ⨂[𝕜] (i : ι), E'' i)
⊢ (↑(mapL (E := E) (E' := E'') fun (i : ι) ↦ g i ∘SL f i) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E'' i) =
    (↑(mapL (E := E') (E' := E'') g ∘SL mapL (E := E) (E' := E') f) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E'' i)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
E'' : ι → Type u_2
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
inst_6 : (i : ι) → SeminormedAddCommGroup (E'' i)
inst_7 : (i : ι) → NormedSpace.{u𝕜, u_2} 𝕜 (E'' i)
g : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, u_1, u_2} (RingHom.id 𝕜) (E' i) (E'' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
x : (i : ι) → E i
⊢ Eq (α := ⨂[𝕜] (i : ι), E'' i)
    ((LinearMap.compMultilinearMap (M₁ := E)
            (↑(mapL (E := E) (E' := E'') fun (i : ι) ↦ g i ∘SL f i) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E'' i)
            (tprod 𝕜 (s := E)) :
          (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E'' i)
        x :
      ⨂[𝕜] (i : ι), E'' i)
    (((↑(mapL (E := E') (E' := E'') g ∘SL mapL (E := E) (E' := E') f) :
                (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E'' i).compMultilinearMap
            (M₁ := E) (tprod 𝕜 (s := E)) :
          (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E'' i)
        x :
      ⨂[𝕜] (i : ι), E'' i)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
E' : ι → Type u_1
inst_6 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_7 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
h : ContinuousMultilinearMap 𝕜 E' F
a :
  Eq (α := (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
    (↑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          ((liftIsometry 𝕜 E' F : (a : ContinuousMultilinearMap 𝕜 E' F) → (⨂[𝕜] (i : ι), E' i) →L[𝕜] F) h)
          (mapL (E := E) (E' := E') f)) :
      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
    (↑((liftIsometry 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →L[𝕜] F)
          (h.compContinuousLinearMap (M₁ := E) (M₁' := E') f)) :
      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
⊢ Eq (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] F)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
      ((liftIsometry 𝕜 E' F : (a : ContinuousMultilinearMap 𝕜 E' F) → (⨂[𝕜] (i : ι), E' i) →L[𝕜] F) h)
      (mapL (E := E) (E' := E') f))
    ((liftIsometry 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →L[𝕜] F)
      (h.compContinuousLinearMap (M₁ := E) (M₁' := E') f))

Tactic:
apply ContinuousLinearMap.coe_injective

Premises used: ContinuousLinearMap.coe_injective
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
E' : ι → Type u_1
inst_6 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_7 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
h : ContinuousMultilinearMap 𝕜 E' F
a :
  ∀ (x : (i : ι) → E i),
    Eq.{uF + 1} (α := F)
      ((LinearMap.compMultilinearMap (M₁ := E)
              (↑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                    ((liftIsometry 𝕜 E' F : (a : ContinuousMultilinearMap 𝕜 E' F) → (⨂[𝕜] (i : ι), E' i) →L[𝕜] F) h)
                    (mapL (E := E) (E' := E') f)) :
                (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
              (tprod 𝕜 (s := E)) :
            (a : (i : ι) → E i) → F)
          x :
        F)
      ((LinearMap.compMultilinearMap (M₁ := E)
              (↑((liftIsometry 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →L[𝕜] F)
                    (h.compContinuousLinearMap (M₁ := E) (M₁' := E') f)) :
                (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
              (tprod 𝕜 (s := E)) :
            (a : (i : ι) → E i) → F)
          x :
        F)
⊢ Eq (α := (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
    (↑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          ((liftIsometry 𝕜 E' F : (a : ContinuousMultilinearMap 𝕜 E' F) → (⨂[𝕜] (i : ι), E' i) →L[𝕜] F) h)
          (mapL (E := E) (E' := E') f)) :
      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
    (↑((liftIsometry 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →L[𝕜] F)
          (h.compContinuousLinearMap (M₁ := E) (M₁' := E') f)) :
      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
E' : ι → Type u_1
inst_6 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_7 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
h : ContinuousMultilinearMap 𝕜 E' F
x : (i : ι) → E i
⊢ Eq.{uF + 1} (α := F)
    ((LinearMap.compMultilinearMap (M₁ := E)
            (↑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                  ((liftIsometry 𝕜 E' F : (a : ContinuousMultilinearMap 𝕜 E' F) → (⨂[𝕜] (i : ι), E' i) →L[𝕜] F) h)
                  (mapL (E := E) (E' := E') f)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
            (tprod 𝕜 (s := E)) :
          (a : (i : ι) → E i) → F)
        x :
      F)
    ((LinearMap.compMultilinearMap (M₁ := E)
            (↑((liftIsometry 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →L[𝕜] F)
                  (h.compContinuousLinearMap (M₁ := E) (M₁' := E') f)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
            (tprod 𝕜 (s := E)) :
          (a : (i : ι) → E i) → F)
        x :
      F)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
a :
  Eq (α := (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)
    (↑(mapL (E := E) (E' := E) fun (i : ι) ↦ ContinuousLinearMap.id 𝕜 (E i)) :
      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)
    (↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)
⊢ Eq (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
    (mapL (E := E) (E' := E) fun (i : ι) ↦ ContinuousLinearMap.id 𝕜 (E i))
    (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))

Tactic:
apply ContinuousLinearMap.coe_injective

Premises used: ContinuousLinearMap.coe_injective
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
a :
  ∀ (x : (i : ι) → E i),
    Eq (α := ⨂[𝕜] (i : ι), E i)
      ((LinearMap.compMultilinearMap (M₁ := E)
              (↑(mapL (E := E) (E' := E) fun (i : ι) ↦ ContinuousLinearMap.id 𝕜 (E i)) :
                (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)
              (tprod 𝕜 (s := E)) :
            (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i)
          x :
        ⨂[𝕜] (i : ι), E i)
      ((LinearMap.compMultilinearMap (M₁ := E)
              (↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)
              (tprod 𝕜 (s := E)) :
            (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i)
          x :
        ⨂[𝕜] (i : ι), E i)
⊢ Eq (α := (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)
    (↑(mapL (E := E) (E' := E) fun (i : ι) ↦ ContinuousLinearMap.id 𝕜 (E i)) :
      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)
    (↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
x : (i : ι) → E i
⊢ Eq (α := ⨂[𝕜] (i : ι), E i)
    ((LinearMap.compMultilinearMap (M₁ := E)
            (↑(mapL (E := E) (E' := E) fun (i : ι) ↦ ContinuousLinearMap.id 𝕜 (E i)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)
            (tprod 𝕜 (s := E)) :
          (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i)
        x :
      ⨂[𝕜] (i : ι), E i)
    ((LinearMap.compMultilinearMap (M₁ := E)
            (↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] ⨂[𝕜] (i : ι), E i)
            (tprod 𝕜 (s := E)) :
          (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i)
        x :
      ⨂[𝕜] (i : ι), E i)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ Eq (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i) (mapL (E := E) (E' := E) fun (i : ι) ↦ 1) 1

Tactic:
mapL_id

Premises used: PiTensorProduct.mapL_id
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
f₁ f₂ : (i : ι) → E i →L[𝕜] E i
⊢ (mapL (E := E) (E' := E) fun (i : ι) ↦ f₁ i * f₂ i) =
    HMul.hMul (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i) (mapL (E := E) (E' := E) f₁)
      (mapL (E := E) (E' := E) f₂)

Tactic:
mapL_comp f₁ f₂

Premises used: PiTensorProduct.mapL_comp
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
f : (i : ι) → E i →L[𝕜] E i
n : ℕ
⊢ mapL (E := E) (E' := E) (f ^ n) =
    HPow.hPow (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i) (mapL (E := E) (E' := E) f) n

Tactic:
MonoidHom.map_pow mapLMonoidHom f n

Premises used: PiTensorProduct.mapL, MonoidHom.map_pow
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
𝕜 : Type u𝕜
inst : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
inst_3 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_4 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
inst_5 : DecidableEq ι
i : ι
u : ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
⊢ Eq (α := (j : ι) → LinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E j) (E' j))
    (fun (j : ι) ↦
      (↑(update (β := fun (a : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E a) (E' a)) f i u j) :
        E j →ₗ[𝕜] E' j))
    (update (β := fun (j : ι) ↦ LinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E j) (E' j))
      (fun (j : ι) ↦ (↑(f j) : E j →ₗ[𝕜] E' j)) i (↑u : E i →ₗ[𝕜] E' i))

Tactic:
grind
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
inst_6 : DecidableEq ι
i : ι
u v : ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
h :
  ∀ (x : ⨂[𝕜] (i : ι), E i),
    Eq (α := ⨂[𝕜] (i : ι), E' i)
      ((mapL (E := E) (E' := E')
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i
                (u + v)) :
            (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i)
          x :
        ⨂[𝕜] (i : ι), E' i)
      ((HAdd.hAdd (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i)
              (mapL (E := E) (E' := E')
                (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i u))
              (mapL (E := E) (E' := E')
                (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i v)) :
            (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i)
          x :
        ⨂[𝕜] (i : ι), E' i)
⊢ mapL (E := E) (E' := E')
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i (u + v)) =
    HAdd.hAdd (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i)
      (mapL (E := E) (E' := E')
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i u))
      (mapL (E := E) (E' := E')
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i v))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
inst_6 : DecidableEq ι
i : ι
u v : ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
x : ⨂[𝕜] (i : ι), E i
⊢ Eq (α := ⨂[𝕜] (i : ι), E' i)
    ((mapL (E := E) (E' := E')
            (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i
              (u + v)) :
          (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i)
        x :
      ⨂[𝕜] (i : ι), E' i)
    ((HAdd.hAdd (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i)
            (mapL (E := E) (E' := E')
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i u))
            (mapL (E := E) (E' := E')
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i v)) :
          (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i)
        x :
      ⨂[𝕜] (i : ι), E' i)

Tactic:
simp [mapL_add_smul_aux, PiTensorProduct.map_update_add]

Premises used: _private.0.PiTensorProduct.mapL_add_smul_aux, PiTensorProduct.map_update_add
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
inst_6 : DecidableEq ι
i : ι
c : 𝕜
u : ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
h :
  ∀ (x : ⨂[𝕜] (i : ι), E i),
    Eq (α := ⨂[𝕜] (i : ι), E' i)
      ((mapL (E := E) (E' := E')
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i
                (c • u)) :
            (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i)
          x :
        ⨂[𝕜] (i : ι), E' i)
      ((HSMul.hSMul (β := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i) c
              (mapL (E := E) (E' := E')
                (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i u)) :
            (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i)
          x :
        ⨂[𝕜] (i : ι), E' i)
⊢ mapL (E := E) (E' := E')
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i (c • u)) =
    HSMul.hSMul (β := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i) c
      (mapL (E := E) (E' := E')
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i u))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
inst_6 : DecidableEq ι
i : ι
c : 𝕜
u : ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
x : ⨂[𝕜] (i : ι), E i
⊢ Eq (α := ⨂[𝕜] (i : ι), E' i)
    ((mapL (E := E) (E' := E')
            (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i
              (c • u)) :
          (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i)
        x :
      ⨂[𝕜] (i : ι), E' i)
    ((HSMul.hSMul (β := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i) c
            (mapL (E := E) (E' := E')
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)) f i u)) :
          (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i)
        x :
      ⨂[𝕜] (i : ι), E' i)

Tactic:
simp [mapL_add_smul_aux, PiTensorProduct.map_update_smul]

Premises used: _private.0.PiTensorProduct.mapL_add_smul_aux, PiTensorProduct.map_update_smul
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
E' : ι → Type u_1
inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_5 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
⊢ LE.le (α := ℝ) 0 (∏ i : ι, ‖f i‖)

Tactic:
positivity