-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem tendsto_Lp_iff_tendsto_eLpNorm'' {ι} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → α → E)
    (f_ℒp : ∀ n, MemLp (f n) p μ) (f_lim : α → E) (f_lim_ℒp : MemLp f_lim p μ) :
    fi.Tendsto (fun n => (f_ℒp n).toLp (f n)) (𝓝 (f_lim_ℒp.toLp f_lim)) ↔
      fi.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n => MemLp.toLp (f n) ⋯) fi (𝓝 (MemLp.toLp f_lim f_lim_ℒp)) ↔
    Tendsto (fun n => eLpNorm (f n - f_lim) p μ) fi (𝓝 0)

Tactic:
rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm' (fun n => (f_ℒp n).toLp (f n)) (f_lim_ℒp.toLp f_lim)]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n => eLpNorm (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => eLpNorm (f n - f_lim) p μ) fi (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
⊢ eLpNorm (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ = eLpNorm (f n - f_lim) p μ

Tactic:
apply eLpNorm_congr_ae

Result:
case hfg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
⊢ ↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp) =ᶠ[ae μ] f n - f_lim

Proof state:
case hfg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
⊢ ↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp) =ᶠ[ae μ] f n - f_lim

Tactic:
filter_upwards [((f_ℒp n).sub f_lim_ℒp).coeFn_toLp,
  Lp.coeFn_sub ((f_ℒp n).toLp (f n)) (f_lim_ℒp.toLp f_lim)] with _ hx₁ hx₂

Result:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a✝ : α
hx₁ : ↑↑(MemLp.toLp (f n - f_lim) ⋯) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝
⊢ (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝ = (f n - f_lim) a✝

Proof state:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a✝ : α
hx₁ : ↑↑(MemLp.toLp (f n - f_lim) ⋯) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝
⊢ ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (f n - f_lim) a✝

Tactic:
exact hx₁

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n => eLpNorm (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => eLpNorm (f n - f_lim) p μ) fi (𝓝 0)

Tactic:
refine Filter.tendsto_congr fun n => ?_

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
⊢ eLpNorm (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ = eLpNorm (f n - f_lim) p μ

Proof state:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a✝ : α
hx₁ : ↑↑(MemLp.toLp (f n - f_lim) ⋯) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝
⊢ (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝ = (f n - f_lim) a✝

Tactic:
rw [← hx₂]

Result:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a✝ : α
hx₁ : ↑↑(MemLp.toLp (f n - f_lim) ⋯) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝
⊢ ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (f n - f_lim) a✝