-- Mathlib/Order/Interval/Basic.lean
theorem coe_sInf [DecidableRel (α := α) (· ≤ ·)] (S : Set (Interval α)) :
    ↑(sInf S) = ⋂ s ∈ S, (s : Set α)

Proof state:
case neg.inr.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x : α
hx : ∀ i ∈ S, x ∈ ↑i
⊢ False

Tactic:
exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∈ S ∨ ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
rcases h with h | h

Result:
case neg.inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∈ S
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Proof state:
case pos
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑↑{ toProd := (⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2), fst_le_snd := ⋯ } = ⋂ s ∈ S, ↑s

Tactic:
ext

Result:
case pos.h
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x✝ : α
⊢ x✝ ∈ ↑↑{ toProd := (⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2), fst_le_snd := ⋯ } ↔
    x✝ ∈ ⋂ s ∈ S, ↑s

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
⊢ ↑(sInf S) = ⋂ s ∈ S, ↑s

Tactic:
change ((dite _ _ _ : Interval α) : Set α) = ⋂ (s : Interval α) (_ : s ∈ S), (s : Set α)

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
⊢ ↑(if h :
          ⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2 then
        ↑{ toProd := (⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2), fst_le_snd := ⋯ }
      else ⊥) =
    ⋂ s ∈ S, ↑s

Proof state:
case neg
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬(⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2)
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
simp_rw [not_and_or, Classical.not_not] at h

Result:
case neg
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∈ S ∨ ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Proof state:
case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ¬(⋂ s ∈ S, ↑s).Nonempty

Tactic:
rintro ⟨x, hx⟩

Result:
case neg.inr.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x : α
hx : x ∈ ⋂ s ∈ S, ↑s
⊢ False

Proof state:
case neg.inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∈ S
⊢ ⋂ s ∈ S, ↑s ⊆ ∅

Tactic:
exact iInter₂_subset_of_subset _ h Subset.rfl

Result:
no goals

Proof state:
case pos.h
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x✝ : α
⊢ x✝ ∈ ↑↑{ toProd := (⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2), fst_le_snd := ⋯ } ↔
    x✝ ∈ ⋂ s ∈ S, ↑s

Tactic:
simp [Interval.forall, h.1, ← forall_and, ← NonemptyInterval.mem_def]

Result:
no goals

Proof state:
case neg.inr.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x : α
hx : x ∈ ⋂ s ∈ S, ↑s
⊢ False

Tactic:
rw [mem_iInter₂] at hx

Result:
case neg.inr.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x : α
hx : ∀ i ∈ S, x ∈ ↑i
⊢ False

Proof state:
case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
refine (not_nonempty_iff_eq_empty.1 ?_).symm

Result:
case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ¬(⋂ s ∈ S, ↑s).Nonempty

Proof state:
case neg.inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∈ S
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
refine (eq_empty_of_subset_empty ?_).symm

Result:
case neg.inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∈ S
⊢ ⋂ s ∈ S, ↑s ⊆ ∅

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
⊢ ↑(if h :
          ⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2 then
        ↑{ toProd := (⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2), fst_le_snd := ⋯ }
      else ⊥) =
    ⋂ s ∈ S, ↑s

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑↑{ toProd := (⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2), fst_le_snd := ⋯ } = ⋂ s ∈ S, ↑s

case neg
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
S : Set (Interval α)
h : ¬(⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2)
⊢ ↑⊥ = ⋂ s ∈ S, ↑s