awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
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)
inhabit :
  ∀ (inhabited_h : Inhabited ι),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
inl :
  ∀ (inhabited_h : Inhabited ι) [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 inr₁ inr₂ :
  ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
inr₃ :
  ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
    let 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))),
      ∃ (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))
have inr₄ : ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
  let 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 sorry.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: classical
  inhabit ι
  rcases eq_or_neBot L with (rfl | hL)
  · exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
  set f_lim : α → β := fun x ↦
    if h : ∃ l : β, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose
      else (⟨f default x⟩ : Nonempty β).some
  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
  have hf_lim : AEMeasurable f_lim μ :=
    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
  refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
  filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
  simpa [h_eq] using hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
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
⊢ MeasurableSet A
have simp_rw : ∀ (As_mble : ∀ (i : ι), Measurable (β := ℝ≥0∞) ((As i).indicator fun (x : α) ↦ 1)),
  Measurable (β := ℝ≥0∞) (A.indicator fun (x : α) ↦ 1)
Tactic: simp_rw [← measurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢
Cleared hypotheses: As_mble
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
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
⊢ NullMeasurableSet A μ
have simp_rw : ∀ (As_mble : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) ((As i).indicator fun (x : α) ↦ 1) μ),
  AEMeasurable (β := ℝ≥0∞) (A.indicator fun (x : α) ↦ 1) μ
Tactic: simp_rw [← aemeasurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢
Cleared hypotheses: As_mble
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
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) μ
⊢ AEMeasurable (β := ℝ≥0∞) (A.indicator fun (x : α) ↦ 1) μ
have apply : ∀ᵐ (x : α) ∂μ,
  Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (As n).indicator (fun (x : α) ↦ 1) x) L (𝓝 (A.indicator (fun (x : α) ↦ 1) x))
Tactic: apply aemeasurable_of_tendsto_metrizable_ae L As_mble
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iio)
have refine_1 : borel α ≤ MeasurableSpace.generateFrom (range Iio)
Tactic: refine le_antisymm ?_ (generateFrom_le ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
refine_1 : borel α ≤ MeasurableSpace.generateFrom (range Iio)
⊢ borel α = MeasurableSpace.generateFrom (range Iio)
have refine_2 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (range Iio) t → MeasurableSet t
Tactic: refine le_antisymm ?_ (generateFrom_le ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ borel α ≤ MeasurableSpace.generateFrom (range Iio)
have refine_1 : LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a})
  (MeasurableSpace.generateFrom (range Iio))
Tactic: rw [borel_eq_generateFrom_of_subbasis (@OrderTopology.topology_eq_generate_intervals α _ _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
⊢ LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a})
    (MeasurableSpace.generateFrom (range Iio))
have H : ∀ (a : α), MeasurableSet (Iio a)
Tactic: have H : ∀ a : α, MeasurableSet (Iio a) := fun a => GenerateMeasurable.basic _ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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))
have refine_1 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} t → MeasurableSet t
Tactic: refine generateFrom_le ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 : α
⊢ MeasurableSet (Ioi a)
have refine_1 : ∀ (b : α) (hb : a ⋖ b), MeasurableSet (Ioi a)
Tactic: rcases em (∃ b, a ⋖ b) with ⟨b, hb⟩ | hcovBy
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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)
⊢ MeasurableSet (Ioi a)
have refine_1₁ : ∀ (hcovBy : ¬∃ (b : α), a ⋖ b), MeasurableSet (Ioi a)
Tactic: rcases em (∃ b, a ⋖ b) with ⟨b, hb⟩ | hcovBy
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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 (Ioi a)
have refine_1 : MeasurableSet (Iio b)ᶜ
Tactic: rw [hb.Ioi_eq, ← compl_Iio]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
⊢ MeasurableSet (Ioi a)
have 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)
Tactic: rcases isOpen_biUnion_countable (Ioi a) Ioi fun _ _ ↦ isOpen_Ioi with ⟨t, hat, htc, htU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
have refine : Ioi a ⊆ ⋃ b ∈ t, Ici b
Tactic: refine Subset.antisymm ?_ <| iUnion₂_subset fun b hb ↦ Ici_subset_Ioi.2 (hat hb)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
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
have refine : Ioi a ⊆ ⋃ i ∈ t, Ioi i
Tactic: refine Subset.trans ?_ <| iUnion₂_mono fun _ _ ↦ Ioi_subset_Ici_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
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)
⊢ MeasurableSet (Ioi a)
have this₁ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this_1 : 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)
this : Ioi a = ⋃ b ∈ t, Ici b
⊢ MeasurableSet (Ioi a)
have refine_1 : MeasurableSet.{u_1} (α := α) (⋃ b ∈ t, (Iio b)ᶜ)
Tactic: simp only [this, ← compl_Iio]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (range Iio) t → MeasurableSet t
have refine_2 : ∀ (i : α), MeasurableSet (Iio i)
Tactic: rw [forall_mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iic)
have rw : Eq.{u_1 + 1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
  (MeasurableSpace.generateFrom (range Iic))
Tactic: rw [borel_eq_generateFrom_Ioi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))
have refine_1 : LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
  (MeasurableSpace.generateFrom (range Iic))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
refine_1 :
  LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))
have refine_2 : LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Iic))
  (MeasurableSpace.generateFrom (range Ioi))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))
have refine_1 : ∀ (t : Set α) (ht : Membership.mem (γ := Set (Set α)) (range Ioi) t), MeasurableSet t
Tactic: refine MeasurableSpace.generateFrom_le fun t ht => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
t : Set α
ht : Membership.mem (γ := Set (Set α)) (range Ioi) t
⊢ MeasurableSet t
have refine_1 : ∀ (u : α), MeasurableSet (Ioi u)
Tactic: obtain ⟨u, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)
have refine_1 : MeasurableSet (Iic u)ᶜ
Tactic: rw [← compl_Iic]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Iic))
    (MeasurableSpace.generateFrom (range Ioi))
have refine_2 : ∀ (t : Set α) (ht : Membership.mem (γ := Set (Set α)) (range Iic) t), MeasurableSet t
Tactic: refine MeasurableSpace.generateFrom_le fun t ht => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
t : Set α
ht : Membership.mem (γ := Set (Set α)) (range Iic) t
⊢ MeasurableSet t
have refine_2 : ∀ (u : α), MeasurableSet (Iic u)
Tactic: obtain ⟨u, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)
have refine_2 : MeasurableSet (Ioi u)ᶜ
Tactic: rw [← compl_Ioi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : OrderClosedTopology α
⊢ (𝓝[Icc a b] x).IsMeasurablyGenerated
have rw : (𝓝[Ici a] x ⊓ 𝓝[Iic b] x).IsMeasurablyGenerated
Tactic: rw [← Ici_inter_Iic, nhdsWithin_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : R1Space α
s_1 : Set α
hs : s_1 ∈ cocompact α
⊢ ∃ t ∈ cocompact α, MeasurableSet t ∧ t ⊆ s_1
have obtain : ∀ (t : Set α) (ht : IsCompact t) (hts : tᶜ ⊆ s_1), ∃ t ∈ cocompact α, MeasurableSet t ∧ t ⊆ s_1
Tactic: obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
⊢ MeasurableSet s
have huopen : IsOpen[inst] u
Tactic: have huopen : IsOpen u := isOpen_biUnion fun _ _ => isOpen_biUnion fun _ _ => isOpen_Ioo
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
⊢ MeasurableSet s
have humeas : MeasurableSet u
Tactic: have humeas : MeasurableSet u := huopen.measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
humeas : MeasurableSet u
⊢ MeasurableSet s
have hfinite : (s \ u).Finite
Tactic: have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
⊢ MeasurableSet s
have this : u ⊆ s
Tactic: have : u ⊆ s := iUnion₂_subset fun x hx => iUnion₂_subset fun y hy =>
    Ioo_subset_Icc_self.trans (h.out hx hy)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
inst_3 : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst] u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
this : u ⊆ s
⊢ MeasurableSet s
have rw : MeasurableSet (u ∪ s \ u)
Tactic: rw [← union_diff_cancel this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
s t : Set α
⊢ MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Icc l u = S} ≤ borel α
have h : ∀ (t_1 : Set α),
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Icc l u = S} t_1 → MeasurableSet t_1
Tactic: apply generateFrom_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
s t : Set α
⊢ ∀ (t_1 : Set α),
    Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Icc l u = S} t_1 → MeasurableSet t_1
have this : let this := borel α;
BorelSpace α
Tactic: borelize α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
⊢ borel α = MeasurableSpace.generateFrom S
have refine : borel α ≤ MeasurableSpace.generateFrom S
Tactic: refine le_antisymm ?_ (generateFrom_Icc_mem_le_borel _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
⊢ borel α ≤ MeasurableSpace.generateFrom S
have rw : MeasurableSpace.generateFrom (range Iio) ≤ MeasurableSpace.generateFrom S
Tactic: rw [borel_eq_generateFrom_Iio]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
⊢ MeasurableSpace.generateFrom (range Iio) ≤ MeasurableSpace.generateFrom S
have refine : ∀ (a : α), MeasurableSet (Iio a)
Tactic: refine generateFrom_le (forall_mem_range.2 fun a => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
⊢ MeasurableSet (Iio a)
have rcases : ∀ (t : Set α) (hts : t ⊆ s) (hc : t.Countable) (htd : Dense t) (htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t),
  MeasurableSet (Iio a)
Tactic: rcases hd.exists_countable_dense_subset_bot_top with ⟨t, hts, hc, htd, htb, -⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
⊢ MeasurableSet (Iio a)
have pos : ∀ (ha : ∀ b < a, (Ioo b a).Nonempty), MeasurableSet (Iio a)
Tactic: by_cases! ha : ∀ b < a, (Ioo b a).Nonempty