-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Measurable.biSup {ι} (s : Set ι) {f : ι → δ → α} (hs : s.Countable)
    (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun b => ⨆ i ∈ s, 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 α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = (⨆ i, f (↑i) b) ⊔ sSup ∅
⊢ Measurable fun a => ⨆ i, f (↑i) a

Tactic:
exact .iSup (fun (i : s) ↦ hf i i.2)

Result:
no goals

Proof state:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
⊢ Measurable fun b => ⨆ i ∈ s, f i b

Tactic:
have : ∀ b, ⨆ i ∈ s, f i b = (⨆ (i : s), f i b) ⊔ sSup ∅ :=
  fun b ↦ cbiSup_eq_of_not_forall (f := fun i ↦ f i b) H

Result:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = (⨆ i, f (↑i) b) ⊔ sSup ∅
⊢ Measurable fun b => ⨆ i ∈ s, 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 α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun b => ⨆ i ∈ s, f i b

Tactic:
haveI : Encodable s := hs.toEncodable

Result:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
⊢ Measurable fun b => ⨆ i ∈ s, f i b

Proof state:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = (⨆ i, f (↑i) b) ⊔ sSup ∅
⊢ Measurable fun b => (⨆ i, f (↑i) b) ⊔ sSup ∅

Tactic:
apply Measurable.sup _ measurable_const

Result:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = (⨆ i, f (↑i) b) ⊔ sSup ∅
⊢ Measurable fun a => ⨆ i, f (↑i) a

Proof state:
case pos
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
H : ∀ (i : ι), i ∈ s
⊢ Measurable fun b => ⨆ i ∈ s, f i b

Tactic:
have : ∀ b, ⨆ i ∈ s, f i b = ⨆ (i : s), f i b :=
  fun b ↦ cbiSup_eq_of_forall (f := fun i ↦ f i b) H

Result:
case pos
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = ⨆ i, f (↑i) b
⊢ Measurable fun b => ⨆ i ∈ s, f i b

Proof state:
case pos
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = ⨆ i, f (↑i) b
⊢ Measurable fun b => ⨆ i ∈ s, f i b

Tactic:
simp only [this]

Result:
case pos
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = ⨆ i, f (↑i) b
⊢ 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 α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
⊢ Measurable fun b => ⨆ i ∈ s, f i b

Tactic:
by_cases H : ∀ i, i ∈ s

Result:
case pos
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
H : ∀ (i : ι), i ∈ s
⊢ Measurable fun b => ⨆ i ∈ s, f i b

case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
⊢ Measurable fun b => ⨆ i ∈ s, f i b

Proof state:
case pos
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = ⨆ i, f (↑i) b
⊢ Measurable fun b => ⨆ i, f (↑i) b

Tactic:
exact .iSup (fun (i : s) ↦ hf i i.2)

Result:
no goals