-- Mathlib/MeasureTheory/Function/Egorov.lean
theorem measure_notConvergentSeq_tendsto_zero [SemilatticeSup ι] [Countable ι]
    (hf : ∀ n, StronglyMeasurable (f n)) (hg : StronglyMeasurable g) (hsm : MeasurableSet s)
    (hs : μ s ≠ ∞) (hfg : ∀ᵐ x ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))) (n : ℕ) :
    Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Proof state:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
this : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0
⊢ Tendsto (fun j => 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

Result:
no goals

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

Tactic:
rcases isEmpty_or_nonempty ι with h | h

Result:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
⊢ Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

case inr
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : Nonempty ι
⊢ Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Proof state:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
this : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0
⊢ Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
rw [this]

Result:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
this : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0
⊢ Tendsto (fun j => 0) atTop (𝓝 0)

Proof state:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : Nonempty ι
⊢ Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 (μ (⋂ i, s ∩ notConvergentSeq f g n i)))

Tactic:
refine tendsto_measure_iInter_atTop
  (fun n ↦ (hsm.inter <| notConvergentSeq_measurableSet hf hg).nullMeasurableSet)
  (fun k l hkl => Set.inter_subset_inter_right _ <| notConvergentSeq_antitone hkl)
  ⟨h.some, ne_top_of_le_ne_top hs (measure_mono Set.inter_subset_left)⟩

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
⊢ Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
have : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0 := by
  simp only [eq_iff_true_of_subsingleton]

Result:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
this : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0
⊢ Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
⊢ (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : Nonempty ι
⊢ Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
rw [← measure_inter_notConvergentSeq_eq_zero hfg n, Set.inter_iInter]

Result:
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : Nonempty ι
⊢ Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 (μ (⋂ i, s ∩ notConvergentSeq f g n i)))