awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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)
neg : ∀ (h : b ∉ aeSeqSet hf p), IsLUB {a : α | ∃ (i : ι), Nonempty.some ⋯ = a} hα.some
⊢ 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)

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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₁ :
  ∀ (x : α),
    Membership.mem (γ := Set α) {a : α | ∃ (i : ι), mk (f i) ⋯ b = a} x ↔
      Membership.mem (γ := Set α) {a : α | ∃ (i : ι), f i b = a} x
⊢ Eq.{u_1 + 1} (α := Set α) {a : α | ∃ (i : ι), mk (f i) ⋯ b = a} {a : α | ∃ (i : ι), f i b = a}

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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}

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]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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}
pos : IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
⊢ IsLUB {a : α | ∃ (i : ι), mk (f i) ⋯ b = a} (g b)

Tactic:
rw [h_set_eq]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : ι), f i b = a} (g b)

Tactic:
aeSeq.fun_prop_of_mem_aeSeqSet hf h

Premises used: setOf, aeSeq.fun_prop_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : ι), f i b = a} (g b)

Tactic:
exact aeSeq.fun_prop_of_mem_aeSeqSet hf h

Premises used: aeSeq.fun_prop_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : ι), Nonempty.some ⋯ = a} hα.some

Tactic:
IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩

Premises used: Iff.mpr, Eq.ge, Nonempty.some, LE.le, IsGreatest.isLUB, And.intro, exists_const, _private.0.AEMeasurable.isLUB.match_2, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : ι), Nonempty.some ⋯ = a} hα.some

Tactic:
exact IsGreatest.isLUB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.ge⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : ι), 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⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 μ

Tactic:
⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩

Premises used: AEMeasurable, aeSeq.measurable, Measurable.isLUB, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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)
inr : g =ᶠ[ae μ] g_seq
⊢ AEMeasurable g μ

Tactic:
refine ⟨g_seq, Measurable.isLUB (aeSeq.measurable hf p) hg_seq, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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)
⊢ g =ᶠ[ae μ] g_seq

Tactic:
(ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm

Premises used: Nonempty.some, aeSeq.measure_compl_aeSeqSet_eq_zero, MeasureTheory.ite_ae_eq_of_measure_compl_zero, aeSeqSet, Set.piecewise, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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)
⊢ g =ᶠ[ae μ] g_seq

Tactic:
exact
    (ite_ae_eq_of_measure_compl_zero g (fun _ => hα.some) (aeSeqSet hf p)
        (aeSeq.measure_compl_aeSeqSet_eq_zero hf hg)).symm

Premises used: Nonempty.some, aeSeq.measure_compl_aeSeqSet_eq_zero, MeasureTheory.ite_ae_eq_of_measure_compl_zero, aeSeqSet, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 μ
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
⊢ 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

Premises used: isEmpty_or_nonempty, IsEmpty.exists_iff, Set.setOf_false, isLUB_empty_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)
⊢ Measurable g

Tactic:
Measurable.isLUB (α := αᵒᵈ) hf hg

Premises used: Measurable.isLUB, OrderDual
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
⊢ Measurable g

Tactic:
Measurable.isLUB_of_mem (α := αᵒᵈ) hf hs hg hg' g'_meas

Premises used: Measurable.isLUB_of_mem, OrderDual
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : δ) ∂μ, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)
⊢ AEMeasurable g μ

Tactic:
AEMeasurable.isLUB (α := αᵒᵈ) hf hg

Premises used: AEMeasurable.isLUB, OrderDual
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : TopologicalSpace β
mβ : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : LinearOrder α
inst_5 : OrderTopology α
inst_6 : SecondCountableTopology α
inst_7 : LinearOrder β
inst_8 : OrderClosedTopology β
f : β → α
hf : Monotone f
⊢ Measurable f

Tactic:
suffices h : ∀ x, OrdConnected (f ⁻¹' Ioi x) from measurable_of_Ioi fun x => (h x).measurableSet
  fun _ => ordConnected_def.mpr fun _a ha _ _ _c hc => lt_of_lt_of_le ha (hf hc.1)

Premises used: Iff.mpr, Set.OrdConnected.measurableSet, Set.ordConnected_def, measurable_of_Ioi, And.left, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : TopologicalSpace β
mβ : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : LinearOrder α
inst_5 : OrderTopology α
inst_6 : SecondCountableTopology α
inst_7 : LinearOrder β
inst_8 : OrderClosedTopology β
μ : Measure β
s : Set β
hs : MeasurableSet s
f : β → α
hf : MonotoneOn f s
⊢ AEMeasurable f (μ.restrict s)

Tactic:
have : Monotone (f ∘ (↑) : s → α) := fun ⟨x, hx⟩ ⟨y, hy⟩ => fun (hxy : x ≤ y) => hf hx hy hxy
  aemeasurable_restrict_of_measurable_subtype hs this.measurable

Premises used: aemeasurable_restrict_of_measurable_subtype, _private.0.aemeasurable_restrict_of_monotoneOn.match_1, Monotone.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : TopologicalSpace β
mβ : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : LinearOrder α
inst_5 : OrderTopology α
inst_6 : SecondCountableTopology α
inst_7 : LinearOrder β
inst_8 : OrderClosedTopology β
f : β → α
hf : Antitone f
⊢ Measurable f

Tactic:
@Monotone.measurable αᵒᵈ β _ _ ‹_› _ _ _ _ _ ‹_› _ _ _ hf

Premises used: Monotone.measurable, OrderDual
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : TopologicalSpace β
mβ : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : LinearOrder α
inst_5 : OrderTopology α
inst_6 : SecondCountableTopology α
inst_7 : LinearOrder β
inst_8 : OrderClosedTopology β
μ : Measure β
s : Set β
hs : MeasurableSet s
f : β → α
hf : AntitoneOn f s
⊢ AEMeasurable f (μ.restrict s)

Tactic:
@aemeasurable_restrict_of_monotoneOn αᵒᵈ β _ _ ‹_› _ _ _ _ _ ‹_› _ _ _ _ hs _ hf

Premises used: aemeasurable_restrict_of_monotoneOn, OrderDual
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
choose! : ∀ (M : (x : α) → α) (hM : ∀ x ∈ s, x < M x), MeasurableSet s
⊢ MeasurableSet s

Tactic:
choose! M hM using h'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
rw rw₁ : s = s
⊢ s = interior s ∪ s \ interior s

Tactic:
rw [union_diff_cancel interior_subset]

Premises used: interior_subset, Set.union_diff_cancel
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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

Tactic:
have : s = interior s ∪ s \ interior s := by rw [union_diff_cancel interior_subset]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
rw : MeasurableSet (interior s ∪ s \ interior s)
⊢ MeasurableSet s

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 (interior s ∪ s \ interior s)

Tactic:
isOpen_interior.measurableSet.union H.measurableSet

Premises used: isOpen_interior, Set.Countable.measurableSet, IsOpen.measurableSet, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 (interior s ∪ s \ interior s)

Tactic:
exact isOpen_interior.measurableSet.union H.measurableSet

Premises used: isOpen_interior, Set.Countable.measurableSet, IsOpen.measurableSet, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
suffices : (s \ interior s).Countable
⊢ MeasurableSet s

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
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
⊢ ∀ 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)