-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem sum_rpow_le_of_tendsto (hp : p ≠ ∞) {C : ℝ} {F : ι → lp E p} (hCF : ∀ᶠ k in l, ‖F k‖ ≤ C)
    {f : ∀ a, E a} (hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) (s : Finset α) :
    ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal

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)
hp : p ≠ ⊤
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal
a : α
a✝ : a ∈ s
this : Continuous fun f => f a
⊢ Continuous fun f => ‖f a‖ ^ p.toReal

Tactic:
exact this.norm.rpow_const fun _ => Or.inr hp''.le

Result:
no goals

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)
hp : p ≠ ⊤
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous G
k : ι
hCFk : ‖F k‖ ≤ C
⊢ ‖F k‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
gcongr

Result:
no goals

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)
hp : p ≠ ⊤
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous G
⊢ ∀ᶠ (c : ι) in l, (G ∘ id fun i => ↑(F i)) c ≤ C ^ p.toReal

Tactic:
refine hCF.mono ?_

Result:
α : 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)
hp : p ≠ ⊤
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous G
⊢ ∀ (x : ι), ‖F x‖ ≤ C → (G ∘ id fun i => ↑(F i)) x ≤ C ^ p.toReal

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)
hp : p ≠ ⊤
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous G
⊢ ∀ (x : ι), ‖F x‖ ≤ C → (G ∘ id fun i => ↑(F i)) x ≤ C ^ p.toReal

Tactic:
intro k hCFk

Result:
α : 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)
hp : p ≠ ⊤
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous G
k : ι
hCFk : ‖F k‖ ≤ C
⊢ (G ∘ id fun i => ↑(F i)) k ≤ C ^ p.toReal

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)
hp : p ≠ ⊤
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
s : Finset α
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
have hp' : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'

Result:
α : 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)
hp : p ≠ ⊤
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal