α : Type u_2
E : Type u_3
F : Type ?u.8125054
G : Type ?u.8125057
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → { x // x ∈ Lp E p }
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
⊢ Tendsto (fun n => snorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => snorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)
α : Type u_2
E : Type u_3
F : Type ?u.8125054
G : Type ?u.8125057
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → { x // x ∈ Lp E p }
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
⊢ Tendsto f fi (𝓝 (Memℒp.toLp f_lim f_lim_ℒp)) ↔ Tendsto (fun n => snorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)
rw [tendsto_Lp_iff_tendsto_ℒp']
α : Type u_2
E : Type u_3
F : Type ?u.8125054
G : Type ?u.8125057
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → { x // x ∈ Lp E p }
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
h_eq : (fun n => snorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) = fun n => snorm (↑↑(f n) - f_lim) p μ
⊢ Tendsto (fun n => snorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => snorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)

case h_eq
α : Type u_2
E : Type u_3
F : Type ?u.8125054
G : Type ?u.8125057
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → { x // x ∈ Lp E p }
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
⊢ (fun n => snorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) = fun n => snorm (↑↑(f n) - f_lim) p μ
α : Type u_2
E : Type u_3
F : Type ?u.8125054
G : Type ?u.8125057
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → { x // x ∈ Lp E p }
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
⊢ Tendsto (fun n => snorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => snorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)
suffices h_eq :
  (fun n => snorm (⇑(f n) - ⇑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) =
    (fun n => snorm (⇑(f n) - f_lim) p μ)
no goals
case h_eq
α : Type u_2
E : Type u_3
F : Type ?u.8125054
G : Type ?u.8125057
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → { x // x ∈ Lp E p }
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
⊢ (fun n => snorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) = fun n => snorm (↑↑(f n) - f_lim) p μ
exact funext fun n => snorm_congr_ae (EventuallyEq.rfl.sub (Memℒp.coeFn_toLp f_lim_ℒp))
no goals
α : Type u_2
E : Type u_3
F : Type ?u.8125054
G : Type ?u.8125057
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → { x // x ∈ Lp E p }
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
h_eq : (fun n => snorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) = fun n => snorm (↑↑(f n) - f_lim) p μ
⊢ Tendsto (fun n => snorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => snorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)
rw [h_eq]