case none
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
t : Interval α
⊢ ↑⊥ = ↑⊥ ∩ ↑t
case none
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
t : Interval α
⊢ ↑(none ⊓ t) = ↑none ∩ ↑t
rw [WithBot.none_eq_bot, bot_inf_eq]
no goals
case none
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
t : Interval α
⊢ ↑⊥ = ↑⊥ ∩ ↑t
exact (empty_inter _).symm
case some.none
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : NonemptyInterval α
⊢ ↑⊥ = ↑(some s) ∩ ↑⊥
case some.none
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : NonemptyInterval α
⊢ ↑(some s ⊓ none) = ↑(some s) ∩ ↑none
rw [WithBot.none_eq_bot, inf_bot_eq]
no goals
case some.none
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : NonemptyInterval α
⊢ ↑⊥ = ↑(some s) ∩ ↑⊥
exact (inter_empty _).symm
case some.some
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s t : NonemptyInterval α
⊢ ↑(if h : s.fst ≤ t.snd ∧ t.fst ≤ s.snd then
        some
          { toProd := (s.fst ⊔ t.fst, s.snd ⊓ t.snd),
            fst_le_snd := (_ : s.fst ⊔ t.fst ≤ (s.fst ⊔ t.fst, s.snd ⊓ t.snd).snd) }
      else ⊥) =
    Icc (s.fst ⊔ t.fst) (s.snd ⊓ t.snd)
case some.some
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s t : NonemptyInterval α
⊢ ↑(some s ⊓ some t) = ↑(some s) ∩ ↑(some t)
refine' (_ : setLike.coe (dite
  (s.toProd.fst ≤ t.toProd.snd ∧ t.toProd.fst ≤ s.toProd.snd)
  _ _) = _).trans Icc_inter_Icc.symm
case some.some.inl
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s t : NonemptyInterval α
h : s.fst ≤ t.snd ∧ t.fst ≤ s.snd
⊢ ↑(some
        { toProd := (s.fst ⊔ t.fst, s.snd ⊓ t.snd),
          fst_le_snd := (_ : s.fst ⊔ t.fst ≤ (s.fst ⊔ t.fst, s.snd ⊓ t.snd).snd) }) =
    Icc (s.fst ⊔ t.fst) (s.snd ⊓ t.snd)

case some.some.inr
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s t : NonemptyInterval α
h : ¬(s.fst ≤ t.snd ∧ t.fst ≤ s.snd)
⊢ ↑⊥ = Icc (s.fst ⊔ t.fst) (s.snd ⊓ t.snd)
case some.some
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s t : NonemptyInterval α
⊢ ↑(if h : s.fst ≤ t.snd ∧ t.fst ≤ s.snd then
        some
          { toProd := (s.fst ⊔ t.fst, s.snd ⊓ t.snd),
            fst_le_snd := (_ : s.fst ⊔ t.fst ≤ (s.fst ⊔ t.fst, s.snd ⊓ t.snd).snd) }
      else ⊥) =
    Icc (s.fst ⊔ t.fst) (s.snd ⊓ t.snd)
split_ifs with h
no goals
case some.some.inl
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s t : NonemptyInterval α
h : s.fst ≤ t.snd ∧ t.fst ≤ s.snd
⊢ ↑(some
        { toProd := (s.fst ⊔ t.fst, s.snd ⊓ t.snd),
          fst_le_snd := (_ : s.fst ⊔ t.fst ≤ (s.fst ⊔ t.fst, s.snd ⊓ t.snd).snd) }) =
    Icc (s.fst ⊔ t.fst) (s.snd ⊓ t.snd)
rfl
no goals
case some.some.inr
α : Type u_1
β : Type ?u.38930
γ : Type ?u.38933
δ : Type ?u.38936
ι : Sort ?u.38939
κ : ι → Sort ?u.38944
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s t : NonemptyInterval α
h : ¬(s.fst ≤ t.snd ∧ t.fst ≤ s.snd)
⊢ ↑⊥ = Icc (s.fst ⊔ t.fst) (s.snd ⊓ t.snd)
exact (Icc_eq_empty fun H =>
  h ⟨le_sup_left.trans <| H.trans inf_le_right,
  le_sup_right.trans <| H.trans inf_le_left⟩).symm