-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Measurable.iSup {ι} [Countable ι] {f : ι → δ → α} (hf : ∀ i, Measurable (f i)) :
    Measurable (fun b ↦ ⨆ i, f i b)

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun b => ⨆ i, f i b

Tactic:
rcases isEmpty_or_nonempty ι with hι|hι

Result:
case inl
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : IsEmpty ι
⊢ Measurable fun b => ⨆ i, f i b

case inr
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
⊢ Measurable fun b => ⨆ i, f i b

Proof state:
case hs
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
b : δ
hb : b ∈ {b | BddAbove (range fun i => f i b)}ᶜ
⊢ ¬BddAbove (range fun i => f i b)

Tactic:
exact hb

Result:
no goals

Proof state:
case inr
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
⊢ Measurable fun b => ⨆ i, f i b

Tactic:
apply Measurable.isLUB_of_mem hf A _ _ this

Result:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
⊢ ∀ b ∈ {b | BddAbove (range fun i => f i b)}, IsLUB {a | ∃ i, f i b = a} (⨆ i, f i b)

α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
⊢ EqOn (fun b => ⨆ i, f i b) (fun _b => sSup ∅) {b | BddAbove (range fun i => f i b)}ᶜ

Proof state:
case inl
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : IsEmpty ι
⊢ Measurable fun b => ⨆ i, f i b

Tactic:
simp [iSup_of_empty']

Result:
no goals

Proof state:
case intro.H.intro
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
b : δ
c : α
hc : c ∈ upperBounds (range fun i => f i b)
i : ι
⊢ (fun y => f y b) i ≤ c

Tactic:
exact hc (mem_range_self i)

Result:
no goals

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
b : δ
hb : b ∈ {b | BddAbove (range fun i => f i b)}ᶜ
⊢ (fun b => ⨆ i, f i b) b = (fun _b => sSup ∅) b

Tactic:
apply csSup_of_not_bddAbove

Result:
case hs
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
b : δ
hb : b ∈ {b | BddAbove (range fun i => f i b)}ᶜ
⊢ ¬BddAbove (range fun i => f i b)

Proof state:
case intro.H
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
b : δ
c : α
hc : c ∈ upperBounds (range fun i => f i b)
⊢ BddAbove (range fun y => f y b)

Tactic:
refine ⟨c, ?_⟩

Result:
case intro.H
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
b : δ
c : α
hc : c ∈ upperBounds (range fun i => f i b)
⊢ c ∈ upperBounds (range fun y => f y b)

Proof state:
case intro.H
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
b : δ
c : α
hc : c ∈ upperBounds (range fun i => f i b)
⊢ c ∈ upperBounds (range fun y => f y b)

Tactic:
rintro d ⟨i, rfl⟩

Result:
case intro.H.intro
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i => f i b)}
this : Measurable fun _b => sSup ∅
b : δ
c : α
hc : c ∈ upperBounds (range fun i => f i b)
i : ι
⊢ (fun y => f y b) i ≤ c