α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
⊢ AEMeasurable g
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
⊢ AEMeasurable g
nontriviality α
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
⊢ AEMeasurable g
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
⊢ AEMeasurable g
haveI hα : Nonempty α := inferInstance
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : IsEmpty ι
⊢ AEMeasurable g

case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
⊢ AEMeasurable g
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
⊢ AEMeasurable g
cases' isEmpty_or_nonempty ι with hι hι
case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
⊢ AEMeasurable g
case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
⊢ AEMeasurable g
let p : δ → (ι → α) → Prop := fun x f' => IsGLB { a | ∃ i, f' i = a } (g x)
case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
⊢ AEMeasurable g
case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
⊢ AEMeasurable g
let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
hg_seq : ∀ (b : δ), IsGLB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)
⊢ g =ᵐ[μ] g_seq
case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
hg_seq : ∀ (b : δ), IsGLB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)
⊢ AEMeasurable g
refine' ⟨g_seq, Measurable.isGLB (aeSeq.measurable hf p) hg_seq, _⟩
no goals
case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
hg_seq : ∀ (b : δ), IsGLB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)
⊢ g =ᵐ[μ] g_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
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
✝ : Nontrivial α
hα : Nonempty α
hι : IsEmpty ι
hg : ∀ᵐ (b : δ) ∂μ, IsTop (g b)
⊢ AEMeasurable g
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : IsEmpty ι
⊢ AEMeasurable g
simp only [IsEmpty.exists_iff, setOf_false, isGLB_empty_iff] at hg
no goals
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
✝ : Nontrivial α
hα : Nonempty α
hι : IsEmpty ι
hg : ∀ᵐ (b : δ) ∂μ, IsTop (g b)
⊢ AEMeasurable g
exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (hb _).antisymm (ha _))
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
⊢ IsGLB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
⊢ ∀ (b : δ), IsGLB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)
intro b
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
⊢ IsGLB
    {a |
      ∃ i,
        (if b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x) then mk (f i) (_ : AEMeasurable (f i)) b
          else Nonempty.some (_ : Nonempty α)) =
          a}
    (if b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x) then g b else Nonempty.some hα)
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
⊢ IsGLB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)
simp only [aeSeq, Set.piecewise]
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
⊢ IsGLB {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} (g b)

case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : ¬b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
⊢ IsGLB {a | ∃ i, Nonempty.some (_ : Nonempty α) = a} (Nonempty.some hα)
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
⊢ IsGLB
    {a |
      ∃ i,
        (if b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x) then mk (f i) (_ : AEMeasurable (f i)) b
          else Nonempty.some (_ : Nonempty α)) =
          a}
    (if b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x) then g b else Nonempty.some hα)
split_ifs with h
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
h_set_eq : {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} = {a | ∃ i, f i b = a}
⊢ IsGLB {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} (g b)
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
⊢ IsGLB {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} (g b)
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]
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
h_set_eq : {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} = {a | ∃ i, f i b = a}
⊢ IsGLB {a | ∃ i, f i b = a} (g b)
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
h_set_eq : {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} = {a | ∃ i, f i b = a}
⊢ IsGLB {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} (g b)
rw [h_set_eq]
no goals
case inl
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
h_set_eq : {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} = {a | ∃ i, f i b = a}
⊢ IsGLB {a | ∃ i, f i b = a} (g b)
exact aeSeq.fun_prop_of_mem_aeSeqSet hf h
case h
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
x : α
⊢ x ∈ {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} ↔ x ∈ {a | ∃ i, f i b = a}
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
⊢ {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} = {a | ∃ i, f i b = a}
ext x
no goals
case h
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
x : α
⊢ x ∈ {a | ∃ i, mk (f i) (_ : AEMeasurable (f i)) b = a} ↔ x ∈ {a | ∃ i, f i b = a}
simp_rw [Set.mem_setOf_eq, aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h]
no goals
case inr
α : Type u_3
β : Type ?u.1213665
γ : Type ?u.1213668
γ₂ : Type ?u.1213671
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)
✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := piecewise (aeSeqSet hf p) g fun x => Nonempty.some hα
b : δ
h : ¬b ∈ aeSeqSet hf fun x f' => IsGLB {a | ∃ i, f' i = a} (g x)
⊢ IsGLB {a | ∃ i, Nonempty.some (_ : Nonempty α) = a} (Nonempty.some hα)
exact IsLeast.isGLB ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, fun x ⟨i, hi⟩ => hi.le⟩