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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero, ← hfg]

Premises used: nonpos_iff_eq_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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)

Tactic:
measure_mono fun x => ?_

Premises used: MeasureTheory.measure_mono
-- 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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
refine :
  ∀ x ∈ s ∩ ⋂ (j : ι), notConvergentSeq f g n j,
    Membership.mem (γ := Set α) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} x
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)

Tactic:
refine measure_mono fun x => ?_

Premises used: MeasureTheory.measure_mono
-- 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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
simp :
  (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)) →
    Membership.mem (γ := Set α) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} x
⊢ x ∈ s ∩ ⋂ (j : ι), notConvergentSeq f g n j →
    Membership.mem (γ := Set α) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} x

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

Premises used: Set.mem_inter_iff, Set.mem_iInter, MeasureTheory.Egorov.mem_notConvergentSeq_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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
push :
  (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)) →
    Membership.mem (γ := Set α) {a : α | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ edist (f n a) (g a)} x
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)) →
    Membership.mem (γ := Set α) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} x

Tactic:
push Not

Premises used: Not
-- 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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
⊢ GT.gt (α := ℝ≥0∞) (↑n : ℝ≥0∞)⁻¹ 0

Tactic:
simp
-- 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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
refine : ∀ (N : ι), ∃ n_1 ≥ N, (↑n : ℝ≥0∞)⁻¹ ≤ edist (f n_1 x) (g x)
⊢ Membership.mem (γ := Set α) {a : α | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ edist (f n a) (g a)} x

Tactic:
refine ⟨hmem, (n : ℝ≥0∞)⁻¹, by simp, fun N => ?_⟩
-- 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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
N : ι
obtain :
  ∀ (n_1 : ι) (hn₁ : n_1 ≥ N) (hn₂ : (↑n : ℝ≥0∞)⁻¹ < edist (f n_1 x) (g x)),
    ∃ n_2 ≥ N, (↑n : ℝ≥0∞)⁻¹ ≤ edist (f n_2 x) (g x)
⊢ ∃ n_1 ≥ N, (↑n : ℝ≥0∞)⁻¹ ≤ edist (f n_1 x) (g x)

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := hx N
-- 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 ι
n_1 : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n_1 : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
N n : ι
hn₁ : n ≥ N
hn₂ : (↑n_1 : ℝ≥0∞)⁻¹ < edist (f n x) (g x)
⊢ ∃ n ≥ N, (↑n_1 : ℝ≥0∞)⁻¹ ≤ edist (f n x) (g x)

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

Premises used: LT.lt.le, And.intro, Exists.intro
-- 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 ι
n_1 : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n_1 : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
N n : ι
hn₁ : n ≥ N
hn₂ : (↑n_1 : ℝ≥0∞)⁻¹ < edist (f n x) (g x)
⊢ ∃ n ≥ N, (↑n_1 : ℝ≥0∞)⁻¹ ≤ edist (f n x) (g x)

Tactic:
exact ⟨n, hn₁, hn₂.le⟩
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst_1 : Preorder ι
inst_2 : Countable ι
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
⊢ MeasurableSet (notConvergentSeq f g n j)

Tactic:
MeasurableSet.iUnion fun k ↦ MeasurableSet.iUnion fun _ ↦
      measurableSet_lt measurable_const <| hf k

Premises used: MeasureTheory.Egorov.notConvergentSeq, measurableSet_lt, measurable_const, MeasurableSet.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 : Countable ι
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 : ℕ
inl :
  ∀ (h : IsEmpty ι),
    Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
inr :
  ∀ (h : Nonempty ι),
    Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
rcases isEmpty_or_nonempty ι with h | h

Premises used: isEmpty_or_nonempty
-- 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 : Countable ι
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 : ℕ
h : IsEmpty ι
⊢ Eq.{u_3 + 1} (α := (j : ι) → ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j))
    fun (j : ι) ↦ 0

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- 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 : Countable ι
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 : ℕ
h : IsEmpty ι
⊢ Eq.{u_3 + 1} (α := (j : ι) → ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j))
    fun (j : ι) ↦ 0

Tactic:
have : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0 := by
      simp only [eq_iff_true_of_subsingleton]
-- 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 : Countable ι
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 : ℕ
h : IsEmpty ι
this :
  Eq.{u_3 + 1} (α := (j : ι) → ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j))
    fun (j : ι) ↦ 0
inl : Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ 0) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
rw [this]
-- 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 : Countable ι
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 : ℕ
h : IsEmpty ι
this :
  Eq.{u_3 + 1} (α := (j : ι) → ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j))
    fun (j : ι) ↦ 0
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ 0) atTop (𝓝 0)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- 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 : Countable ι
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 : ℕ
h : IsEmpty ι
this :
  Eq.{u_3 + 1} (α := (j : ι) → ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j))
    fun (j : ι) ↦ 0
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- 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 : Countable ι
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 : ℕ
h : Nonempty ι
inr :
  Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s ∩ notConvergentSeq f g n i)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

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

Premises used: MeasureTheory.Egorov.measure_inter_notConvergentSeq_eq_zero, Set.inter_iInter
-- 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 : Countable ι
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 : ℕ
h : Nonempty ι
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s ∩ notConvergentSeq f g n i)) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_iInter_atTop
    (fun n ↦ (hsm.inter <| notConvergentSeq_measurableSet hf).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)⟩

Premises used: Set.inter_subset_inter_right, MeasurableSet.nullMeasurableSet, Nonempty.some, Set.inter_subset_left, ne_top_of_le_ne_top, MeasureTheory.Egorov.notConvergentSeq_antitone, MeasureTheory.tendsto_measure_iInter_atTop, MeasureTheory.Egorov.notConvergentSeq_measurableSet, MeasureTheory.measure_mono, Exists.intro, MeasurableSet.inter
-- 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 : Countable ι
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 : ℕ
h : Nonempty ι
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s ∩ notConvergentSeq f g n i)) : Filter ℝ≥0∞)

Tactic:
refine tendsto_measure_iInter_atTop
    (fun n ↦ (hsm.inter <| notConvergentSeq_measurableSet hf).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)⟩

Premises used: Set.inter_subset_inter_right, MeasurableSet.nullMeasurableSet, Nonempty.some, Set.inter_subset_left, ne_top_of_le_ne_top, MeasureTheory.Egorov.notConvergentSeq_antitone, MeasureTheory.tendsto_measure_iInter_atTop, MeasureTheory.Egorov.notConvergentSeq_measurableSet, MeasureTheory.measure_mono, Exists.intro, MeasurableSet.inter
-- 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 : ℕ
⊢ ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n) > 0

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))
n : ℕ
have :
  ∀ (N : ι)
    (hN :
      ∀ n_1 ≥ N,
        Membership.mem (α := ℝ≥0∞)
          (Icc (0 - ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)) (0 + ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)))
          ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n n_1) : ℝ≥0∞)),
    ∃ (j : ι), (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)
⊢ ∃ (j : ι), (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)

Tactic:
have ⟨N, hN⟩ := (ENNReal.tendsto_atTop ENNReal.zero_ne_top).1
    (measure_notConvergentSeq_tendsto_zero hf hsm hs hfg n) (.ofReal (ε * 2⁻¹ ^ n))
      (by 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))
n : ℕ
N : ι
hN :
  ∀ n_1 ≥ N,
    Membership.mem (α := ℝ≥0∞)
      (Icc (0 - ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)) (0 + ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n n_1) : ℝ≥0∞)
⊢ ∀ n_1 ≥ N,
    Membership.mem (α := ℝ≥0∞)
      (Icc (0 - ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)) (ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n n_1) : ℝ≥0∞)

Tactic:
rw [zero_add] at hN

Premises used: zero_add
-- 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 : ℕ
N : ι
hN :
  ∀ n_1 ≥ N,
    Membership.mem (α := ℝ≥0∞)
      (Icc (0 - ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)) (ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n n_1) : ℝ≥0∞)
⊢ ∃ (j : ι), (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)

Tactic:
⟨N, (hN N le_rfl).2⟩

Premises used: le_rfl, And.right, Exists.intro
-- 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 : ℕ
N : ι
hN :
  ∀ n_1 ≥ N,
    Membership.mem (α := ℝ≥0∞)
      (Icc (0 - ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)) (ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n n_1) : ℝ≥0∞)
⊢ ∃ (j : ι), (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)

Tactic:
exact ⟨N, (hN N le_rfl).2⟩
-- 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 : ℕ
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n (notConvergentSeqLTIndex (s := s) hε hf hsm hs hfg n)) ≤
    ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)

Tactic:
Classical.choose_spec <| exists_notConvergentSeq_lt hε hf hsm hs hfg n

Premises used: Classical.choose_spec, MeasureTheory.Egorov.exists_notConvergentSeq_lt, 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))
⊢ MeasurableSet (iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg)

Tactic:
MeasurableSet.iUnion fun _ ↦ hsm.inter <| notConvergentSeq_measurableSet hf

Premises used: MeasureTheory.Egorov.iUnionNotConvergentSeq, MeasureTheory.Egorov.notConvergentSeq_measurableSet, MeasurableSet.iUnion, MeasurableSet.inter
-- 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))
⊢ (μ : (a : Set α) → ℝ≥0∞) (iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg) ≤ ENNReal.ofReal ε

Tactic:
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