awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
h : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x)
g_seq : (i : δ) → α := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some
b : δ
⊢ IsLUB {a : α | ∃ (i : ι), (if b ∈ aeSeqSet hf p then mk (f i) ⋯ b else Nonempty.some ⋯) = a}
    (if b ∈ aeSeqSet hf p then g b else hα.some)
have pos : ∀ (h : b ∈ aeSeqSet hf p), IsLUB {a : α | ∃ (i : ι), mk (f i) sorry b = a} (g b)
Tactic: split_ifs with 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
h : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x)
g_seq : (i : δ) → α := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some
b : δ
pos : ∀ (h : b ∈ aeSeqSet hf p), IsLUB {a : α | ∃ (i : ι), mk (f i) ⋯ b = a} (g b)
⊢ IsLUB {a : α | ∃ (i : ι), (if b ∈ aeSeqSet hf p then mk (f i) ⋯ b else Nonempty.some ⋯) = a}
    (if b ∈ aeSeqSet hf p then g b else hα.some)
have neg : ∀ (h : b ∉ aeSeqSet hf p), IsLUB {a : α | ∃ (i : ι), Nonempty.some sorry = a} hα.some
Tactic: split_ifs with 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
h_1 : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x)
g_seq : (i : δ) → α := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some
b : δ
h : b ∈ aeSeqSet hf p
⊢ Eq.{u_1 + 1} (α := Set α) {a : α | ∃ (i : ι), mk (f i) ⋯ b = a} {a : α | ∃ (i : ι), f i b = a}
have h₁ : ∀ (x : α),
  Membership.mem (γ := Set α) {a : α | ∃ (i : ι), mk (f i) sorry b = a} x ↔
    Membership.mem (γ := Set α) {a : α | ∃ (i : ι), f i b = a} x
Tactic: ext x
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
h_1 : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x)
g_seq : (i : δ) → α := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some
b : δ
h : b ∈ aeSeqSet hf p
⊢ IsLUB {a : α | ∃ (i : ι), mk (f i) ⋯ b = a} (g b)
have h_set_eq : Eq.{u_1 + 1} (α := Set α) {a : α | ∃ (i : ι), mk (f i) sorry b = a} {a : α | ∃ (i : ι), f i b = a}
Tactic: have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
h_1 : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x)
g_seq : (i : δ) → α := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some
b : δ
h : b ∈ aeSeqSet hf p
h_set_eq : Eq.{u_1 + 1} (α := Set α) {a : α | ∃ (i : ι), mk (f i) ⋯ b = a} {a : α | ∃ (i : ι), f i b = a}
⊢ IsLUB {a : α | ∃ (i : ι), mk (f i) ⋯ b = a} (g b)
have pos : IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
Tactic: rw [h_set_eq]
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
h : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x)
g_seq : (i : δ) → α := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some
⊢ AEMeasurable g μ
have hg_seq : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), aeSeq hf p i b = a} (g_seq b)
Tactic: have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
h : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x)
g_seq : (i : δ) → α := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some
hg_seq : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), aeSeq hf p i b = a} (g_seq b)
⊢ AEMeasurable g μ
have inr : g =ᶠ[ae μ] g_seq
Tactic: refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
⊢ AEMeasurable g μ
have nontriviality : Subsingleton α → AEMeasurable g μ
Tactic: classical
  nontriviality α
  haveI hα : Nonempty α := inferInstance
  rcases isEmpty_or_nonempty ι with hι | hι
  · simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
  let p : δ → (ι → α) → Prop := fun x f' => IsLUB { a | ∃ i, f' i = a } (g x)
  let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
  have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
  refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
  exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
nontriviality : Subsingleton α → AEMeasurable g μ
⊢ AEMeasurable g μ
have nontriviality₁ : Nontrivial α → AEMeasurable g μ
Tactic: classical
  nontriviality α
  haveI hα : Nonempty α := inferInstance
  rcases isEmpty_or_nonempty ι with hι | hι
  · simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
  let p : δ → (ι → α) → Prop := fun x f' => IsLUB { a | ∃ i, f' i = a } (g x)
  let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
  have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
  refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
  exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
nontriviality : Subsingleton α → AEMeasurable g μ
nontriviality₁ : Nontrivial α → AEMeasurable g μ
⊢ AEMeasurable g μ
have nontriviality₂ : Nontrivial α → ∀ (hα : Nonempty α), AEMeasurable g μ
Tactic: classical
  nontriviality α
  haveI hα : Nonempty α := inferInstance
  rcases isEmpty_or_nonempty ι with hι | hι
  · simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
  let p : δ → (ι → α) → Prop := fun x f' => IsLUB { a | ∃ i, f' i = a } (g x)
  let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
  have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
  refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
  exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
nontriviality : Subsingleton α → AEMeasurable g μ
nontriviality₁ : Nontrivial α → AEMeasurable g μ
nontriviality₂ : Nontrivial α → ∀ (hα : Nonempty α), AEMeasurable g μ
⊢ AEMeasurable g μ
have inl : Nontrivial α → ∀ (hα : Nonempty α) (hι : IsEmpty ι), AEMeasurable g μ
Tactic: classical
  nontriviality α
  haveI hα : Nonempty α := inferInstance
  rcases isEmpty_or_nonempty ι with hι | hι
  · simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
  let p : δ → (ι → α) → Prop := fun x f' => IsLUB { a | ∃ i, f' i = a } (g x)
  let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
  have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
  refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
  exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
nontriviality : Subsingleton α → AEMeasurable g μ
nontriviality₁ : Nontrivial α → AEMeasurable g μ
nontriviality₂ : Nontrivial α → ∀ (hα : Nonempty α), AEMeasurable g μ
inl : Nontrivial α → ∀ (hα : Nonempty α) (hι : IsEmpty ι), AEMeasurable g μ
⊢ AEMeasurable g μ
have inr : Nontrivial α → ∀ (hα : Nonempty α) (hι : Nonempty ι), AEMeasurable g μ
Tactic: classical
  nontriviality α
  haveI hα : Nonempty α := inferInstance
  rcases isEmpty_or_nonempty ι with hι | hι
  · simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
  let p : δ → (ι → α) → Prop := fun x f' => IsLUB { a | ∃ i, f' i = a } (g x)
  let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
  have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
  refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
  exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
nontriviality : Subsingleton α → AEMeasurable g μ
nontriviality₁ : Nontrivial α → AEMeasurable g μ
nontriviality₂ : Nontrivial α → ∀ (hα : Nonempty α), AEMeasurable g μ
inl : Nontrivial α → ∀ (hα : Nonempty α) (hι : IsEmpty ι), AEMeasurable g μ
inr inr₁ inr₂ inr₃ : Nontrivial α → ∀ (hα : Nonempty α) (hι : Nonempty ι), AEMeasurable g μ
⊢ AEMeasurable g μ
have inr₄ : Nontrivial α →
  ∀ (hα : Nonempty α) (hι : Nonempty ι),
    let p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x);
    let g_seq := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some;
    ∀ (hg_seq : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), aeSeq hf p i b = a} (g_seq b)), AEMeasurable g μ
Tactic: classical
  nontriviality α
  haveI hα : Nonempty α := inferInstance
  rcases isEmpty_or_nonempty ι with hι | hι
  · simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
  let p : δ → (ι → α) → Prop := fun x f' => IsLUB { a | ∃ i, f' i = a } (g x)
  let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
  have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
  refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
  exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm
-- 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
nontriviality : Subsingleton α → AEMeasurable g μ
nontriviality₁ : Nontrivial α → AEMeasurable g μ
nontriviality₂ : Nontrivial α → ∀ (hα : Nonempty α), AEMeasurable g μ
inl : Nontrivial α → ∀ (hα : Nonempty α) (hι : IsEmpty ι), AEMeasurable g μ
inr inr₁ inr₂ inr₃ : Nontrivial α → ∀ (hα : Nonempty α) (hι : Nonempty ι), AEMeasurable g μ
inr₄ :
  Nontrivial α →
    ∀ (hα : Nonempty α) (hι : Nonempty ι),
      let p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x);
      let g_seq := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some;
      ∀ (hg_seq : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), aeSeq hf p i b = a} (g_seq b)), AEMeasurable g μ
⊢ AEMeasurable g μ
have inr₅ : Nontrivial α →
  ∀ (hα : Nonempty α) (hι : Nonempty ι),
    let p : δ → (ι → α) → Prop := fun (x : δ) (f' : ι → α) ↦ IsLUB {a : α | ∃ (i : ι), f' i = a} (g x);
    let g_seq := (aeSeqSet hf p).piecewise (β := fun (i : δ) ↦ α) g fun (x : δ) ↦ hα.some;
    ∀ (hg_seq : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), aeSeq hf p i b = a} (g_seq b)), g =ᶠ[ae μ] g_seq
Tactic: classical
  nontriviality α
  haveI hα : Nonempty α := inferInstance
  rcases isEmpty_or_nonempty ι with hι | hι
  · simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))
  let p : δ → (ι → α) → Prop := fun x f' => IsLUB { a | ∃ i, f' i = a } (g x)
  let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
  have hg_seq : ∀ b, IsLUB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) := by
    intro b
    simp only [g_seq, aeSeq, Set.piecewise]
    split_ifs with h
    · have h_set_eq : { a : α | ∃ i : ι, (hf i).mk (f i) b = a } =
        { a : α | ∃ i : ι, f i b = a } := by
        ext x
        simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
      rw [h_set_eq]
      exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
    · exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
  refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
  exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm
-- 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, ∃ (y : α), x < y
⊢ MeasurableSet s
have choose! : ∀ (M : (x : α) → α) (hM : ∀ x ∈ s, x < M x), MeasurableSet s
Tactic: choose! M hM using 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
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
H : (s \ interior s).Countable
⊢ s = interior s ∪ s \ interior s
have rw : s = s
Tactic: rw [union_diff_cancel interior_subset]
-- 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
H : (s \ interior s).Countable
⊢ MeasurableSet s
have this : s = interior s ∪ s \ interior s
Tactic: have : s = interior s ∪ s \ interior s := by rw [union_diff_cancel interior_subset]
-- 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
H : (s \ interior s).Countable
this : s = interior s ∪ s \ interior s
⊢ MeasurableSet s
have rw : MeasurableSet (interior s ∪ s \ interior s)
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
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
⊢ MeasurableSet s
have suffices : (s \ interior s).Countable
Tactic: suffices H : (s \ interior s).Countable by
    have : s = interior s ∪ s \ interior s := by rw [union_diff_cancel interior_subset]
    rw [this]
    exact isOpen_interior.measurableSet.union H.measurableSet