-- Mathlib/Order/Interval/Basic.lean
theorem coe_inf : ∀ s t : Interval α, (↑(s ⊓ t) : Set α) = ↑s ∩ ↑t
  | ⊥, _ => by
    rw [bot_inf_eq]
    exact (empty_inter _).symm
  | (s : NonemptyInterval α), ⊥ => by
    rw [inf_bot_eq]
    exact (inter_empty _).symm
  | (s : NonemptyInterval α), (t : NonemptyInterval α) => by
    simp only [Min.min, coe_coe, NonemptyInterval.coe_def, Icc_inter_Icc,
      SemilatticeInf.inf, Lattice.inf]
    split_ifs with h
    · simp only [coe_coe, NonemptyInterval.coe_def]
    · refine (Icc_eq_empty <| mt ?_ h).symm
      exact fun h ↦ ⟨le_sup_left.trans <| h.trans inf_le_right,
        le_sup_right.trans <| h.trans inf_le_left⟩

Proof state:
case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ s.toProd.1 ⊔ t.toProd.1 ≤ Lattice.inf s.toProd.2 t.toProd.2 → s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2

Tactic:
exact fun h ↦ ⟨le_sup_left.trans <| h.trans inf_le_right,
  le_sup_right.trans <| h.trans inf_le_left⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s : NonemptyInterval α
⊢ ↑(↑s ⊓ ⊥) = ↑↑s ∩ ↑⊥

Tactic:
rw [inf_bot_eq]

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s : NonemptyInterval α
⊢ ↑⊥ = ↑↑s ∩ ↑⊥

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s : NonemptyInterval α
⊢ ↑⊥ = ↑↑s ∩ ↑⊥

Tactic:
exact (inter_empty _).symm

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ↑⊥ = Icc (s.toProd.1 ⊔ t.toProd.1) (Lattice.inf s.toProd.2 t.toProd.2)

Tactic:
refine (Icc_eq_empty <| mt ?_ h).symm

Result:
case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ s.toProd.1 ⊔ t.toProd.1 ≤ Lattice.inf s.toProd.2 t.toProd.2 → s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2

Proof state:
case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : NonemptyInterval α
h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ ↑↑{ toProd := (s.toProd.1 ⊔ t.toProd.1, Lattice.inf s.toProd.2 t.toProd.2), fst_le_snd := ⋯ } =
    Icc (s.toProd.1 ⊔ t.toProd.1) (Lattice.inf s.toProd.2 t.toProd.2)

Tactic:
simp only [coe_coe, NonemptyInterval.coe_def]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x✝ : Interval α
⊢ ↑⊥ = ↑⊥ ∩ ↑x✝

Tactic:
exact (empty_inter _).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x✝ : Interval α
⊢ ↑(⊥ ⊓ x✝) = ↑⊥ ∩ ↑x✝

Tactic:
rw [bot_inf_eq]

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x✝ : Interval α
⊢ ↑⊥ = ↑⊥ ∩ ↑x✝

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : NonemptyInterval α
⊢ ↑(if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        ↑{ toProd := (s.toProd.1 ⊔ t.toProd.1, Lattice.inf s.toProd.2 t.toProd.2), fst_le_snd := ⋯ }
      else ⊥) =
    Icc (s.toProd.1 ⊔ t.toProd.1) (Lattice.inf s.toProd.2 t.toProd.2)

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : NonemptyInterval α
h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ ↑↑{ toProd := (s.toProd.1 ⊔ t.toProd.1, Lattice.inf s.toProd.2 t.toProd.2), fst_le_snd := ⋯ } =
    Icc (s.toProd.1 ⊔ t.toProd.1) (Lattice.inf s.toProd.2 t.toProd.2)

case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ↑⊥ = Icc (s.toProd.1 ⊔ t.toProd.1) (Lattice.inf s.toProd.2 t.toProd.2)

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : NonemptyInterval α
⊢ ↑(↑s ⊓ ↑t) = ↑↑s ∩ ↑↑t

Tactic:
simp only [Min.min, coe_coe, NonemptyInterval.coe_def, Icc_inter_Icc,
  SemilatticeInf.inf, Lattice.inf]

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : NonemptyInterval α
⊢ ↑(if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        ↑{ toProd := (s.toProd.1 ⊔ t.toProd.1, Lattice.inf s.toProd.2 t.toProd.2), fst_le_snd := ⋯ }
      else ⊥) =
    Icc (s.toProd.1 ⊔ t.toProd.1) (Lattice.inf s.toProd.2 t.toProd.2)