-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem AEMeasurable.isLUB {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α}
    (hf : ∀ i, AEMeasurable (f i) μ) (hg : ∀ᵐ b ∂μ, IsLUB { a | ∃ i, f i b = a } (g b)) :
    AEMeasurable g μ

Proof state:
case h
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some
b : δ
h : b ∈ aeSeqSet hf p
x : α
⊢ x ∈ {a | ∃ i, mk (f i) ⋯ b = a} ↔ x ∈ {a | ∃ i, f i b = a}

Tactic:
simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]

Result:
no goals

Proof state:
case pos
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some
b : δ
h : b ∈ aeSeqSet hf p
h_set_eq : {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

Result:
no goals

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
⊢ AEMeasurable g μ

Tactic:
nontriviality α

Result:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
⊢ AEMeasurable g μ

Proof state:
case inr
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some
hg_seq : ∀ (b : δ), IsLUB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)
⊢ AEMeasurable g μ

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

Result:
case inr
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some
hg_seq : ∀ (b : δ), IsLUB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)
⊢ g =ᶠ[ae μ] g_seq

Proof state:
case inr
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
⊢ AEMeasurable g μ

Tactic:
let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some

Result:
case inr
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some
⊢ AEMeasurable g μ

Proof state:
case neg
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some
b : δ
h : b ∉ aeSeqSet hf p
⊢ IsLUB {a | ∃ i, ⋯.some = a} hα.some

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

Result:
no goals

Proof state:
case pos
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some
b : δ
h : b ∈ aeSeqSet hf p
⊢ IsLUB {a | ∃ i, mk (f i) ⋯ b = a} (g b)

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]

Result:
case pos
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x => hα.some
b : δ
h : b ∈ aeSeqSet hf p
h_set_eq : {a | ∃ i, mk (f i) ⋯ b = a} = {a | ∃ i, f i b = a}
⊢ IsLUB {a | ∃ i, mk (f i) ⋯ b = a} (g b)