awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (hypothesis)
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
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
have hb₂ : s.toProd.2 ≤ t.toProd.2
Tactic: rcases hb with ⟨hb₁, hb₂⟩
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (hypothesis)
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
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
have hc₁ : c.toProd.1 ≤ s.toProd.1
Tactic: rcases hc with ⟨hc₁, hc₂⟩
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (hypothesis)
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
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
have hc₂ : s.toProd.2 ≤ c.toProd.2
Tactic: rcases hc with ⟨hc₁, hc₂⟩
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
⊢ (↑((↑s : Interval α) ⊓ (↑t : Interval α)) : Set α) = (↑(↑s : Interval α) : Set α) ∩ (↑(↑t : Interval α) : Set α)
have 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 := sorry : NonemptyInterval α } :
          Interval α)
      else ⊥) :
    Set α) =
  Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)
Tactic: simp only [coe_coe, NonemptyInterval.coe_def, Icc_inter_Icc, inf_coe]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : DecidableLE α
s t : NonemptyInterval α
⊢ (↑(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)
have 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 := sorry : NonemptyInterval α } :
          Interval α) :
      Set α) =
    Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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)
⊢ (↑(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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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)
have 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
Tactic: refine (Icc_eq_empty <| mt ?_ h).symm
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : Lattice α
s t : Interval α
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t
have rw : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ (↑s : Set α) ∩ (↑t : Set α) ⊆ (↑⊥ : Set α)
Tactic: rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : Lattice α
s t : Interval α
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t
have rw : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ Disjoint s t
Tactic: classical
    rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : Lattice α
s t : Interval α
rw : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ Disjoint s t
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t
have rw₁ : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ s ⊓ t ≤ ⊥
Tactic: classical
    rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : Lattice α
s t : Interval α
rw : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ Disjoint s t
rw₁ : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ s ⊓ t ≤ ⊥
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t
have rw₂ : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ (↑(s ⊓ t) : Set α) ⊆ (↑⊥ : Set α)
Tactic: classical
    rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 α)
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t
have rw₃ : (↑s : Set α) ⊓ (↑t : Set α) ≤ ⊥ ↔ (↑s : Set α) ∩ (↑t : Set α) ⊆ (↑⊥ : Set α)
Tactic: classical
    rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s : NonemptyInterval α
a : α
⊢ (↑s : Interval α) = Interval.pure a ↔ s = pure a
have rw : (↑s : Interval α) = Interval.pure a ↔ (↑s : Interval α) = (↑(pure a) : Interval α)
Tactic: rw [← Interval.coe_inj, coe_pure_interval]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s : NonemptyInterval α
a : α
rw : (↑s : Interval α) = Interval.pure a ↔ (↑s : Interval α) = (↑(pure a) : Interval α)
⊢ (↑s : Interval α) = Interval.pure a ↔ s = pure a
have rw₁ : (↑s : Interval α) = Interval.pure a ↔ (↑s : Interval α) = Interval.pure a
Tactic: rw [← Interval.coe_inj, coe_pure_interval]
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 ⊆ {⊥}
⊢ 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
have 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
Tactic: obtain ⟨s, hs, ha⟩ := not_subset.1 h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 ∉ {⊥}
⊢ 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
have 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
Tactic: lift s to NonemptyInterval α using ha
Cleared hypotheses: s, hs, ha
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
x : Set (Interval α)
⊢ 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 α))
have 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 := sorry } :
      Interval α)) ∈
  upperBounds x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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
⊢ 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 α))
have 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 := sorry } :
      Interval α)) ∈
  lowerBounds (upperBounds x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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
⊢ 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 α)
have pos : ∀ (h : x ⊆ {⊥}), s ≤ ⊥
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 ≤ ⊥
⊢ 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 α)
have 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 := sorry } :
      Interval α)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 ≤
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α)
have neg : ∀ (ha : ⊥ ∈ x),
  ⊥ ≤
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := sorry :
          NonemptyInterval α } :
      Interval α)
Tactic: cases s
Cleared hypotheses: s, ha
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 α)
⊢ s ≤
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α)
have 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 := sorry } :
      Interval α)
Tactic: cases s
Cleared hypotheses: s, ha
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 α) ≤
    (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α)
have neg : a ≤
  { fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
    snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := sorry }
Tactic: apply Interval.coe_le_coe.2
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 ≤
    { fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
      snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ }
have neg : { fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
        snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := sorry :
        NonemptyInterval α }.toProd.1 ≤
  a.toProd.1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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
⊢ a ≤
    { fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
      snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ }
have 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 := sorry :
        NonemptyInterval α }.toProd.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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
⊢ (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
have pos : ∀ (h : x ⊆ {⊥}), ⊥ ≤ s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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
⊢ (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
have neg : ∀ (h : ¬x ⊆ {⊥}),
  (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := sorry :
          NonemptyInterval α } :
      Interval α) ≤
    s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 ⊆ {⊥}
⊢ (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α } :
      Interval α) ≤
    s
have 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 := sorry :
          NonemptyInterval α } :
      Interval α) ≤
    s
Tactic: obtain ⟨b, hs, hb⟩ := not_subset.1 h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 ∉ {⊥}
⊢ (↑{ fst := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ x), s.toProd.1,
          snd := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ x), s.toProd.2, fst_le_snd := ⋯ :
          NonemptyInterval α } :
      Interval α) ≤
    s
have 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 := sorry :
          NonemptyInterval α } :
      Interval α) ≤
    (↑s : Interval α)
Tactic: lift s to NonemptyInterval α using ne_bot_of_le_ne_bot hb (ha hs)
Cleared hypotheses: s, ha
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
s₁ : Set (Interval α)
⊢ 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 ⊥)
have 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 := sorry } :
      Interval α)
  else ⊥) ∈
  lowerBounds s₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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₁
⊢ 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 ⊥)
have 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 := sorry } :
      Interval α)
  else ⊥) ∈
  upperBounds (lowerBounds s₁)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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₁
⊢ (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
have 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 := sorry } :
      Interval α) ≤
    s
Tactic: split_ifs with h