awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
inl :
  ∀ [IsCountablyGenerated.{u_3} (α := ι) ⊥]
    (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 l)),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 (f_lim x))
inr :
  ∀ (hL : L.NeBot), ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))

Tactic:
rcases eq_or_neBot L with (rfl | hL)

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
hf : ∀ (n : ι), AEMeasurable (f n) μ
inhabited_h : Inhabited ι
inst_7 : IsCountablyGenerated.{u_3} (α := ι) ⊥
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 l)
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 (f_lim x))

Tactic:
⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩

Premises used: Inhabited.default, Filter.tendsto_bot, AEMeasurable.mk, Filter.Eventually.of_forall, And.intro, Exists.intro, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
hf : ∀ (n : ι), AEMeasurable (f n) μ
inhabited_h : Inhabited ι
inst_7 : IsCountablyGenerated.{u_3} (α := ι) ⊥
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 l)
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 (f_lim x))

Tactic:
exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
h : ∀ (x : α) (hx : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))

Tactic:
filter_upwards [h_ae_tendsto] with x hx
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
x : α
hx : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
⊢ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))

Tactic:
simpa [f_lim, hx] using hx.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))

Tactic:
have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
    filter_upwards [h_ae_tendsto] with x hx
    simpa [f_lim, hx] using hx.choose_spec
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
⊢ AEMeasurable f_lim μ

Tactic:
have hf_lim : AEMeasurable f_lim μ :=
    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))

Tactic:
⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩

Premises used: AEMeasurable.mk, And.intro, Exists.intro, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
inr : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))

Tactic:
refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
h :
  ∀ (x : α) (hx : Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))) (h_eq : f_lim x = AEMeasurable.mk f_lim hf_lim x),
    Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))

Tactic:
filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
x : α
hx : Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
h_eq : f_lim x = AEMeasurable.mk f_lim hf_lim x
⊢ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))

Tactic:
simpa [h_eq] using hx
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_3
inst : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
inst_2 : L.NeBot
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
simp_rw :
  ∀ (As_mble : ∀ (i : ι), Measurable (β := ℝ≥0∞) ((As i).indicator fun (x : α) ↦ 1)),
    Measurable (β := ℝ≥0∞) (A.indicator fun (x : α) ↦ 1)
⊢ MeasurableSet A

Tactic:
simp_rw [← measurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢

Premises used: measurable_indicator_const_iff, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_3
inst : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
inst_2 : L.NeBot
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), Measurable (β := ℝ≥0∞) ((As i).indicator fun (x : α) ↦ 1)
⊢ Measurable (β := ℝ≥0∞) (A.indicator fun (x : α) ↦ 1)

Tactic:
ENNReal.measurable_of_tendsto' L As_mble
    ((tendsto_indicator_const_iff_forall_eventually L (1 : ℝ≥0∞)).mpr h_lim)

Premises used: Iff.mpr, tendsto_indicator_const_iff_forall_eventually, ENNReal.measurable_of_tendsto', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_3
inst : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
inst_2 : L.NeBot
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), Measurable (β := ℝ≥0∞) ((As i).indicator fun (x : α) ↦ 1)
⊢ Measurable (β := ℝ≥0∞) (A.indicator fun (x : α) ↦ 1)

Tactic:
exact ENNReal.measurable_of_tendsto' L As_mble
    ((tendsto_indicator_const_iff_forall_eventually L (1 : ℝ≥0∞)).mpr h_lim)

Premises used: Iff.mpr, tendsto_indicator_const_iff_forall_eventually, ENNReal.measurable_of_tendsto', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_3
inst : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
inst_2 : L.NeBot
μ : Measure α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
simp_rw :
  ∀ (As_mble : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) ((As i).indicator fun (x : α) ↦ 1) μ),
    AEMeasurable (β := ℝ≥0∞) (A.indicator fun (x : α) ↦ 1) μ
⊢ NullMeasurableSet A μ

Tactic:
simp_rw [← aemeasurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢

Premises used: aemeasurable_indicator_const_iff, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_3
inst : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
inst_2 : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) ((As i).indicator fun (x : α) ↦ 1) μ
apply :
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (As n).indicator (fun (x : α) ↦ 1) x) L (𝓝 (A.indicator (fun (x : α) ↦ 1) x))
⊢ AEMeasurable (β := ℝ≥0∞) (A.indicator fun (x : α) ↦ 1) μ

Tactic:
apply aemeasurable_of_tendsto_metrizable_ae L As_mble

Premises used: aemeasurable_of_tendsto_metrizable_ae
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_3
inst : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
inst_2 : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) ((As i).indicator fun (x : α) ↦ 1) μ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (As n).indicator (fun (x : α) ↦ 1) x) L (𝓝 (A.indicator (fun (x : α) ↦ 1) x))

Tactic:
simpa [tendsto_indicator_const_apply_iff_eventually] using h_lim

Premises used: tendsto_indicator_const_apply_iff_eventually
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iio)

Tactic:
le_antisymm ?_ (generateFrom_le ?_)

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
refine_1 : borel α ≤ MeasurableSpace.generateFrom (range Iio)
refine_2 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (range Iio) t → MeasurableSet t
⊢ borel α = MeasurableSpace.generateFrom (range Iio)

Tactic:
refine le_antisymm ?_ (generateFrom_le ?_)

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
refine_1 :
  LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a})
    (MeasurableSpace.generateFrom (range Iio))
⊢ borel α ≤ MeasurableSpace.generateFrom (range Iio)

Tactic:
rw [borel_eq_generateFrom_of_subbasis (@OrderTopology.topology_eq_generate_intervals α _ _ _)]

Premises used: borel_eq_generateFrom_of_subbasis, OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
⊢ ∀ (a : α), MeasurableSet (Iio a)

Tactic:
have H : ∀ a : α, MeasurableSet (Iio a) := fun a => GenerateMeasurable.basic _ ⟨_, rfl⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
⊢ LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a})
    (MeasurableSpace.generateFrom (range Iio))

Tactic:
generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
refine_1 :
  ∀ (t : Set α), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} t → MeasurableSet t
⊢ LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a})
    (MeasurableSpace.generateFrom (range Iio))

Tactic:
refine generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
refine_1 : ∀ (b : α) (hb : a ⋖ b), MeasurableSet (Ioi a)
refine_1₁ : ∀ (hcovBy : ¬∃ (b : α), a ⋖ b), MeasurableSet (Ioi a)
⊢ MeasurableSet (Ioi a)

Tactic:
rcases em (∃ b, a ⋖ b) with ⟨b, hb⟩ | hcovBy

Premises used: CovBy, Exists, em
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a b : α
hb : a ⋖ b
refine_1 : MeasurableSet (Iio b)ᶜ
⊢ MeasurableSet (Ioi a)

Tactic:
rw [hb.Ioi_eq, ← compl_Iio]

Premises used: Set.compl_Iio, CovBy.Ioi_eq
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a b : α
hb : a ⋖ b
⊢ MeasurableSet (Iio b)ᶜ

Tactic:
(H _).compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a b : α
hb : a ⋖ b
⊢ MeasurableSet (Iio b)ᶜ

Tactic:
exact (H _).compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
refine_1 :
  ∀ (t : Set α) (hat : t ⊆ Ioi a) (htc : t.Countable)
    (htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)), MeasurableSet (Ioi a)
⊢ MeasurableSet (Ioi a)

Tactic:
rcases isOpen_biUnion_countable (Ioi a) Ioi fun _ _ ↦ isOpen_Ioi with ⟨t, hat, htc, htU⟩

Premises used: Set.Ioi, isOpen_Ioi, TopologicalSpace.isOpen_biUnion_countable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)
⊢ Ioi a = ⋃ b ∈ t, Ici b

Tactic:
Subset.antisymm ?_ <| iUnion₂_subset fun b hb ↦ Ici_subset_Ioi.2 (hat hb)

Premises used: Set.Subset.antisymm, Iff.mpr, Set.iUnion₂_subset, Set.Ici_subset_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)
refine : Ioi a ⊆ ⋃ b ∈ t, Ici b
⊢ Ioi a = ⋃ b ∈ t, Ici b

Tactic:
refine Subset.antisymm ?_ <| iUnion₂_subset fun b hb ↦ Ici_subset_Ioi.2 (hat hb)

Premises used: Set.Subset.antisymm, Iff.mpr, Set.iUnion₂_subset, Set.Ici_subset_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)
⊢ Ioi a ⊆ ⋃ b ∈ t, Ici b

Tactic:
Subset.trans ?_ <| iUnion₂_mono fun _ _ ↦ Ioi_subset_Ici_self

Premises used: Set.Subset.trans, Set.Ioi_subset_Ici_self, Set.iUnion₂_mono
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)
refine : Ioi a ⊆ ⋃ i ∈ t, Ioi i
⊢ Ioi a ⊆ ⋃ b ∈ t, Ici b

Tactic:
refine Subset.trans ?_ <| iUnion₂_mono fun _ _ ↦ Ioi_subset_Ici_self

Premises used: Set.Subset.trans, Set.Ioi_subset_Ici_self, Set.iUnion₂_mono
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)
⊢ Ioi a ⊆ ⋃ i ∈ t, Ioi i

Tactic:
simpa [CovBy, htU, subset_def] using hcovBy

Premises used: Set.subset_def, CovBy
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)
⊢ Ioi a = ⋃ b ∈ t, Ici b

Tactic:
have : Ioi a = ⋃ b ∈ t, Ici b := by
          refine Subset.antisymm ?_ <| iUnion₂_subset fun b hb ↦ Ici_subset_Ioi.2 (hat hb)
          refine Subset.trans ?_ <| iUnion₂_mono fun _ _ ↦ Ioi_subset_Ici_self
          simpa [CovBy, htU, subset_def] using hcovBy