-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_le_of_tendsto {C : ℝ} {F : ι → lp E p} (hCF : ∀ᶠ k in l, ‖F k‖ ≤ C) {f : lp E p}
    (hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) : ‖f‖ ≤ C

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
⊢ ‖f‖ ≤ C

Tactic:
obtain ⟨i, hi⟩ := hCF.exists

Result:
case intro
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C

Proof state:
case intro.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
⊢ ‖f‖ ≤ C

Tactic:
have : 0 < p := zero_lt_one.trans_le _i.elim

Result:
case intro.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
⊢ ‖f‖ ≤ C

Proof state:
case intro.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
hp' : 0 < p.toReal
⊢ ∀ (s : Finset α), ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
exact sum_rpow_le_of_tendsto hp.ne hCF hf

Result:
no goals

Proof state:
case intro.inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E ⊤)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
apply norm_le_of_forall_le hC

Result:
case intro.inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E ⊤)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ∀ (i : α), ‖↑f i‖ ≤ C

Proof state:
case intro.inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E ⊤)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ∀ (i : α), ‖↑f i‖ ≤ C

Tactic:
exact norm_apply_le_of_tendsto hCF hf

Result:
no goals

Proof state:
case intro.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
⊢ ‖f‖ ≤ C

Tactic:
have hp' : 0 < p.toReal := ENNReal.toReal_pos this.ne' hp.ne

Result:
case intro.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
hp' : 0 < p.toReal
⊢ ‖f‖ ≤ C

Proof state:
case intro
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
have hC : 0 ≤ C := (norm_nonneg _).trans hi

Result:
case intro
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
⊢ ‖f‖ ≤ C

Proof state:
case intro
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
⊢ ‖f‖ ≤ C

Tactic:
rcases eq_top_or_lt_top p with (rfl | hp)

Result:
case intro.inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E ⊤)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C

case intro.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
⊢ ‖f‖ ≤ C

Proof state:
case intro.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
hp' : 0 < p.toReal
⊢ ‖f‖ ≤ C

Tactic:
apply norm_le_of_forall_sum_le hp' hC

Result:
case intro.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
hp' : 0 < p.toReal
⊢ ∀ (s : Finset α), ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal