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
inst_5 : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
inl :
  ∀ (hs : MeasurableSet.{u_4} (α := δ) ∅)
    (hg : ∀ (b : δ), Membership.mem (γ := Set δ) ∅ b → IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : EqOn g g' ∅ᶜ),
    Measurable g
inl₁ : ∀ (x : δ) (hx : x ∈ s), Measurable g
⊢ Measurable g

Tactic:
rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩

Premises used: Set.eq_empty_or_nonempty, 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
inst_5 : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
g'_meas : Measurable g'
hι : IsEmpty ι
hs : MeasurableSet.{u_4} (α := δ) ∅
hg : ∀ (b : δ), Membership.mem (γ := Set δ) ∅ b → IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' ∅ᶜ
⊢ Measurable g'

Tactic:
g'_meas
-- 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)
g'_meas : Measurable g'
hι : IsEmpty ι
hs : MeasurableSet.{u_4} (α := δ) ∅
hg : ∀ (b : δ), Membership.mem (γ := Set δ) ∅ b → IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' ∅ᶜ
h : g = g'
⊢ Measurable g

Tactic:
convert! g'_meas
-- 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)
g'_meas : Measurable g'
hι : IsEmpty ι
hs : MeasurableSet.{u_4} (α := δ) ∅
hg : ∀ (b : δ), Membership.mem (γ := Set δ) ∅ b → IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' ∅ᶜ
h : ∀ (hg' : EqOn g g' univ), g = g'
h₁ h₂ h₃ h₄ : ∀ (hg' : g = g'), g = g'
⊢ g = g'

Tactic:
rwa [compl_empty, eqOn_univ] at hg'

Premises used: Set.eqOn_univ, Set.compl_empty
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
⊢ ∀ b ∈ s, IsBot (g b)

Tactic:
simpa using hg
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
⊢ ∀ b ∈ s, IsBot (g b)

Tactic:
have A : ∀ b ∈ s, IsBot (g b) := by simpa using hg
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
b : δ
hb : b ∈ s
⊢ g b = g x

Tactic:
apply le_antisymm (A b hb (g x)) (A x hx (g b))

Premises used: le_antisymm
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
⊢ ∀ b ∈ s, g b = g x

Tactic:
have B : ∀ b ∈ s, g b = g x := by
        intro b hb
        apply le_antisymm (A b hb (g x)) (A x hx (g b))
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
h : ∀ (b : δ), g b = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g' b
⊢ g = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g'

Tactic:
ext b
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
b : δ
pos : ∀ (hb : b ∈ s), g b = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g' b
neg : ∀ (hb : b ∉ s), g b = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g' b
⊢ g b = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g' b

Tactic:
by_cases hb : b ∈ s
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
b : δ
hb : b ∈ s
⊢ g b = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g' b

Tactic:
simp [hb, B]
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
b : δ
hb : b ∉ s
⊢ g b = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g' b

Tactic:
simp [hb, hg' hb]
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
⊢ g = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g'

Tactic:
have : g = s.piecewise (fun _y ↦ g x) g' := by
        ext b
        by_cases hb : b ∈ s
        · simp [hb, B]
        · simp [hb, hg' hb]
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
this : g = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g'
inl : Measurable (s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g')
⊢ Measurable g

Tactic:
rw [this]
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
this : g = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g'
⊢ Measurable (s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g')

Tactic:
Measurable.piecewise hs measurable_const g'_meas

Premises used: Measurable.piecewise, measurable_const
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
this : g = s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g'
⊢ Measurable (s.piecewise (β := fun (_y : δ) ↦ α) (fun (_y : δ) ↦ g x) g')

Tactic:
exact Measurable.piecewise hs measurable_const g'_meas

Premises used: Measurable.piecewise, measurable_const
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨i⟩
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun (i : ι) ↦ s.piecewise (β := fun (a : δ) ↦ α) (f i) g'
inr : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), f' i b = a} (g b)
⊢ Measurable g

Tactic:
suffices ∀ b, IsLUB { a | ∃ i, f' i b = a } (g b) from
      Measurable.isLUB (fun i ↦ Measurable.piecewise hs (hf i) g'_meas) this
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun (i : ι) ↦ s.piecewise (β := fun (a : δ) ↦ α) (f i) g'
b : δ
pos : ∀ (hb : b ∈ s), IsLUB {a : α | ∃ (i : ι), f' i b = a} (g b)
neg : ∀ (hb : b ∉ s), IsLUB {a : α | ∃ (i : ι), f' i b = a} (g b)
⊢ IsLUB {a : α | ∃ (i : ι), f' i b = a} (g b)

Tactic:
by_cases hb : b ∈ s
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i_1 : ι
this : Nonempty ι
f' : ι → δ → α := fun (i : ι) ↦ s.piecewise (β := fun (a : δ) ↦ α) (f i) g'
b : δ
hb : b ∈ s
i : ι
⊢ f' i b = f i b

Tactic:
simp [f', hb]
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun (i : ι) ↦ s.piecewise (β := fun (a : δ) ↦ α) (f i) g'
b : δ
hb : b ∈ s
⊢ ∀ (i : ι), f' i b = f i b

Tactic:
have A : ∀ i, f' i b = f i b := fun i ↦ by simp [f', hb]
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun (i : ι) ↦ s.piecewise (β := fun (a : δ) ↦ α) (f i) g'
b : δ
hb : b ∈ s
A : ∀ (i : ι), f' i b = f i b
⊢ IsLUB {a : α | ∃ (i : ι), f' i b = a} (g b)

Tactic:
simpa [A] using hg b hb
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i_1 : ι
this : Nonempty ι
f' : ι → δ → α := fun (i : ι) ↦ s.piecewise (β := fun (a : δ) ↦ α) (f i) g'
b : δ
hb : b ∉ s
i : ι
⊢ f' i b = g' b

Tactic:
simp [f', hb]
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun (i : ι) ↦ s.piecewise (β := fun (a : δ) ↦ α) (f i) g'
b : δ
hb : b ∉ s
⊢ ∀ (i : ι), f' i b = g' b

Tactic:
have A : ∀ i, f' i b = g' b := fun i ↦ by simp [f', hb]
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun (i : ι) ↦ s.piecewise (β := fun (a : δ) ↦ α) (f i) g'
b : δ
hb : b ∉ s
A : ∀ (i : ι), f' i b = g' b
⊢ IsLUB {a : α | ∃ (i : ι), f' i b = a} (g b)

Tactic:
simp [A, hg' hb, isLUB_singleton]

Premises used: isLUB_singleton
-- 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, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
inl : ∀ (hι : IsEmpty ι), Measurable g
inr inr₁ : ∀ (i : ι), Measurable g
⊢ Measurable g

Tactic:
classical
  rcases isEmpty_or_nonempty ι with hι | ⟨⟨i⟩⟩
  · rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩
    · convert! g'_meas
      rwa [compl_empty, eqOn_univ] at hg'
    · have A : ∀ b ∈ s, IsBot (g b) := by simpa using hg
      have B : ∀ b ∈ s, g b = g x := by
        intro b hb
        apply le_antisymm (A b hb (g x)) (A x hx (g b))
      have : g = s.piecewise (fun _y ↦ g x) g' := by
        ext b
        by_cases hb : b ∈ s
        · simp [hb, B]
        · simp [hb, hg' hb]
      rw [this]
      exact Measurable.piecewise hs measurable_const g'_meas
  · have : Nonempty ι := ⟨i⟩
    let f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
    suffices ∀ b, IsLUB { a | ∃ i, f' i b = a } (g b) from
      Measurable.isLUB (fun i ↦ Measurable.piecewise hs (hf i) g'_meas) this
    intro b
    by_cases hb : b ∈ s
    · have A : ∀ i, f' i b = f i b := fun i ↦ by simp [f', hb]
      simpa [A] using hg b hb
    · have A : ∀ i, f' i b = g' b := fun i ↦ by simp [f', hb]
      simp [A, hg' hb, isLUB_singleton]

Premises used: isLUB_singleton, Measurable.piecewise, Set.eqOn_univ, isEmpty_or_nonempty, Set.eq_empty_or_nonempty, Set.compl_empty, measurable_const, 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)
⊢ Nontrivial α

Tactic:
nontriviality α
-- 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 α
⊢ Nonempty α

Tactic:
haveI hα : Nonempty α := inferInstance
-- 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 α
inl : ∀ (hι : IsEmpty ι), AEMeasurable g μ
inr : ∀ (hι : Nonempty ι), AEMeasurable g μ
⊢ AEMeasurable g μ

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Premises used: isEmpty_or_nonempty
-- 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ι : IsEmpty ι
⊢ ∀ᵐ (b : δ) ∂μ, IsBot (g b)

Tactic:
simp only [IsEmpty.exists_iff, setOf_false, isLUB_empty_iff] at hg

Premises used: 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
μ : Measure δ
inst_5 : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : Nontrivial α
hα : Nonempty α
hι : IsEmpty ι
hg : ∀ᵐ (b : δ) ∂μ, IsBot (g b)
⊢ AEMeasurable g μ

Tactic:
aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))

Premises used: LE.le.antisymm, Filter.Eventually.mono, aemeasurable_const'
-- 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) μ
h : Nontrivial α
hα : Nonempty α
hι : IsEmpty ι
hg : ∀ᵐ (b : δ) ∂μ, IsBot (g b)
⊢ AEMeasurable g μ

Tactic:
exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))

Premises used: LE.le.antisymm, Filter.Eventually.mono, aemeasurable_const'
-- 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 : δ
simp :
  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)
⊢ IsLUB {a : α | ∃ (i : ι), aeSeq hf p i b = a} (g_seq b)

Tactic:
simp only [g_seq, aeSeq, Set.piecewise]

Premises used: aeSeq, Set.piecewise