awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
rw : s ≤ { fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }
hc₁ : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
⊢ (↑s : Interval α) ≤
    if h : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥

Tactic:
rw [dif_pos, Interval.coe_le_coe]

Premises used: Interval.coe_le_coe, dif_pos
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ s ≤ { fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }

Tactic:
⟨sup_le hb.1 hc.1, le_inf hb.2 hc.2⟩

Premises used: le_inf, And.right, And.left, And.intro, sup_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ s ≤ { fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }

Tactic:
exact ⟨sup_le hb.1 hc.1, le_inf hb.2 hc.2⟩
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ t.toProd.1 ≤ s.toProd.1

Tactic:
rcases hb with ⟨hb₁, hb₂⟩
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
hb₁ : t.toProd.1 ≤ s.toProd.1
⊢ s.toProd.2 ≤ t.toProd.2

Tactic:
rcases hb with ⟨hb₁, hb₂⟩
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hc : s ≤ c
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
⊢ c.toProd.1 ≤ s.toProd.1

Tactic:
rcases hc with ⟨hc₁, hc₂⟩
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hc : s ≤ c
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
hc₁ : c.toProd.1 ≤ s.toProd.1
⊢ s.toProd.2 ≤ c.toProd.2

Tactic:
rcases hc with ⟨hc₁, hc₂⟩
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
hc₁ : c.toProd.1 ≤ s.toProd.1
hc₂ : s.toProd.2 ≤ c.toProd.2
⊢ t.toProd.1 ≤ s.toProd.1

Tactic:
change t.toProd.fst ≤ s.toProd.fst at hb₁

Premises used: Prod.fst, NonemptyInterval.toProd
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb₂ : s.toProd.2 ≤ t.toProd.2
hc₁ : c.toProd.1 ≤ s.toProd.1
hc₂ : s.toProd.2 ≤ c.toProd.2
hb₁ : t.toProd.1 ≤ s.toProd.1
⊢ s.toProd.2 ≤ t.toProd.2

Tactic:
change s.toProd.snd ≤ t.toProd.snd at hb₂

Premises used: NonemptyInterval.toProd, Prod.snd
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hc₁ : c.toProd.1 ≤ s.toProd.1
hc₂ : s.toProd.2 ≤ c.toProd.2
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
⊢ c.toProd.1 ≤ s.toProd.1

Tactic:
change c.toProd.fst ≤ s.toProd.fst at hc₁

Premises used: Prod.fst, NonemptyInterval.toProd
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hc₂ : s.toProd.2 ≤ c.toProd.2
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
hc₁ : c.toProd.1 ≤ s.toProd.1
⊢ s.toProd.2 ≤ c.toProd.2

Tactic:
change s.toProd.snd ≤ c.toProd.snd at hc₂

Premises used: NonemptyInterval.toProd, Prod.snd
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
hc₁ : c.toProd.1 ≤ s.toProd.1
hc₂ : s.toProd.2 ≤ c.toProd.2
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2

Tactic:
⟨hb₁.trans <| s.fst_le_snd.trans hc₂, hc₁.trans <| s.fst_le_snd.trans hb₂⟩

Premises used: And.intro, LE.le.trans, NonemptyInterval.fst_le_snd
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t c : NonemptyInterval α
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
hc₁ : c.toProd.1 ≤ s.toProd.1
hc₂ : s.toProd.2 ≤ c.toProd.2
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2

Tactic:
exact ⟨hb₁.trans <| s.fst_le_snd.trans hc₂, hc₁.trans <| s.fst_le_snd.trans hb₂⟩
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
⊢ (↑s : Interval α) ⊓ (↑t : Interval α) =
    if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
      (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
x : Interval α
⊢ (↑⊥ : Set α) = (↑⊥ : Set α) ∩ (↑x : Set α)

Tactic:
(empty_inter _).symm

Premises used: Set.empty_inter, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
x : Interval α
⊢ (↑⊥ : Set α) = (↑⊥ : Set α) ∩ (↑x : Set α)

Tactic:
exact (empty_inter _).symm

Premises used: Set.empty_inter, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s : NonemptyInterval α
⊢ (↑⊥ : Set α) = (↑(↑s : Interval α) : Set α) ∩ (↑⊥ : Set α)

Tactic:
(inter_empty _).symm

Premises used: Set.inter_empty, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s : NonemptyInterval α
⊢ (↑⊥ : Set α) = (↑(↑s : Interval α) : Set α) ∩ (↑⊥ : Set α)

Tactic:
exact (inter_empty _).symm

Premises used: Set.inter_empty, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
simp :
  (↑(if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
          (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
            Interval α)
        else ⊥) :
      Set α) =
    Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)
⊢ (↑((↑s : Interval α) ⊓ (↑t : Interval α)) : Set α) = (↑(↑s : Interval α) : Set α) ∩ (↑(↑t : Interval α) : Set α)

Tactic:
simp only [coe_coe, NonemptyInterval.coe_def, Icc_inter_Icc, inf_coe]

Premises used: Set.Icc_inter_Icc, Interval.coe_coe, Interval.inf_coe, NonemptyInterval.coe_def
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
pos :
  ∀ (h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2),
    (↑(↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
            Interval α) :
        Set α) =
      Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)
neg :
  ∀ (h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)),
    (↑⊥ : Set α) = Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)
⊢ (↑(if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
          (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
            Interval α)
        else ⊥) :
      Set α) =
    Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ (↑(↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
          Interval α) :
      Set α) =
    Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)

Tactic:
simp only [coe_coe, NonemptyInterval.coe_def]

Premises used: Interval.coe_coe, NonemptyInterval.coe_def
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ (↑⊥ : Set α) = Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)

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

Premises used: Set.Icc_eq_empty, mt, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
neg : s.toProd.1 ⊔ t.toProd.1 ≤ s.toProd.2 ⊓ t.toProd.2 → s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ (↑⊥ : Set α) = Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)

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

Premises used: Set.Icc_eq_empty, mt, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ s.toProd.1 ⊔ t.toProd.1 ≤ s.toProd.2 ⊓ t.toProd.2 → s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2

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

Premises used: le_sup_left, inf_le_right, le_sup_right, And.intro, inf_le_left, LE.le.trans
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ s.toProd.1 ⊔ t.toProd.1 ≤ 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⟩
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
s t : Interval α
rw : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ (↑s : Set α) ∩ (↑t : Set α) ⊆ (↑⊥ : Set α)
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t

Tactic:
rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]

Premises used: Interval.coe_subset_coe, Interval.coe_inf, disjoint_iff_inf_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
s t : Interval α
⊢ (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ (↑s : Set α) ∩ (↑t : Set α) ⊆ (↑⊥ : Set α)

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
s t : Interval α
rw : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ Disjoint s t
rw₁ : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ s ⊓ t ≤ ⊥
rw₂ : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ (↑(s ⊓ t) : Set α) ⊆ (↑⊥ : Set α)
rw₃ rw₄ rw₅ : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ (↑s : Set α) ∩ (↑t : Set α) ⊆ (↑⊥ : Set α)
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t

Tactic:
classical
    rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
    rfl

Premises used: Interval.coe_subset_coe, Interval.coe_inf, disjoint_iff_inf_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := Interval α) (↑(pure a) : Interval α) (Interval.pure a)

Tactic:
rfl

Premises used: Interval.pure, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
s : NonemptyInterval α
a : α
rw : (↑s : Interval α) = Interval.pure a ↔ (↑s : Interval α) = (↑(pure a) : Interval α)
rw₁ rw₂ : (↑s : Interval α) = Interval.pure a ↔ (↑s : Interval α) = Interval.pure a
⊢ (↑s : Interval α) = Interval.pure a ↔ s = pure a

Tactic:
rw [← Interval.coe_inj, coe_pure_interval]

Premises used: Interval.coe_inj, NonemptyInterval.coe_pure_interval
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : BoundedOrder α
⊢ Eq.{u_1 + 1} (α := Interval α) (↑⊤ : Interval α) ⊤

Tactic:
rfl

Premises used: WithBot.some, Interval.coe, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : NonemptyInterval α
x : α
⊢ x ∈ (↑s : Interval α) ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Icc
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
s t : NonemptyInterval α
⊢ (↑(s ⊔ t) : Interval α) = (↑s : Interval α) ⊔ (↑t : Interval α)

Tactic:
rfl

Premises used: WithBot.some, Interval.coe, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ¬S ⊆ {⊥}
obtain :
  ∀ (s : Interval α) (hs : s ∈ S) (ha : s ∉ {⊥}),
    LE.le.{u_1} (α := α)
      (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
          ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).1
      (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
          ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).2
⊢ LE.le.{u_1} (α := α)
    (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
        ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).1
    (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
        ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).2

Tactic:
obtain ⟨s, hs, ha⟩ := not_subset.1 h

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ¬S ⊆ {⊥}
s : Interval α
hs : s ∈ S
ha : s ∉ {⊥}
⊢ s ≠ ⊥

Tactic:
ha

Premises used: Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ¬S ⊆ {⊥}
s : Interval α
hs : s ∈ S
ha : s ∉ {⊥}
lift :
  ∀ (s : NonemptyInterval α) (hs : (↑s : Interval α) ∈ S),
    LE.le.{u_1} (α := α)
      (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
          ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).1
      (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
          ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).2
⊢ LE.le.{u_1} (α := α)
    (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
        ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).1
    (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
        ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).2

Tactic:
lift s to NonemptyInterval α using ha

Premises used: NonemptyInterval
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ¬S ⊆ {⊥}
s : NonemptyInterval α
hs : (↑s : Interval α) ∈ S
⊢ LE.le.{u_1} (α := α)
    (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
        ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).1
    (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
        ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).2

Tactic:
iInf₂_le_of_le s hs (le_iSup₂_of_le s hs s.fst_le_snd)

Premises used: iInf, iInf₂_le_of_le, le_iSup₂_of_le, NonemptyInterval.fst_le_snd
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ¬S ⊆ {⊥}
s : NonemptyInterval α
hs : (↑s : Interval α) ∈ S
⊢ LE.le.{u_1} (α := α)
    (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
        ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).1
    (⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
        ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.2).2

Tactic:
exact iInf₂_le_of_le s hs (le_iSup₂_of_le s hs s.fst_le_snd)

Premises used: iInf₂_le_of_le, le_iSup₂_of_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
left :
  (if h : x ⊆ {⊥} then ⊥
    else
      (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)) ∈
    upperBounds x
right :
  (if h : x ⊆ {⊥} then ⊥
    else
      (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)) ∈
    lowerBounds (upperBounds x)
⊢ IsLUB x
    (if h : x ⊆ {⊥} then ⊥
    else
      (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α))

Tactic:
constructor
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
s : Interval α
ha : s ∈ x
pos : ∀ (h : x ⊆ {⊥}), s ≤ ⊥
neg :
  ∀ (h : ¬x ⊆ {⊥}),
    s ≤
      (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
⊢ s ≤
    if h : x ⊆ {⊥} then ⊥
    else
      (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
s : Interval α
ha : s ∈ x
h : x ⊆ {⊥}
⊢ s ≤ ⊥

Tactic:
(h ha).le

Premises used: Eq.le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
s : Interval α
ha : s ∈ x
h : x ⊆ {⊥}
⊢ s ≤ ⊥

Tactic:
exact (h ha).le

Premises used: Eq.le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
s : Interval α
ha : s ∈ x
h : ¬x ⊆ {⊥}
neg :
  ∀ (ha : ⊥ ∈ x),
    ⊥ ≤
      (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
            NonemptyInterval α } :
        Interval α)
neg₁ :
  ∀ (a : NonemptyInterval α) (ha : (↑a : Interval α) ∈ x),
    (↑a : Interval α) ≤
      (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
⊢ s ≤
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α)

Tactic:
cases s
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
ha : ⊥ ∈ x
⊢ ⊥ ≤
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α } :
      Interval α)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
ha : ⊥ ∈ x
⊢ ⊥ ≤
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α } :
      Interval α)

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
a : NonemptyInterval α
ha : (↑a : Interval α) ∈ x
neg :
  a ≤
    { fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
      snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ }
⊢ (↑a : Interval α) ≤
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α)

Tactic:
apply Interval.coe_le_coe.2

Premises used: Iff.mpr, Interval.coe_le_coe
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
a : NonemptyInterval α
ha : (↑a : Interval α) ∈ x
neg :
  { fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α }.toProd.1 ≤
    a.toProd.1
neg₁ :
  a.toProd.2 ≤
    { fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α }.toProd.2
⊢ a ≤
    { fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
      snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ }

Tactic:
constructor
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
a : NonemptyInterval α
ha neg : (↑a : Interval α) ∈ x
⊢ { fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α }.toProd.1 ≤
    a.toProd.1

Tactic:
apply iInf₂_le

Premises used: iInf₂_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
a : NonemptyInterval α
ha : (↑a : Interval α) ∈ x
⊢ (↑a : Interval α) ∈ x

Tactic:
ha
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
a : NonemptyInterval α
ha : (↑a : Interval α) ∈ x
⊢ (↑a : Interval α) ∈ x

Tactic:
exact ha