-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem memℓp_of_tendsto {F : ι → lp E p} (hF : Bornology.IsBounded (Set.range F)) {f : ∀ a, E a}
    (hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) : Memℓp f p

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)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ Memℓp f p

Tactic:
apply memℓp_gen'

Result:
case intro.inr.hf
α : 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)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ?intro.inr.C

case intro.inr.C
α : 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)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ ℝ

Proof state:
case h
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
f : (a : α) → E a
C : ℝ
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hF : Bornology.IsBounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ C ∈ upperBounds (Set.range fun i => ‖f i‖)

Tactic:
rintro _ ⟨a, rfl⟩

Result:
case h.intro
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
f : (a : α) → E a
C : ℝ
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hF : Bornology.IsBounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF : ∀ (k : ι), ‖F k‖ ≤ C
a : α
⊢ (fun i => ‖f i‖) a ≤ C

Proof state:
case intro.inr.hf
α : 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)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ?intro.inr.C

case intro.inr.C
α : 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)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ ℝ

Tactic:
exact sum_rpow_le_of_tendsto hp.ne (Eventually.of_forall 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
f : (a : α) → E a
C : ℝ
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hF : Bornology.IsBounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ Memℓp f ⊤

Tactic:
apply memℓp_infty

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

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

Tactic:
use C

Result:
case h
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
f : (a : α) → E a
C : ℝ
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hF : Bornology.IsBounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ C ∈ upperBounds (Set.range fun i => ‖f i‖)

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)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
⊢ Memℓp f p

Tactic:
obtain ⟨C, hCF⟩ : ∃ C, ∀ k, ‖F k‖ ≤ C := hF.exists_norm_le.imp fun _ ↦ Set.forall_mem_range.1

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)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ Memℓp f p

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)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ Memℓp f p

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
f : (a : α) → E a
C : ℝ
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hF : Bornology.IsBounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ Memℓp f ⊤

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)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ Memℓp f p

Proof state:
case h.intro
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
f : (a : α) → E a
C : ℝ
_i : Fact (1 ≤ ⊤)
F : ι → ↥(lp E ⊤)
hF : Bornology.IsBounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF : ∀ (k : ι), ‖F k‖ ≤ C
a : α
⊢ (fun i => ‖f i‖) a ≤ C

Tactic:
exact norm_apply_le_of_tendsto (Eventually.of_forall hCF) hf a

Result:
no goals