-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem tendstoInMeasure_iff_tendsto_toNNReal [Dist E] [IsFiniteMeasure μ]
    {f : ι → α → E} {l : Filter ι} {g : α → E} :
    TendstoInMeasure μ f l g ↔
      ∀ ε, 0 < ε → Tendsto (fun i => (μ { x | ε ≤ dist (f i x) (g x) }).toNNReal) l (𝓝 0)

Proof state:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (ENNReal.toNNReal ∘ fun x => μ {x_1 | ε ≤ dist (f x x_1) (g x_1)}) l (𝓝 (ENNReal.toNNReal 0))

Tactic:
exact h ε hε

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)

Tactic:
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩

Result:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)

case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Proof state:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
hf : (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) = ENNReal.toNNReal ∘ fun i => μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)

Tactic:
rw [hf, ENNReal.tendsto_toNNReal_iff' (hfin ε)]

Result:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
hf : (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) = ENNReal.toNNReal ∘ fun i => μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun x => μ {x_1 | ε ≤ dist (f x x_1) (g x_1)}) l (𝓝 ↑0)

Proof state:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)

Tactic:
have hf : (fun i => (μ { x | ε ≤ dist (f i x) (g x) }).toNNReal) =
    ENNReal.toNNReal ∘ (fun i => (μ { x | ε ≤ dist (f i x) (g x) })) := rfl

Result:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
hf : (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) = ENNReal.toNNReal ∘ fun i => μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)

Proof state:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
hf : (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) = ENNReal.toNNReal ∘ fun i => μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun x => μ {x_1 | ε ≤ dist (f x x_1) (g x_1)}) l (𝓝 ↑0)

Tactic:
exact h ε hε

Result:
no goals

Proof state:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
rw [← ENNReal.tendsto_toNNReal_iff ENNReal.zero_ne_top (hfin ε)]

Result:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
h : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (ENNReal.toNNReal ∘ fun x => μ {x_1 | ε ≤ dist (f x x_1) (g x_1)}) l (𝓝 (ENNReal.toNNReal 0))

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)

Tactic:
have hfin ε i : μ { x | ε ≤ dist (f i x) (g x) } ≠ ⊤ :=
  measure_ne_top μ {x | ε ≤ dist (f i x) (g x)}

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Dist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ) (i : ι), μ {x | ε ≤ dist (f i x) (g x)} ≠ ⊤
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => (μ {x | ε ≤ dist (f i x) (g x)}).toNNReal) l (𝓝 0)