awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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)
⊢ (↑(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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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)
⊢ 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)
have 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)
Tactic: apply ContinuousLinearMap.coe_injective
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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)
⊢ (↑(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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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
⊢ 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))
have 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)
Tactic: apply ContinuousLinearMap.coe_injective
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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 : ι) ↦ ContinuousLinearMap.id 𝕜 (E i))
    (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))
have 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)
Tactic: apply ContinuousLinearMap.coe_injective
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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) →ₗ[𝕜] ⨂[𝕜] (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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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)
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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)
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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)
⊢ norm (E := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i) (mapL (E := E) (E' := E') f) ≤ ∏ i : ι, ‖f i‖
have refine : ∀ (x : ⨂[𝕜] (i : ι), E i),
  norm (E := ⨂[𝕜] (i : ι), E' i)
      ((mapL (E := E) (E' := E') f : (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i) x : ⨂[𝕜] (i : ι), E' i) ≤
    (∏ i : ι, ‖f i‖) * ‖x‖
Tactic: refine (ContinuousLinearMap.opNorm_le_iff (by positivity)).mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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
⊢ norm (E := ⨂[𝕜] (i : ι), E' i)
      ((mapL (E := E) (E' := E') f : (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E' i) x : ⨂[𝕜] (i : ι), E' i) ≤
    (∏ i : ι, ‖f i‖) * ‖x‖
have apply : norm (E := ContinuousMultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E' i))
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := E) (M₁' := E') (tprodL 𝕜 (E := E')) f) ≤
  ∏ i : ι, ‖f i‖
Tactic: apply le_trans (norm_eval_le_projectiveSeminorm ..) (mul_le_mul_of_nonneg_right _ (norm_nonneg x))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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
⊢ norm (E := ContinuousMultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E' i))
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := E) (M₁' := E') (tprodL 𝕜 (E := E')) f) ≤
    ∏ i : ι, ‖f i‖
have refine : ∀ (m : (i : ι) → E i),
  norm (E := ⨂[𝕜] (i : ι), E' i)
      ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := E) (M₁' := E') (tprodL 𝕜 (E := E')) f :
            (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E' i)
          m :
        ⨂[𝕜] (i : ι), E' i) ≤
    HMul.hMul (α := ℝ) (∏ i : ι, ‖f i‖) (∏ i : ι, ‖m i‖)
Tactic: refine (ContinuousMultilinearMap.opNorm_le_iff (by positivity)).mpr fun m ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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
m : (i : ι) → E i
⊢ norm (E := ⨂[𝕜] (i : ι), E' i)
      ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := E) (M₁' := E') (tprodL 𝕜 (E := E')) f :
            (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E' i)
          m :
        ⨂[𝕜] (i : ι), E' i) ≤
    HMul.hMul (α := ℝ) (∏ i : ι, ‖f i‖) (∏ i : ι, ‖m i‖)
have apply : ∏ i : ι, norm.{u_1} (E := E' i) ((f i : (a : E i) → E' i) (m i) : E' i) ≤
  HMul.hMul (α := ℝ) (∏ i : ι, ‖f i‖) (∏ i : ι, ‖m i‖)
Tactic: apply le_trans (projectiveSeminorm_tprod_le fun i ↦ f i (m i))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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
m : (i : ι) → E i
⊢ ∏ i : ι, norm.{u_1} (E := E' i) ((f i : (a : E i) → E' i) (m i) : E' i) ≤
    HMul.hMul (α := ℝ) (∏ i : ι, ‖f i‖) (∏ i : ι, ‖m i‖)
have rw : LE.le (α := ℝ) (∏ i : ι, norm.{u_1} (E := E' i) ((f i : (a : E i) → E' i) (m i) : E' i)) (∏ x : ι, ‖f x‖ * ‖m x‖)
Tactic: rw [← Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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
m : (i : ι) → E i
⊢ LE.le (α := ℝ) (∏ i : ι, norm.{u_1} (E := E' i) ((f i : (a : E i) → E' i) (m i) : E' i)) (∏ x : ι, ‖f x‖ * ‖m x‖)
have h1 : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    norm.{u_1} (E := E' i) ((f i : (a : E i) → E' i) (m i) : E' i) ≤ ‖f i‖ * ‖m i‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
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
E'' : ι → Type u_2
inst_6 : (i : ι) → SeminormedAddCommGroup (E' i)
inst_7 : (i : ι) → NormedSpace.{u𝕜, u_1} 𝕜 (E' i)
inst_8 : (i : ι) → SeminormedAddCommGroup (E'' i)
inst_9 : (i : ι) → NormedSpace.{u𝕜, u_2} 𝕜 (E'' i)
g : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, u_1, u_2} (RingHom.id 𝕜) (E' i) (E'' i)
f_1 f : (i : ι) → ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i)
⊢ norm (E := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i)
      ((MultilinearMap.mk (M₁ := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i))
              (mapL (E := E) (E' := E')) ⋯ ⋯ :
            (a : (i : ι) → E i →L[𝕜] E' i) → (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i)
          f :
        (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖f i‖)
have rw : norm (E := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i)
    ((MultilinearMap.mk (M₁ := fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i))
            (mapL (E := E) (E' := E')) sorry sorry :
          (a : (i : ι) → E i →L[𝕜] E' i) → (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i)
        f :
      (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i) ≤
  ∏ i : ι, ‖f i‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
⊢ 0 ≤ projectiveSeminormAux (E := E) p
have refine : ∀ (a : ℝ),
  Membership.mem (γ := List ℝ)
      (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ ‖p.1‖ * ∏ i : ι, ‖p.2 i‖)
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p))
      a →
    0 ≤ a
Tactic: refine List.sum_nonneg fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : ℝ
⊢ Membership.mem (γ := List ℝ)
      (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ ‖p.1‖ * ∏ i : ι, ‖p.2 i‖)
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p))
      a →
    0 ≤ a
have simp : ∀ (x : 𝕜) (x_1 : (i : ι) → E i),
  Membership.mem (γ := List (𝕜 × ((i : ι) → E i)))
      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p :
        List (𝕜 × ((i : ι) → E i)))
      (x, x_1) →
    ‖x‖ * ∏ x : ι, ‖x_1 x‖ = a → 0 ≤ a
Tactic: simp only [List.mem_map, Prod.exists, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : ℝ
x : 𝕜
m : (i : ι) → E i
h_1 :
  Membership.mem (γ := List (𝕜 × ((i : ι) → E i)))
    ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p :
      List (𝕜 × ((i : ι) → E i)))
    (x, m)
h : ‖x‖ * ∏ x : ι, ‖m x‖ = a
⊢ 0 ≤ a
have simpa : 0 ≤ ‖x‖ * ∏ x : ι, ‖m x‖
Tactic: simpa [← h] using by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
⊢ ‖a • x‖ ≤ ‖a‖ * ‖x‖
have simp : LE.le (α := ℝ)
  (⨅ (p : (↑((a • x).lifts (s := E)) : Type (max (max uE uι) u𝕜))),
    projectiveSeminormAux (E := E) (↑p : FreeAddMonoid (𝕜 × ((i : ι) → E i))))
  (⨅ (i : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
    ‖a‖ * projectiveSeminormAux (E := E) (↑i : FreeAddMonoid (𝕜 × ((i : ι) → E i))))
Tactic: simp only [norm_def, Real.mul_iInf_of_nonneg (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
⊢ LE.le (α := ℝ)
    (⨅ (p : (↑((a • x).lifts (s := E)) : Type (max (max uE uι) u𝕜))),
      projectiveSeminormAux (E := E) (↑p : FreeAddMonoid (𝕜 × ((i : ι) → E i))))
    (⨅ (i : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
      ‖a‖ * projectiveSeminormAux (E := E) (↑i : FreeAddMonoid (𝕜 × ((i : ι) → E i))))
have refine : ∀ (p : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
  ⨅ (p : (↑((a • x).lifts (s := E)) : Type (max (max uE uι) u𝕜))),
      projectiveSeminormAux (E := E) (↑p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ≤
    ‖a‖ * projectiveSeminormAux (E := E) (↑p : FreeAddMonoid (𝕜 × ((i : ι) → E i)))
Tactic: refine le_ciInf fun p ↦ ?_