awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
⊢ (s \ interior s).Countable
have A : ∀ x ∈ s, ∃ y ∈ Ioi x, Ioo x y ⊆ s
Tactic: have A : ∀ x ∈ s, ∃ y ∈ Ioi x, Ioo x y ⊆ s := fun x hx =>
    (mem_nhdsGT_iff_exists_Ioo_subset' (hM x hx)).1 (h x hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
A : ∀ x ∈ s, ∃ y ∈ Ioi x, Ioo x y ⊆ s
⊢ (s \ interior s).Countable
have choose! : ∀ (y : (x : α) → α) (hy : ∀ x ∈ s, y x ∈ Ioi x) (h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s), (s \ interior s).Countable
Tactic: choose! y hy h'y using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'
have inl : ∀ (h' : x < x'), Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'
Tactic: rcases lt_or_gt_of_ne hxx' with (h' | h')
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
inl : ∀ (h' : x < x'), Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'
have inr : ∀ (h' : x' < x), Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'
Tactic: rcases lt_or_gt_of_ne hxx' with (h' | h')
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'
have inl : ∀ (z : α) (hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z)
  (h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z), False
Tactic: refine disjoint_left.2 fun z hz h'z => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
z : α
hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z
h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z
⊢ False
have this : x' ∈ interior s
Tactic: have : x' ∈ interior s :=
        mem_interior.2 ⟨Ioo x (y x), h'y _ hx.1, isOpen_Ioo, ⟨h', h'z.1.trans hz.2⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'
have inr : ∀ (z : α) (hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z)
  (h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z), False
Tactic: refine disjoint_left.2 fun z hz h'z => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
z : α
hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z
h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z
⊢ False
have this : x ∈ interior s
Tactic: have : x ∈ interior s :=
        mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
⊢ (s \ interior s).Countable
have B : (s \ interior s).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y x)
Tactic: have B : Set.PairwiseDisjoint (s \ interior s) fun x => Ioo x (y x) := by
    intro x hx x' hx' hxx'
    rcases lt_or_gt_of_ne hxx' with (h' | h')
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x' ∈ interior s :=
        mem_interior.2 ⟨Ioo x (y x), h'y _ hx.1, isOpen_Ioo, ⟨h', h'z.1.trans hz.2⟩⟩
      exact False.elim (hx'.2 this)
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x ∈ interior s :=
        mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
      exact False.elim (hx.2 this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
⊢ MeasurableSet s
have pos : ∀ (H : ∃ x ∈ s, IsTop x), MeasurableSet s
Tactic: by_cases H : ∃ x ∈ s, IsTop x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
pos : ∀ (H : ∃ x ∈ s, IsTop x), MeasurableSet s
⊢ MeasurableSet s
have neg : ∀ (H : ¬∃ x ∈ s, IsTop x), MeasurableSet s
Tactic: by_cases H : ∃ x ∈ s, IsTop x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ∃ x ∈ s, IsTop x
⊢ MeasurableSet s
have pos : ∀ (x₀ : α) (x₀s : x₀ ∈ s) (h₀ : IsTop x₀), MeasurableSet s
Tactic: rcases H with ⟨x₀, x₀s, h₀⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
⊢ s = {x₀} ∪ s \ {x₀}
have rw : s = s
Tactic: rw [union_diff_cancel (singleton_subset_iff.2 x₀s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
⊢ MeasurableSet s
have this : s = {x₀} ∪ s \ {x₀}
Tactic: have : s = { x₀ } ∪ s \ { x₀ } := by rw [union_diff_cancel (singleton_subset_iff.2 x₀s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet s
have pos : MeasurableSet ({x₀} ∪ s \ {x₀})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet ({x₀} ∪ s \ {x₀})
have pos : MeasurableSet (s \ {x₀})
Tactic: refine (measurableSet_singleton _).union ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet (s \ {x₀})
have A : ∀ x ∈ s \ {x₀}, x < x₀
Tactic: have A : ∀ x ∈ s \ { x₀ }, x < x₀ := fun x hx => lt_of_le_of_ne (h₀ _) (by simpa using hx.2)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
⊢ MeasurableSet (s \ {x₀})
have pos : ∀ (x : α) (hx : x ∈ s \ {x₀}), s \ {x₀} ∈ 𝓝[>] x
Tactic: refine .of_mem_nhdsGT_aux (fun x hx => ?_) fun x hx => ⟨x₀, A x hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
⊢ s \ {x₀} ∈ 𝓝[>] x
have pos : ∀ (u : α) (hu : u ∈ Ioi x) (us : Ioo x u ⊆ s), s \ {x₀} ∈ 𝓝[>] x
Tactic: obtain ⟨u, hu, us⟩ : ∃ (u : α), u ∈ Ioi x ∧ Ioo x u ⊆ s :=
      (mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).1 (h x hx.1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
⊢ s \ {x₀} ∈ 𝓝[>] x
have pos : ∀ (y : α) (hy : y ∈ Ioo x u), y ∉ {x₀}
Tactic: refine (mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).2 ⟨u, hu, fun y hy => ⟨us hy, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ¬∃ x ∈ s, IsTop x
⊢ MeasurableSet s
have neg : ∀ x ∈ s, ∃ (y : α), x < y
Tactic: refine .of_mem_nhdsGT_aux h ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
have inl : ∀ (hα : IsEmpty α), MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
inl : ∀ (hα : IsEmpty α), MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
have inr : ∀ (hα : Nonempty α), MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : IsEmpty α
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
have this : ∀ (b : δ), Eq.{u_1 + 1} (α := Set α) (range fun (i : ι) ↦ f i b) ∅
Tactic: have : ∀ b, range (fun i ↦ f i b) = ∅ := fun b ↦ eq_empty_of_isEmpty _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
have A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
Tactic: have A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c} := by
    intro i c
    exact measurableSet_le (hf i) measurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
c : α
⊢ MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
have rw : MeasurableSet.{u_4} (α := δ) (⋂ (i : ι), {x : δ | f i x ≤ c})
Tactic: rw [setOf_forall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
have B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
Tactic: have B : ∀ (c : α), MeasurableSet {x | ∀ i, f i x ≤ c} := by
    intro c
    rw [setOf_forall]
    exact MeasurableSet.iInter (fun i ↦ A i c)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
have inr : ∀ (u : ℕ → α) (hu : Tendsto u atTop atTop),
  MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
Tactic: obtain ⟨u, hu⟩ : ∃ (u : ℕ → α), Tendsto u atTop atTop := exists_seq_tendsto (atTop : Filter α)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
⊢ Eq.{u_4 + 1} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
have h₁ : Subset.{u_4} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
  {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
h₁ :
  Subset.{u_4} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
⊢ Eq.{u_4 + 1} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
have h₂ : Subset.{u_4} (α := Set δ) {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
  {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
c : α
hc : Membership.mem (γ := Set α) (upperBounds (range fun (i : ι) ↦ f i x)) c
⊢ Membership.mem (γ := Set δ) {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n} x
have h₁ : ∀ (n : ℕ) (hn : c ≤ u n), Membership.mem (γ := Set δ) {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n} x
Tactic: obtain ⟨n, hn⟩ : ∃ n, c ≤ u n := (tendsto_atTop.1 hu c).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
n : ℕ
hn : ∀ (i : ι), f i x ≤ u n
⊢ Membership.mem (γ := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)} x
have h₂ : Membership.mem (γ := Set α) (upperBounds (range fun (i : ι) ↦ f i x)) (u n)
Tactic: refine ⟨u n, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
have this : Eq.{u_4 + 1} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
  {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
Tactic: have : {b | BddAbove (range (fun i ↦ f i b))} = {x | ∃ n, ∀ i, f i x ≤ u n} := by
    apply Subset.antisymm
    · rintro x ⟨c, hc⟩
      obtain ⟨n, hn⟩ : ∃ n, c ≤ u n := (tendsto_atTop.1 hu c).exists
      exact ⟨n, fun i ↦ (hc ((mem_range_self i))).trans hn⟩
    · rintro x ⟨n, hn⟩
      refine ⟨u n, ?_⟩
      rintro - ⟨i, rfl⟩
      exact hn i
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}
B : ∀ (c : α), MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
this :
  Eq.{u_4 + 1} (α := Set δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
    {x : δ | ∃ (n : ℕ), ∀ (i : ι), f i x ≤ u n}
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
have inr : MeasurableSet.{u_4} (α := δ) (⋃ (i : ℕ), {x : δ | ∀ (i_1 : ι), f i_1 x ≤ u i})
Tactic: rw [this, setOf_exists]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ ⨆ (_ : p), f b
have simp_rw : Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sSup ∅
Tactic: simp_rw [ciSup_eq_ite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ if h : p then f b else sSup ∅
have pos : ∀ (h : p), Measurable.{u_4, u_5} (β := α) fun (b : δ) ↦ f b
Tactic: split_ifs with h