α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
⊢ ↑(if h : ¬⊥ ∈ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd then
        some
          { toProd := (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst, ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd),
            fst_le_snd :=
              (_ :
                (⨆ (i : NonemptyInterval α) (_ : ↑i ∈ S), i.fst) ≤
                  (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst,
                      ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd).snd) }
      else ⊥) =
    ⋂ (s : Interval α) (_ : s ∈ S), ↑s
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
⊢ ↑(sInf S) = ⋂ (s : Interval α) (_ : s ∈ S), ↑s
change setLike.coe (dite _ _ _) = ⋂ (s : Interval α) (_ : s ∈ S), (s : Set α)
case inl
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬⊥ ∈ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
⊢ ↑(some
        { toProd := (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst, ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd),
          fst_le_snd :=
            (_ :
              (⨆ (i : NonemptyInterval α) (_ : ↑i ∈ S), i.fst) ≤
                (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst,
                    ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd).snd) }) =
    ⋂ (s : Interval α) (_ : s ∈ S), ↑s

case inr
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬(¬⊥ ∈ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd)
⊢ ↑⊥ = ⋂ (s : Interval α) (_ : s ∈ S), ↑s
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
⊢ ↑(if h : ¬⊥ ∈ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd then
        some
          { toProd := (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst, ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd),
            fst_le_snd :=
              (_ :
                (⨆ (i : NonemptyInterval α) (_ : ↑i ∈ S), i.fst) ≤
                  (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst,
                      ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd).snd) }
      else ⊥) =
    ⋂ (s : Interval α) (_ : s ∈ S), ↑s
split_ifs with h
case inr
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ⊥ ∈ S ∨ ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
⊢ ↑⊥ = ⋂ (s : Interval α) (_ : s ∈ S), ↑s
case inr
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬(¬⊥ ∈ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd)
⊢ ↑⊥ = ⋂ (s : Interval α) (_ : s ∈ S), ↑s
simp_rw [not_and_or, Classical.not_not] at h
case inr.inl
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ⊥ ∈ S
⊢ ↑⊥ = ⋂ (s : Interval α) (_ : s ∈ S), ↑s

case inr.inr
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
⊢ ↑⊥ = ⋂ (s : Interval α) (_ : s ∈ S), ↑s
case inr
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ⊥ ∈ S ∨ ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
⊢ ↑⊥ = ⋂ (s : Interval α) (_ : s ∈ S), ↑s
rcases h with h | h
case inl.h
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬⊥ ∈ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
x✝ : α
⊢ x✝ ∈
      ↑(some
          { toProd := (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst, ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd),
            fst_le_snd :=
              (_ :
                (⨆ (i : NonemptyInterval α) (_ : ↑i ∈ S), i.fst) ≤
                  (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst,
                      ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd).snd) }) ↔
    x✝ ∈ ⋂ (s : Interval α) (_ : s ∈ S), ↑s
case inl
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬⊥ ∈ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
⊢ ↑(some
        { toProd := (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst, ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd),
          fst_le_snd :=
            (_ :
              (⨆ (i : NonemptyInterval α) (_ : ↑i ∈ S), i.fst) ≤
                (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst,
                    ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd).snd) }) =
    ⋂ (s : Interval α) (_ : s ∈ S), ↑s
ext
no goals
case inl.h
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬⊥ ∈ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
x✝ : α
⊢ x✝ ∈
      ↑(some
          { toProd := (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst, ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd),
            fst_le_snd :=
              (_ :
                (⨆ (i : NonemptyInterval α) (_ : ↑i ∈ S), i.fst) ≤
                  (⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst,
                      ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd).snd) }) ↔
    x✝ ∈ ⋂ (s : Interval α) (_ : s ∈ S), ↑s
simp [WithBot.some_eq_coe, Interval.forall, h.1, ← forall_and, ← NonemptyInterval.mem_def]
case inr.inl
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ⊥ ∈ S
⊢ (⋂ (s : Interval α) (_ : s ∈ S), ↑s) ⊆ ∅
case inr.inl
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ⊥ ∈ S
⊢ ↑⊥ = ⋂ (s : Interval α) (_ : s ∈ S), ↑s
refine' (eq_empty_of_subset_empty _).symm
no goals
case inr.inl
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ⊥ ∈ S
⊢ (⋂ (s : Interval α) (_ : s ∈ S), ↑s) ⊆ ∅
exact iInter₂_subset_of_subset _ h Subset.rfl
case inr.inr
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
⊢ ¬Set.Nonempty (⋂ (s : Interval α) (_ : s ∈ S), ↑s)
case inr.inr
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
⊢ ↑⊥ = ⋂ (s : Interval α) (_ : s ∈ S), ↑s
refine' (not_nonempty_iff_eq_empty.1 _).symm
case inr.inr.intro
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
x : α
hx : x ∈ ⋂ (s : Interval α) (_ : s ∈ S), ↑s
⊢ False
case inr.inr
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
⊢ ¬Set.Nonempty (⋂ (s : Interval α) (_ : s ∈ S), ↑s)
rintro ⟨x, hx⟩
case inr.inr.intro
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
x : α
hx : ∀ (i : Interval α), i ∈ S → x ∈ ↑i
⊢ False
case inr.inr.intro
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
x : α
hx : x ∈ ⋂ (s : Interval α) (_ : s ∈ S), ↑s
⊢ False
rw [mem_iInter₂] at hx
no goals
case inr.inr.intro
α : Type u_1
β : Type ?u.53885
γ : Type ?u.53888
δ : Type ?u.53891
ι : Sort ?u.53894
κ : ι → Sort ?u.53899
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd
x : α
hx : ∀ (i : Interval α), i ∈ S → x ∈ ↑i
⊢ False
exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2