mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ ((fun l ↦ (lift.symm ↑l).mkContinuous ‖l‖ ⋯) ((fun f ↦ (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯) f)) x✝ = f x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ ((fun l ↦ (lift.symm ↑l).mkContinuous ‖l‖ ⋯) ((fun f ↦ (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯) f)) x✝ = f x✝
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
x✝ : (i : ι) → E i
⊢ ((↑((fun f ↦ (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯)
              ((fun l ↦ (lift.symm ↑l).mkContinuous ‖l‖ ⋯) l))).compMultilinearMap
        (tprod 𝕜))
      x✝ =
    ((↑l).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
x✝ : (i : ι) → E i
⊢ ((↑((fun f ↦ (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯)
              ((fun l ↦ (lift.symm ↑l).mkContinuous ‖l‖ ⋯) l))).compMultilinearMap
        (tprod 𝕜))
      x✝ =
    ((↑l).compMultilinearMap (tprod 𝕜)) x✝
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : (i : ι) → E i
⊢ (tprodL 𝕜).toMultilinearMap x✝ = (tprod 𝕜) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : (i : ι) → E i
⊢ (tprodL 𝕜).toMultilinearMap x✝ = (tprod 𝕜) x✝
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : ⨂[𝕜] (i : ι), E i
⊢ ((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i)) (tprodL 𝕜)) x✝ = (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : ⨂[𝕜] (i : ι), E i
⊢ ((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i)) (tprodL 𝕜)) x✝ = (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) x✝
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x✝ : (i : ι) → E i
⊢ ((↑(mapL f)).compMultilinearMap (tprod 𝕜)) x✝ = ((map fun i ↦ ↑(f i)).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x✝ : (i : ι) → E i
⊢ ((↑(mapL f)).compMultilinearMap (tprod 𝕜)) x✝ = ((map fun i ↦ ↑(f i)).compMultilinearMap (tprod 𝕜)) x✝
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
E'' : ι → Type u_6
inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)
g : (i : ι) → E' i →L[𝕜] E'' i
f : (i : ι) → E i →L[𝕜] E' i
x✝ : (i : ι) → E i
⊢ ((↑(mapL fun i ↦ g i ∘SL f i)).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑(mapL g ∘SL mapL f)).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝⁷ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
E'' : ι → Type u_6
inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)
g : (i : ι) → E' i →L[𝕜] E'' i
f : (i : ι) → E i →L[𝕜] E' i
x✝ : (i : ι) → E i
⊢ ((↑(mapL fun i ↦ g i ∘SL f i)).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑(mapL g ∘SL mapL f)).compMultilinearMap (tprod 𝕜)) x✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case hf
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
i✝ : ι
a✝ : i✝ ∈ s
⊢ 0 ≤ ‖e i✝‖

Tactic:
;

Goal state after:
case hf
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
i✝ : ι
a✝ : i✝ ∈ s
⊢ 0 ≤ ‖e i✝‖
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
x✝ : (i : ι) → E i
⊢ ((↑((liftIsometry 𝕜 E' F) h ∘SL mapL f)).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝⁷ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
x✝ : (i : ι) → E i
⊢ ((↑((liftIsometry 𝕜 E' F) h ∘SL mapL f)).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))).compMultilinearMap (tprod 𝕜)) x✝
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : (i : ι) → E i
⊢ ((↑(mapL fun i ↦ ContinuousLinearMap.id 𝕜 (E i))).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : (i : ι) → E i
⊢ ((↑(mapL fun i ↦ ContinuousLinearMap.id 𝕜 (E i))).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑(ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i))).compMultilinearMap (tprod 𝕜)) x✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case hg
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
i✝ : ι
a✝ : i✝ ∈ s
⊢ 0 ≤ ‖f i✝‖

Tactic:
;

Goal state after:
case hg
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
i✝ : ι
a✝ : i✝ ∈ s
⊢ 0 ≤ ‖f i✝‖
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁹ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E' : ι → Type u_5
E'' : ι → Type u_6
inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)
g : (i : ι) → E' i →L[𝕜] E'' i
f✝ f : (i : ι) → E i →L[𝕜] E' i
⊢ ‖{ toFun := mapL, map_update_add' := ⋯, map_update_smul' := ⋯ } f‖ ≤ ∏ i, ‖f i‖

Tactic:
;

Goal state after:
ι : Type u_1
inst✝⁹ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E' : ι → Type u_5
E'' : ι → Type u_6
inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)
g : (i : ι) → E' i →L[𝕜] E'' i
f✝ f : (i : ι) → E i →L[𝕜] E' i
⊢ ‖{ toFun := mapL, map_update_add' := ⋯, map_update_smul' := ⋯ } f‖ ≤ ∏ i, ‖f i‖
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
⊢ ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ r.toReal ≤ K ^ r.toReal * C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)

Tactic:
by
  have hpqr := hpqr.toReal r hp hq
  have hr := hpqr.pos'
  suffices ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal ≤
      C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal) from calc
    ∑ i ∈ s, ‖B i (e i) (f i)‖ ^ r.toReal
    _ ≤ K ^ r.toReal * ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal := by
      rw [s.mul_sum]
      gcongr with i hi
      rw [← Real.mul_rpow (by positivity) (by positivity), ← mul_assoc]
      gcongr
      exact (B i (e i)).le_of_opNorm_le ((B i).le_of_opNorm_le (hBK i) _) _
    _ ≤ _ := by
      rw [mul_assoc]
      gcongr
  calc
    _ ≤ (∑ i ∈ s, ‖e i‖ ^ p.toReal) ^ (r.toReal / p.toReal) *
        (∑ i ∈ s, ‖f i‖ ^ q.toReal) ^ (r.toReal / q.toReal) := by
      apply Real.Lr_rpow_le_Lp_mul_Lq_of_nonneg s hpqr <;> (intros; positivity)
    _ ≤ _ := by
      gcongr
      · exact hCe s
      · exact hDf s

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m₁✝ m₂✝ : ↥(lp E p)
n✝ : ↥(lp F q)
⊢ holder r B hBK (m₁✝ + m₂✝) n✝ = holder r B hBK m₁✝ n✝ + holder r B hBK m₂✝ n✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m₁✝ m₂✝ : ↥(lp E p)
n✝ : ↥(lp F q)
⊢ holder r B hBK (m₁✝ + m₂✝) n✝ = holder r B hBK m₁✝ n✝ + holder r B hBK m₂✝ n✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m₁✝ m₂✝ : ↥(lp E p)
n✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK (m₁✝ + m₂✝) n✝) x✝ = ↑(holder r B hBK m₁✝ n✝ + holder r B hBK m₂✝ n✝) x✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m₁✝ m₂✝ : ↥(lp E p)
n✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK (m₁✝ + m₂✝) n✝) x✝ = ↑(holder r B hBK m₁✝ n✝ + holder r B hBK m₂✝ n✝) x✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
⊢ holder r B hBK (c✝ • m✝) n✝ = c✝ • holder r B hBK m✝ n✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
⊢ holder r B hBK (c✝ • m✝) n✝ = c✝ • holder r B hBK m✝ n✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK (c✝ • m✝) n✝) x✝ = ↑(c✝ • holder r B hBK m✝ n✝) x✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK (c✝ • m✝) n✝) x✝ = ↑(c✝ • holder r B hBK m✝ n✝) x✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m✝ : ↥(lp E p)
n₁✝ n₂✝ : ↥(lp F q)
⊢ holder r B hBK m✝ (n₁✝ + n₂✝) = holder r B hBK m✝ n₁✝ + holder r B hBK m✝ n₂✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m✝ : ↥(lp E p)
n₁✝ n₂✝ : ↥(lp F q)
⊢ holder r B hBK m✝ (n₁✝ + n₂✝) = holder r B hBK m✝ n₁✝ + holder r B hBK m✝ n₂✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m✝ : ↥(lp E p)
n₁✝ n₂✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK m✝ (n₁✝ + n₂✝)) x✝ = ↑(holder r B hBK m✝ n₁✝ + holder r B hBK m✝ n₂✝) x✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
m✝ : ↥(lp E p)
n₁✝ n₂✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK m✝ (n₁✝ + n₂✝)) x✝ = ↑(holder r B hBK m✝ n₁✝ + holder r B hBK m✝ n₂✝) x✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
⊢ holder r B hBK m✝ (c✝ • n✝) = c✝ • holder r B hBK m✝ n✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
⊢ holder r B hBK m✝ (c✝ • n✝) = c✝ • holder r B hBK m✝ n✝
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK m✝ (c✝ • n✝)) x✝ = ↑(c✝ • holder r B hBK m✝ n✝) x✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
c✝ : 𝕜
m✝ : ↥(lp E p)
n✝ : ↥(lp F q)
x✝ : ι
⊢ ↑(holder r B hBK m✝ (c✝ • n✝)) x✝ = ↑(c✝ • holder r B hBK m✝ n✝) x✝