-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    (hf : ∀ n, AEStronglyMeasurable (f n) μ) (hg : AEStronglyMeasurable g μ) {l : Filter ι}
    (hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)) : TendstoInMeasure μ f l g

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
this :
  (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) = fun n =>
    eLpNorm (f n - g) p μ
⊢ Tendsto (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) l (𝓝 0)

Tactic:
rw [this]

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
this :
  (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) = fun n =>
    eLpNorm (f n - g) p μ
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) = fun n =>
    eLpNorm (f n - g) p μ

Tactic:
ext1 n

Result:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
n : ι
⊢ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ = eLpNorm (f n - g) p μ

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ (fun i => AEStronglyMeasurable.mk (f i) ⋯) l (AEStronglyMeasurable.mk g hg)

Tactic:
refine tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable
  hp_ne_zero hp_ne_top (fun i => (hf i).stronglyMeasurable_mk) hg.stronglyMeasurable_mk ?_

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ Tendsto (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) l (𝓝 0)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ Tendsto (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) l (𝓝 0)

Tactic:
have : (fun n => eLpNorm ((hf n).mk (f n) - hg.mk g) p μ) = fun n => eLpNorm (f n - g) p μ := by
  ext1 n; refine eLpNorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
this :
  (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) = fun n =>
    eLpNorm (f n - g) p μ
⊢ Tendsto (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) l (𝓝 0)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ (fun i => AEStronglyMeasurable.mk (f i) ⋯) l (AEStronglyMeasurable.mk g hg)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
this :
  (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) = fun n =>
    eLpNorm (f n - g) p μ
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)

Tactic:
exact hfg

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
n : ι
⊢ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ = eLpNorm (f n - g) p μ

Tactic:
refine eLpNorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)

Result:
no goals