awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
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
⊢ (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 neg : ∀
  (h :
    ¬(⊥ ∉ s₁ ∧
        ∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2)),
  ⊥ ≤ 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 α
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
⊢ (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ s₁), s.toProd.1,
          snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } :
      Interval α) ≤
    s
have 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 := sorry } :
      Interval α) ≤
    (↑s : Interval α)
Tactic: lift s to NonemptyInterval α using ne_of_mem_of_not_mem ha h.1
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 α)
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 ⊥
have 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 := 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 α
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 α)
⊢ (↑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 ⊥
have neg : ∀
  (h :
    ¬(⊥ ∉ s₁ ∧
        ∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2)),
  (↑s : Interval α) ≤ ⊥
Tactic: split_ifs with h
-- 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 : 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 α) ≤ ⊥
have h₁ : ⊥ ∈ 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
Cleared hypotheses: 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 α)
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 α) ≤ ⊥
have neg : ∀ (h : ⊥ ∈ s₁), (↑s : Interval α) ≤ ⊥
Tactic: rcases h with h | h
Cleared hypotheses: 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 α)
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 α) ≤ ⊥
⊢ (↑s : Interval α) ≤ ⊥
have neg₁ : ∀
  (h :
    ¬∀ ⦃s : NonemptyInterval α⦄,
        (↑s : Interval α) ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ s₁ → s.toProd.1 ≤ t.toProd.2),
  (↑s : Interval α) ≤ ⊥
Tactic: rcases h with h | h
Cleared hypotheses: 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 α)
s : Interval α
ha : s ∈ lowerBounds 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 ⊥
have 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 := sorry } :
        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)
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 α)
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 ⊥)
⊢ 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₁ : ∀ (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 := sorry } :
        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)
Cleared hypotheses: s, ha
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (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 := ⋯ :
                NonemptyInterval α } :
            Interval α)
        else ⊥) :
      Set α) =
    ⋂ s ∈ S, (↑s : Set α)
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 :
              NonemptyInterval α } :
          Interval α) :
      Set α) =
    ⋂ s ∈ S, (↑s : Set α)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
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 α)
⊢ (↑(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 α)
have neg : ∀
  (h :
    ¬(⊥ ∉ S ∧
        ∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2)),
  (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
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
⊢ (↑(↑{ 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 α)
have pos : ∀ (x : α),
  x ∈
      (↑(↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
                snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.2, fst_le_snd := sorry :
                NonemptyInterval α } :
            Interval α) :
        Set α) ↔
    Membership.mem (γ := Set α) (⋂ s ∈ S, (↑s : Set α)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (hypothesis)
Goal:
α : Type u_1
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)
⊢ (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
have h₁ : ⊥ ∈ S ∨
  ¬∀ ⦃s : NonemptyInterval α⦄,
      (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2
Tactic: simp_rw [not_and_or, Classical.not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
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
⊢ (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
have neg : ∀ (h : ⊥ ∈ S), (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
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
neg : ∀ (h : ⊥ ∈ S), (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
⊢ (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
have neg₁ : ∀
  (h :
    ¬∀ ⦃s : NonemptyInterval α⦄,
        (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
  (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ⊥ ∈ S
⊢ (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
have neg : Subset.{u_1} (α := Set α) (⋂ s ∈ S, (↑s : Set α)) ∅
Tactic: refine (eq_empty_of_subset_empty ?_).symm
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h :
  ¬∀ ⦃s : NonemptyInterval α⦄,
      (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
have neg : ¬Set.Nonempty.{u_1} (α := α) (⋂ s ∈ S, (↑s : Set α))
Tactic: refine (not_nonempty_iff_eq_empty.1 ?_).symm
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h :
  ¬∀ ⦃s : NonemptyInterval α⦄,
      (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2
x : α
hx : Membership.mem (γ := Set α) (⋂ s ∈ S, (↑s : Set α)) x
⊢ False
have hx₁ : ∀ (i : Interval α) (j : i ∈ S), x ∈ (↑i : Set α)
Tactic: rw [mem_iInter₂] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
⊢ (↑(sInf S) : Set α) = ⋂ s ∈ S, (↑s : Set α)
have change : (↑(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 :
              NonemptyInterval α } :
          Interval α)
      else ⊥) :
    Set α) =
  ⋂ s ∈ S, (↑s : Set α)
Tactic: classical
  change ((dite _ _ _ : Interval α) : Set α) = ⋂ (s : Interval α) (_ : s ∈ S), (s : Set α)
  split_ifs with h
  · ext
    simp [Interval.forall, h.1, ← forall_and, ← NonemptyInterval.mem_def]
  simp_rw [not_and_or, Classical.not_not] at h
  rcases h with h | h
  · refine (eq_empty_of_subset_empty ?_).symm
    exact iInter₂_subset_of_subset _ h Subset.rfl
  · refine (not_nonempty_iff_eq_empty.1 ?_).symm
    rintro ⟨x, hx⟩
    rw [mem_iInter₂] at hx
    exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
change :
  (↑(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 α)
⊢ (↑(sInf S) : Set α) = ⋂ s ∈ S, (↑s : Set α)
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 :
              NonemptyInterval α } :
          Interval α) :
      Set α) =
    ⋂ s ∈ S, (↑s : Set α)
Tactic: classical
  change ((dite _ _ _ : Interval α) : Set α) = ⋂ (s : Interval α) (_ : s ∈ S), (s : Set α)
  split_ifs with h
  · ext
    simp [Interval.forall, h.1, ← forall_and, ← NonemptyInterval.mem_def]
  simp_rw [not_and_or, Classical.not_not] at h
  rcases h with h | h
  · refine (eq_empty_of_subset_empty ?_).symm
    exact iInter₂_subset_of_subset _ h Subset.rfl
  · refine (not_nonempty_iff_eq_empty.1 ?_).symm
    rintro ⟨x, hx⟩
    rw [mem_iInter₂] at hx
    exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
change :
  (↑(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 α)
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 α)
⊢ (↑(sInf S) : Set α) = ⋂ s ∈ S, (↑s : Set α)
have neg : ∀
  (h :
    ¬(⊥ ∉ S ∧
        ∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2)),
  (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
Tactic: classical
  change ((dite _ _ _ : Interval α) : Set α) = ⋂ (s : Interval α) (_ : s ∈ S), (s : Set α)
  split_ifs with h
  · ext
    simp [Interval.forall, h.1, ← forall_and, ← NonemptyInterval.mem_def]
  simp_rw [not_and_or, Classical.not_not] at h
  rcases h with h | h
  · refine (eq_empty_of_subset_empty ?_).symm
    exact iInter₂_subset_of_subset _ h Subset.rfl
  · refine (not_nonempty_iff_eq_empty.1 ?_).symm
    rintro ⟨x, hx⟩
    rw [mem_iInter₂] at hx
    exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
change :
  (↑(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 α)
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 neg₁ :
  ∀
    (h :
      ¬(⊥ ∉ S ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2)),
    (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
⊢ (↑(sInf S) : Set α) = ⋂ s ∈ S, (↑s : Set α)
have neg₂ : ∀
  (h :
    ⊥ ∈ S ∨
      ¬∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
  (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
Tactic: classical
  change ((dite _ _ _ : Interval α) : Set α) = ⋂ (s : Interval α) (_ : s ∈ S), (s : Set α)
  split_ifs with h
  · ext
    simp [Interval.forall, h.1, ← forall_and, ← NonemptyInterval.mem_def]
  simp_rw [not_and_or, Classical.not_not] at h
  rcases h with h | h
  · refine (eq_empty_of_subset_empty ?_).symm
    exact iInter₂_subset_of_subset _ h Subset.rfl
  · refine (not_nonempty_iff_eq_empty.1 ?_).symm
    rintro ⟨x, hx⟩
    rw [mem_iInter₂] at hx
    exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2