-- Mathlib/MeasureTheory/Function/Egorov.lean
theorem measure_inter_notConvergentSeq_eq_zero [SemilatticeSup ι] [Nonempty ι]
    (hfg : ∀ᵐ x ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))) (n : ℕ) :
    μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0

Proof state:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)
⊢ x ∈ {a | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ dist (f n a) (g a)}

Tactic:
refine ⟨hmem, 1 / (n + 1 : ℝ), Nat.one_div_pos_of_nat, fun N => ?_⟩

Result:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)
N : ι
⊢ ∃ n_1 ≥ N, 1 / (↑n + 1) ≤ dist (f n_1 x) (g x)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) ≤ μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)}

Tactic:
refine measure_mono fun x => ?_

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
⊢ x ∈ s ∩ ⋂ j, notConvergentSeq f g n j → x ∈ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)}

Proof state:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)
N : ι
⊢ ∃ n_1 ≥ N, 1 / (↑n + 1) ≤ dist (f n_1 x) (g x)

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := hx N

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n✝ : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, 1 / (↑n✝ + 1) < dist (f k x) (g x)
N n : ι
hn₁ : n ≥ N
hn₂ : 1 / (↑n✝ + 1) < dist (f n x) (g x)
⊢ ∃ n ≥ N, 1 / (↑n✝ + 1) ≤ dist (f n x) (g x)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0

Tactic:
simp_rw [Metric.tendsto_atTop, ae_iff] at hfg

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)) →
    x ∈ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)}

Tactic:
push_neg

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)) →
    x ∈ {a | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ dist (f n a) (g a)}

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
⊢ x ∈ s ∩ ⋂ j, notConvergentSeq f g n j → x ∈ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)}

Tactic:
simp only [Set.mem_inter_iff, Set.mem_iInter, mem_notConvergentSeq_iff]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)) →
    x ∈ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)}

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)) →
    x ∈ {a | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ dist (f n a) (g a)}

Tactic:
rintro ⟨hmem, hx⟩

Result:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, 1 / (↑n + 1) < dist (f k x) (g x)
⊢ x ∈ {a | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ dist (f n a) (g a)}

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← hfg]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) ≤ μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)}

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n✝ : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, 1 / (↑n✝ + 1) < dist (f k x) (g x)
N n : ι
hn₁ : n ≥ N
hn₂ : 1 / (↑n✝ + 1) < dist (f n x) (g x)
⊢ ∃ n ≥ N, 1 / (↑n✝ + 1) ≤ dist (f n x) (g x)

Tactic:
exact ⟨n, hn₁, hn₂.le⟩

Result:
no goals