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)
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‖
⊢ norm (E := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i) (mapL (E := E) (E' := E') f) ≤ ∏ i : ι, ‖f i‖

Tactic:
refine (ContinuousLinearMap.opNorm_le_iff (by positivity)).mpr fun x ↦ ?_

Premises used: Iff.mpr, ContinuousLinearMap.opNorm_le_iff
-- 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
apply :
  norm (E := ContinuousMultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E' i))
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := E) (M₁' := E') (tprodL 𝕜 (E := E')) f) ≤
    ∏ i : ι, ‖f 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:
apply le_trans (norm_eval_le_projectiveSeminorm ..) (mul_le_mul_of_nonneg_right _ (norm_nonneg x))

Premises used: mul_le_mul_of_nonneg_right, PiTensorProduct.norm_eval_le_projectiveSeminorm, norm_nonneg, le_trans
-- 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
⊢ LE.le (α := ℝ) 0 (∏ i : ι, ‖f i‖)

Tactic:
positivity
-- 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
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‖)
⊢ norm (E := ContinuousMultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E' i))
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := E) (M₁' := E') (tprodL 𝕜 (E := E')) f) ≤
    ∏ i : ι, ‖f i‖

Tactic:
refine (ContinuousMultilinearMap.opNorm_le_iff (by positivity)).mpr fun m ↦ ?_

Premises used: Iff.mpr, ContinuousMultilinearMap.opNorm_le_iff
-- 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
m : (i : ι) → E i
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‖)
⊢ 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:
apply le_trans (projectiveSeminorm_tprod_le fun i ↦ f i (m i))

Premises used: PiTensorProduct.projectiveSeminorm_tprod_le, DFunLike.coe, le_trans
-- 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
m : (i : ι) → E i
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‖)
⊢ ∏ 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:
rw [← Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib
-- 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
m : (i : ι) → E i
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‖
⊢ 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:
gcongr
-- 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
m : (i : ι) → E i
i : ι
h : 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:
ContinuousLinearMap.le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- 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
m : (i : ι) → E i
i : ι
h : 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:
exact ContinuousLinearMap.le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- 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
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)
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')) ⋯ ⋯ :
            (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‖
⊢ 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‖)

Tactic:
rw [one_mul]

Premises used: one_mul
-- 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
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) ≤
    ∏ i : ι, ‖f i‖

Tactic:
mapL_opNorm f

Premises used: PiTensorProduct.mapL, PiTensorProduct.mapL_opNorm
-- 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
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) ≤
    ∏ i : ι, ‖f i‖

Tactic:
exact mapL_opNorm f

Premises used: PiTensorProduct.mapL_opNorm
-- 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)
⊢ norm (E :=
      ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ ContinuousLinearMap.{u𝕜, u𝕜, uE, u_1} (RingHom.id 𝕜) (E i) (E' i))
        ((⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E' i))
      (mapLMultilinear 𝕜 E E') ≤
    1

Tactic:
MultilinearMap.mkContinuous_norm_le _ zero_le_one _

Premises used: PiTensorProduct.mapLMultilinear, zero_le_one, MultilinearMap.mkContinuous_norm_le
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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

Tactic:
List.sum_nonneg fun a ↦ ?_

Premises used: PiTensorProduct.projectiveSeminormAux, List.sum_nonneg
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
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
⊢ 0 ≤ projectiveSeminormAux (E := E) p

Tactic:
refine List.sum_nonneg fun a ↦ ?_

Premises used: List.sum_nonneg
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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 : ℝ
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
⊢ 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:
simp only [List.mem_map, Prod.exists, forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index, List.mem_map, Prod.exists
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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
_ :
  Membership.mem (γ := List (𝕜 × ((i : ι) → E i)))
      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p :
        List (𝕜 × ((i : ι) → E i)))
      (x, m) →
    ‖x‖ * ∏ x : ι, ‖m x‖ = a → 0 ≤ a
⊢ Membership.mem (γ := List (𝕜 × ((i : ι) → E i)))
      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p :
        List (𝕜 × ((i : ι) → E i)))
      (x, m) →
    ‖x‖ * ∏ x : ι, ‖m x‖ = a → 0 ≤ a

Tactic:
_
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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 ≤ ‖x‖ * ∏ x : ι, ‖m x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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
simpa : 0 ≤ ‖x‖ * ∏ x : ι, ‖m x‖
⊢ 0 ≤ a

Tactic:
simpa [← h] using by positivity
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))
⊢ projectiveSeminormAux (E := E) (p + q) ≤ projectiveSeminormAux (E := E) p + projectiveSeminormAux (E := E) q

Tactic:
simp [projectiveSeminormAux]

Premises used: PiTensorProduct.projectiveSeminormAux
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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 : 𝕜
⊢ projectiveSeminormAux.{uι, u𝕜, uE} (𝕜 := 𝕜) (E := E)
      ((FreeAddMonoid.map fun (y : 𝕜 × ((i : ι) → E i)) ↦ (a * y.1, y.2) :
          (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → FreeAddMonoid (𝕜 × ((i : ι) → E i)))
        p) =
    ‖a‖ * projectiveSeminormAux (E := E) p

Tactic:
simp [projectiveSeminormAux, Function.comp_def, mul_assoc, List.sum_map_mul_left]

Premises used: mul_assoc, PiTensorProduct.projectiveSeminormAux, List.sum_map_mul_left, Function.comp_def
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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)
x : ⨂[𝕜] (i : ι), E i
⊢ Membership.mem (γ := Set ℝ)
    (lowerBounds
      (Set.range fun (p : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))) ↦
        projectiveSeminormAux (E := E) (↑p : FreeAddMonoid (𝕜 × ((i : ι) → E i)))))
    0

Tactic:
simp [mem_lowerBounds, projectiveSeminormAux_nonneg]

Premises used: mem_lowerBounds, PiTensorProduct.projectiveSeminormAux_nonneg
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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)
x : ⨂[𝕜] (i : ι), E i
⊢ ‖x‖ =
    ⨅ (p : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
      projectiveSeminormAux (E := E) (↑p : FreeAddMonoid (𝕜 × ((i : ι) → E i)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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)
⊢ norm (E := ⨂[𝕜] (i : ι), E i) 0 = 0

Tactic:
le_antisymm (ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨0, lifts_zero⟩)
    (le_ciInf (fun p ↦ projectiveSeminormAux_nonneg p.val))

Premises used: PiTensorProduct.bddBelow_projectiveSemiNormAux, PiTensorProduct.lifts_zero, Subtype.mk, le_ciInf, le_antisymm, ciInf_le, PiTensorProduct.projectiveSeminormAux_nonneg, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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)
x y : ⨂[𝕜] (i : ι), E i
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖

Tactic:
le_ciInf_add_ciInf (fun p q ↦ ciInf_le_of_le (bddBelow_projectiveSemiNormAux _)
    ⟨p.1 + q.1, lifts_add p.2 q.2⟩ (projectiveSeminormAux_add_le p.1 q.1))

Premises used: le_ciInf_add_ciInf, PiTensorProduct.lifts_add, PiTensorProduct.bddBelow_projectiveSemiNormAux, ciInf_le_of_le, Subtype.mk, HAdd.hAdd, Subtype.val, Subtype.property, PiTensorProduct.projectiveSeminormAux_add_le
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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
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))))
⊢ ‖a • x‖ ≤ ‖a‖ * ‖x‖

Tactic:
simp only [norm_def, Real.mul_iInf_of_nonneg (norm_nonneg _)]

Premises used: PiTensorProduct.norm_def, Real.mul_iInf_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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))))

Tactic:
le_ciInf fun p ↦ ?_

Premises used: le_ciInf
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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
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)))
⊢ 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:
refine le_ciInf fun p ↦ ?_

Premises used: le_ciInf
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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
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:
simpa [projectiveSeminormAux_smul] using
    ciInf_le_of_le (bddBelow_projectiveSemiNormAux _) ⟨_, lifts_smul p.2 a⟩ (le_refl _)

Premises used: le_refl, PiTensorProduct.lifts_smul, PiTensorProduct.projectiveSeminormAux_smul, PiTensorProduct.bddBelow_projectiveSemiNormAux, ciInf_le_of_le, Subtype.mk, Subtype.property
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
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)
x : ⨂[𝕜] (i : ι), E i
⊢ Eq (α := ℝ) ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x : ℝ)
    (⨅ (p : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
        projectiveSeminormAux (E := E) (↑p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) :
      ℝ)

Tactic:
rfl

Premises used: iInf, rfl