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 : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
a : NonemptyInterval α
ha : (↑a : Interval α) ∈ x
⊢ 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

Tactic:
le_iSup₂_of_le _ ha le_rfl

Premises used: le_rfl, iSup, 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 α)
h : ¬x ⊆ {⊥}
a : NonemptyInterval α
ha : (↑a : Interval α) ∈ x
⊢ 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

Tactic:
exact le_iSup₂_of_le _ ha le_rfl

Premises used: le_rfl, 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 α)
s : Interval α
ha : s ∈ upperBounds x
pos : ∀ (h : x ⊆ {⊥}), ⊥ ≤ s
neg :
  ∀ (h : ¬x ⊆ {⊥}),
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
            NonemptyInterval α } :
        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 α)) ≤
    s

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 ∈ upperBounds x
h : x ⊆ {⊥}
⊢ ⊥ ≤ s

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 α)
s : Interval α
ha : s ∈ upperBounds x
h : x ⊆ {⊥}
⊢ ⊥ ≤ s

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 α)
s : Interval α
ha : s ∈ upperBounds x
h : ¬x ⊆ {⊥}
neg :
  ∀ (b : Interval α) (hs : b ∈ x) (hb : b ∉ {⊥}),
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
            NonemptyInterval α } :
        Interval α) ≤
      s
⊢ (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α } :
      Interval α) ≤
    s

Tactic:
obtain ⟨b, hs, hb⟩ := 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 α
x : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x
h : ¬x ⊆ {⊥}
b : Interval α
hs : b ∈ x
hb : b ∉ {⊥}
⊢ s ≠ ⊥

Tactic:
ne_bot_of_le_ne_bot hb (ha hs)

Premises used: ne_bot_of_le_ne_bot
-- 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 ∈ upperBounds x
h : ¬x ⊆ {⊥}
b : Interval α
hs : b ∈ x
hb : b ∉ {⊥}
neg :
  ∀ (s : NonemptyInterval α) (ha : (↑s : Interval α) ∈ upperBounds x),
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
            snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
            NonemptyInterval α } :
        Interval α) ≤
      (↑s : Interval α)
⊢ (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α } :
      Interval α) ≤
    s

Tactic:
lift s to NonemptyInterval α using ne_bot_of_le_ne_bot hb (ha hs)

Premises used: ne_bot_of_le_ne_bot, 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 α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
b : Interval α
hs : b ∈ x
hb : b ∉ {⊥}
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ upperBounds x
⊢ (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α } :
      Interval α) ≤
    (↑s : Interval α)

Tactic:
Interval.coe_le_coe.2
          ⟨le_iInf₂ fun c hc => (WithBot.coe_le_coe.1 <| ha hc).1,
            iSup₂_le fun c hc => (WithBot.coe_le_coe.1 <| ha hc).2⟩

Premises used: Iff.mpr, iSup₂_le, Interval.coe_le_coe, WithBot.coe_le_coe, le_iInf₂, And.right, And.left, And.intro, 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 α
x : Set (Interval α)
h : ¬x ⊆ {⊥}
b : Interval α
hs : b ∈ x
hb : b ∉ {⊥}
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ upperBounds x
⊢ (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α } :
      Interval α) ≤
    (↑s : Interval α)

Tactic:
exact
        Interval.coe_le_coe.2
          ⟨le_iInf₂ fun c hc => (WithBot.coe_le_coe.1 <| ha hc).1,
            iSup₂_le fun c hc => (WithBot.coe_le_coe.1 <| ha hc).2⟩

Premises used: Iff.mpr, Interval.coe_le_coe, And.intro
-- 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 α)
left :
  (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
    else ⊥) ∈
    lowerBounds s₁
right :
  (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
    else ⊥) ∈
    upperBounds (lowerBounds s₁)
⊢ IsGLB s₁
    (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
    else ⊥)

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 α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
pos :
  ∀
    (h :
      ⊥ ∉ s₁ ∧
        ∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2),
    (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α) ≤
      s
neg :
  ∀
    (h :
      ¬(⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2)),
    ⊥ ≤ s
⊢ (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
    else ⊥) ≤
    s

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 α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h :
  ⊥ ∉ s₁ ∧
    ∀ ⦃s : NonemptyInterval α⦄,
      (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2
⊢ s ≠ ⊥

Tactic:
ne_of_mem_of_not_mem ha h.1

Premises used: ne_of_mem_of_not_mem, And.left
-- 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 α)
s : Interval α
ha : s ∈ s₁
h :
  ⊥ ∉ s₁ ∧
    ∀ ⦃s : NonemptyInterval α⦄,
      (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2
pos :
  ∀ (s : NonemptyInterval α) (ha : (↑s : Interval α) ∈ s₁),
    (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α) ≤
      (↑s : Interval α)
⊢ (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
          snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α) ≤
    s

Tactic:
lift s to NonemptyInterval α using ne_of_mem_of_not_mem ha h.1

Premises used: ne_of_mem_of_not_mem, And.left, 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 α⦄,
      (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ s₁
f : (s : NonemptyInterval α) → (↑s : Interval α) ∈ s₁ → α :=
  fun (s : NonemptyInterval α) (x : (↑s : Interval α) ∈ s₁) ↦ s.toProd.1
⊢ (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
          snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α) ≤
    (↑s : Interval α)

Tactic:
WithBot.coe_le_coe.2 ⟨le_iSup₂ (f := f) s ha, iInf₂_le s ha⟩

Premises used: Iff.mpr, le_iSup₂, iInf₂_le, WithBot.coe_le_coe, Interval.coe, And.intro
-- 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 α⦄,
      (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ s₁
f : (s : NonemptyInterval α) → (↑s : Interval α) ∈ s₁ → α :=
  fun (s : NonemptyInterval α) (x : (↑s : Interval α) ∈ s₁) ↦ s.toProd.1
⊢ (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
          snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α) ≤
    (↑s : Interval α)

Tactic:
exact WithBot.coe_le_coe.2 ⟨le_iSup₂ (f := f) s ha, iInf₂_le s 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 α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h :
  ¬(⊥ ∉ s₁ ∧
      ∀ ⦃s : NonemptyInterval α⦄,
        (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ⊥ ≤ s

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 α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h :
  ¬(⊥ ∉ s₁ ∧
      ∀ ⦃s : NonemptyInterval α⦄,
        (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ⊥ ≤ s

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 α
s₁ : Set (Interval α)
ha : ⊥ ∈ lowerBounds s₁
⊢ LE.le.{u_1} (α := Interval α) ⊥
    (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
    else ⊥)

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 α
s₁ : Set (Interval α)
ha : ⊥ ∈ lowerBounds s₁
⊢ LE.le.{u_1} (α := Interval α) ⊥
    (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
    else ⊥)

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 α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ lowerBounds s₁
pos :
  ∀
    (h :
      ⊥ ∉ s₁ ∧
        ∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2),
    (↑s : Interval α) ≤
      (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
neg :
  ∀
    (h :
      ¬(⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2)),
    (↑s : Interval α) ≤ ⊥
⊢ (↑s : Interval α) ≤
    if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
    else ⊥

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 α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ lowerBounds s₁
h :
  ⊥ ∉ s₁ ∧
    ∀ ⦃s : NonemptyInterval α⦄,
      (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2
⊢ (↑s : Interval α) ≤
    (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
          snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α)

Tactic:
WithBot.coe_le_coe.2
            ⟨iSup₂_le fun t hb => (WithBot.coe_le_coe.1 <| ha hb).1,
              le_iInf₂ fun t hb => (WithBot.coe_le_coe.1 <| ha hb).2⟩

Premises used: Iff.mpr, iSup₂_le, WithBot.coe_le_coe, le_iInf₂, Interval.coe, And.right, And.left, And.intro, 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 α)
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ lowerBounds s₁
h :
  ⊥ ∉ s₁ ∧
    ∀ ⦃s : NonemptyInterval α⦄,
      (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2
⊢ (↑s : Interval α) ≤
    (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
          snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α)

Tactic:
exact WithBot.coe_le_coe.2
            ⟨iSup₂_le fun t hb => (WithBot.coe_le_coe.1 <| ha hb).1,
              le_iInf₂ fun t hb => (WithBot.coe_le_coe.1 <| ha hb).2⟩
-- 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 α)
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ lowerBounds s₁
h :
  ¬(⊥ ∉ s₁ ∧
      ∀ ⦃s : NonemptyInterval α⦄,
        (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ⊥ ∈ s₁ ∨
    ¬∀ ⦃s : NonemptyInterval α⦄,
        (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2

Tactic:
rw [not_and_or, not_not] at h

Premises used: Classical.not_not, not_and_or
-- 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 α)
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ lowerBounds s₁
h :
  ⊥ ∈ s₁ ∨
    ¬∀ ⦃s : NonemptyInterval α⦄,
        (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2
neg : ∀ (h : ⊥ ∈ s₁), (↑s : Interval α) ≤ ⊥
neg₁ :
  ∀
    (h :
      ¬∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2),
    (↑s : Interval α) ≤ ⊥
⊢ (↑s : Interval α) ≤ ⊥

Tactic:
rcases h with h | 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 α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ lowerBounds s₁
h : ⊥ ∈ s₁
⊢ (↑s : Interval α) ≤ ⊥

Tactic:
ha 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 α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ lowerBounds s₁
h : ⊥ ∈ s₁
⊢ (↑s : Interval α) ≤ ⊥

Tactic:
exact ha 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 α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : (↑s : Interval α) ∈ lowerBounds s₁
h :
  ¬∀ ⦃s : NonemptyInterval α⦄,
      (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2
⊢ (↑s : Interval α) ≤ ⊥

Tactic:
cases h fun b hb c hc ↦ (WithBot.coe_le_coe.1 <| ha hb).1.trans
              (s.fst_le_snd.trans (WithBot.coe_le_coe.1 <| ha hc).2)

Premises used: WithBot.coe_le_coe, And.right, And.left, Iff.mp, 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 : CompleteLattice α
inst_1 : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ lowerBounds s₁
right :
  ∀ (ha : ⊥ ∈ lowerBounds s₁),
    LE.le.{u_1} (α := Interval α) ⊥
      (if h :
          ⊥ ∉ s₁ ∧
            ∀ ⦃s : NonemptyInterval α⦄,
              (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
        (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
              snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
          Interval α)
      else ⊥)
right₁ :
  ∀ (s : NonemptyInterval α) (ha : (↑s : Interval α) ∈ lowerBounds s₁),
    (↑s : Interval α) ≤
      if h :
          ⊥ ∉ s₁ ∧
            ∀ ⦃s : NonemptyInterval α⦄,
              (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
        (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
              snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
          Interval α)
      else ⊥
⊢ s ≤
    if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
            snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
        Interval α)
    else ⊥

Tactic:
cases s with
      | bot => exact bot_le
      | coe s =>
        split_ifs with h
        · exact WithBot.coe_le_coe.2
            ⟨iSup₂_le fun t hb => (WithBot.coe_le_coe.1 <| ha hb).1,
              le_iInf₂ fun t hb => (WithBot.coe_le_coe.1 <| ha hb).2⟩
        · rw [not_and_or, not_not] at h
          rcases h with h | h
          · exact ha h
          · cases h fun b hb c hc ↦ (WithBot.coe_le_coe.1 <| ha hb).1.trans
              (s.fst_le_snd.trans (WithBot.coe_le_coe.1 <| ha hc).2)

Premises used: Classical.not_not, Interval.coe, not_and_or, bot_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
pos :
  ∀
    (h :
      ⊥ ∉ S ∧
        ∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
    (↑(↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
                snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.2, fst_le_snd := ⋯ :
                NonemptyInterval α } :
            Interval α) :
        Set α) =
      ⋂ s ∈ S, (↑s : Set α)
neg :
  ∀
    (h :
      ¬(⊥ ∉ S ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2)),
    (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
⊢ (↑(if h :
            ⊥ ∉ S ∧
              ∀ ⦃s : NonemptyInterval α⦄,
                (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2 then
          (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
                snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.2, fst_le_snd := ⋯ :
                NonemptyInterval α } :
            Interval α)
        else ⊥) :
      Set α) =
    ⋂ s ∈ S, (↑s : Set α)

Tactic:
split_ifs with h