awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
refine : ∑' (a : ℕ), ENNReal.ofReal (ε / 2 * HPow.hPow (α := ℝ) 2⁻¹ a) ≤ ENNReal.ofReal ε
⊢ (μ : (a : Set α) → ℝ≥0∞) (iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg) ≤ ENNReal.ofReal ε

Tactic:
refine le_trans (measure_iUnion_le _) (le_trans
    (ENNReal.tsum_le_tsum <| notConvergentSeqLTIndex_spec (half_pos hε) hf hsm hs hfg) ?_)

Premises used: ENNReal.tsum_le_tsum, half_pos, MeasureTheory.Egorov.notConvergentSeqLTIndex_spec, MeasureTheory.measure_iUnion_le, le_trans
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
simp_rw : ∑' (a : ℕ), ENNReal.ofReal (ε / 2) * ENNReal.ofReal (HPow.hPow (α := ℝ) 2⁻¹ a) ≤ ENNReal.ofReal ε
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2 * HPow.hPow (α := ℝ) 2⁻¹ a) ≤ ENNReal.ofReal ε

Tactic:
simp_rw [ENNReal.ofReal_mul (half_pos hε).le]

Premises used: half_pos, ENNReal.ofReal_mul, LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
hf_nonneg : ∀ (n : ℕ), 0 ≤ HPow.hPow (α := ℝ) 2⁻¹ n
hf₁ : Summable (HPow.hPow (α := ℝ) 2⁻¹)
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2) * ENNReal.ofReal (HPow.hPow (α := ℝ) 2⁻¹ a) ≤ ENNReal.ofReal ε

Tactic:
rw [ENNReal.tsum_mul_left, ← ENNReal.ofReal_tsum_of_nonneg, inv_eq_one_div, tsum_geometric_two,
    ← ENNReal.ofReal_mul (half_pos hε).le, div_mul_cancel₀ ε two_ne_zero]

Premises used: div_mul_cancel₀, ENNReal.tsum_mul_left, half_pos, ENNReal.ofReal_mul, ENNReal.ofReal_tsum_of_nonneg, LT.lt.le, tsum_geometric_two, inv_eq_one_div, two_ne_zero
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ 0 ≤ HPow.hPow (α := ℝ) 2⁻¹ n

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
hf₁ : Summable (HPow.hPow (1 / 2))
⊢ Summable (HPow.hPow (α := ℝ) 2⁻¹)

Tactic:
rw [inv_eq_one_div]

Premises used: inv_eq_one_div
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow (1 / 2))

Tactic:
summable_geometric_two

Premises used: summable_geometric_two
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow (1 / 2))

Tactic:
exact summable_geometric_two

Premises used: summable_geometric_two
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
rw : s ∩ ⋃ (i : ℕ), notConvergentSeq f g i (notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg i) ⊆ s
⊢ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg ⊆ s

Tactic:
rw [iUnionNotConvergentSeq, ← Set.inter_iUnion]

Premises used: MeasureTheory.Egorov.iUnionNotConvergentSeq, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ s ∩ ⋃ (i : ℕ), notConvergentSeq f g i (notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg i) ⊆ s

Tactic:
Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ s ∩ ⋃ (i : ℕ), notConvergentSeq f g i (notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg i) ⊆ s

Tactic:
exact Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
rw :
  ∀ ε_1 > 0, ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f n x) < ε_1
⊢ TendstoUniformlyOn f g atTop (s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg)

Tactic:
rw [EMetric.tendstoUniformlyOn_iff]

Premises used: EMetric.tendstoUniformlyOn_iff
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
obtain :
  ∀ (N : ℕ) (hN : (↑N : ℝ≥0∞)⁻¹ < δ),
    ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f n x) < δ
⊢ ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f n x) < δ

Tactic:
obtain ⟨N, hN⟩ := ENNReal.exists_inv_nat_lt hδ.ne'

Premises used: LT.lt.ne', ENNReal.exists_inv_nat_lt
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
rw : ∃ (a : ι), ∀ b ≥ a, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f b x) < δ
⊢ ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f n x) < δ

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
⊢ ∃ (a : ι), ∀ b ≥ a, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f b x) < δ

Tactic:
⟨Egorov.notConvergentSeqLTIndex (half_pos hε) hf hsm hs hfg N, fun n hn x hx => ?_⟩

Premises used: half_pos, Exists.intro, MeasureTheory.Egorov.notConvergentSeqLTIndex
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
refine :
  ∀ (n : ι) (hn : n ≥ notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg N) (x : α)
    (hx : x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg), edist (g x) (f n x) < δ
⊢ ∃ (a : ι), ∀ b ≥ a, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f b x) < δ

Tactic:
refine ⟨Egorov.notConvergentSeqLTIndex (half_pos hε) hf hsm hs hfg N, fun n hn x hx => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg N
x : α
hx : x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg
⊢ edist (g x) (f n x) < δ

Tactic:
lt_of_le_of_lt ?_ hN

Premises used: lt_of_le_of_lt
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg N
x : α
hx : x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg
refine : edist (g x) (f n x) ≤ (↑N : ℝ≥0∞)⁻¹
⊢ edist (g x) (f n x) < δ

Tactic:
refine lt_of_le_of_lt ?_ hN

Premises used: lt_of_le_of_lt
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg N
x : α
hx : x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg
⊢ edist (f n x) (g x) ≤ (↑N : ℝ≥0∞)⁻¹

Tactic:
have : edist (f n x) (g x) ≤ (N : ℝ≥0∞)⁻¹ :=
    not_lt.mp fun h ↦ hx.2 <| Set.mem_iUnion.2 ⟨N, hx.1, mem_notConvergentSeq_iff.2 ⟨n, hn, h⟩⟩
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg N
x : α
hx : x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg
this : edist (f n x) (g x) ≤ (↑N : ℝ≥0∞)⁻¹
⊢ edist (g x) (f n x) ≤ (↑N : ℝ≥0∞)⁻¹

Tactic:
simpa [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
s : Set α
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∃ t ⊆ s, MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (s \ t)

Tactic:
⟨Egorov.iUnionNotConvergentSeq hε hf hsm hs hfg,
    Egorov.iUnionNotConvergentSeq_subset hε hf hsm hs hfg,
    Egorov.iUnionNotConvergentSeq_measurableSet hε hf hsm hs hfg,
    Egorov.measure_iUnionNotConvergentSeq hε hf hsm hs hfg,
    Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq hε hf hsm hs hfg⟩

Premises used: MeasureTheory.Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq, MeasureTheory.Egorov.iUnionNotConvergentSeq, MeasureTheory.Egorov.iUnionNotConvergentSeq_subset, And.intro, Exists.intro, MeasureTheory.Egorov.iUnionNotConvergentSeq_measurableSet, MeasureTheory.Egorov.measure_iUnionNotConvergentSeq
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
s : Set α
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∃ t ⊆ s, MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (s \ t)

Tactic:
tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist
    (fun n ↦ ((hf n).edist hg).measurable) hsm hs hfg hε

Premises used: MeasureTheory.StronglyMeasurable.edist, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
a : α
htendsto : Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (g a))
h : Membership.mem (γ := Set α) univ a → Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (g a))
⊢ Membership.mem (γ := Set α) univ a → Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (g a))

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
a : α
htendsto : Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (g a))
h : Membership.mem (γ := Set α) univ a
⊢ Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (g a))

Tactic:
htendsto
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦ Membership.mem (γ := Set α) univ x → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))) x}
            x}
      a
h₁ h₂ :
  ∀ (a : α) (htendsto : Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (g a))),
    Membership.mem (γ := Set α) univ a → Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (g a))
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) univ x → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))

Tactic:
filter_upwards [hfg] with _ htendsto _ using htendsto
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
have :
  ∀ t ⊆ univ,
    ∀ (ht : MeasurableSet t)
      (htendsto : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)),
      ∃ (t : Set α), MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
⊢ ∃ (t : Set α), MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
have ⟨t, _, ht, htendsto⟩ :=
    tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist hf MeasurableSet.univ
    (measure_ne_top μ Set.univ) (by filter_upwards [hfg] with _ htendsto _ using htendsto) hε
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
left : t ⊆ univ
ht : MeasurableSet t
htendsto : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
⊢ ∃ (t : Set α), MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
⟨_, ht, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
left : t ⊆ univ
ht : MeasurableSet t
htendsto : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
refine : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
⊢ ∃ (t : Set α), MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
refine ⟨_, ht, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
left : t ⊆ univ
ht : MeasurableSet t
htendsto rwa rwa₁ rwa₂ rwa₃ : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
⊢ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
rwa [Set.compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∃ (t : Set α), MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist' (fun n ↦ ((hf n).edist hg).measurable)
    hfg hε

Premises used: MeasureTheory.StronglyMeasurable.edist, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist'
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f g : α → β
hfg : f =ᶠ[ae μ] g
⊢ essSup f μ = essSup g μ

Tactic:
limsup_congr hfg

Premises used: Filter.limsup_congr, essSup