awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Basic
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
pos :
  ∀ (x : α),
    x ∈
        (↑(↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
                  snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.2, fst_le_snd := ⋯ :
                  NonemptyInterval α } :
              Interval α) :
          Set α) ↔
      Membership.mem (γ := Set α) (⋂ s ∈ S, (↑s : Set α)) x
⊢ (↑(↑{ 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 α)

Tactic:
ext
-- Module: Mathlib.Order.Interval.Basic
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
x : α
⊢ x ∈
      (↑(↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
                snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.2, fst_le_snd := ⋯ :
                NonemptyInterval α } :
            Interval α) :
        Set α) ↔
    Membership.mem (γ := Set α) (⋂ s ∈ S, (↑s : Set α)) x

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

Premises used: Interval.forall, And.left, NonemptyInterval.mem_def, forall_and
-- Module: Mathlib.Order.Interval.Basic
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)
⊢ ⊥ ∈ 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

Premises used: Classical.not_not, not_and_or
-- Module: Mathlib.Order.Interval.Basic
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 α)
neg₁ :
  ∀
    (h :
      ¬∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
    (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
⊢ (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)

Tactic:
rcases h with h | h
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ⊥ ∈ S
⊢ (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)

Tactic:
(eq_empty_of_subset_empty ?_).symm

Premises used: Set.eq_empty_of_subset_empty, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ⊥ ∈ S
neg : Subset.{u_1} (α := Set α) (⋂ s ∈ S, (↑s : Set α)) ∅
⊢ (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)

Tactic:
refine (eq_empty_of_subset_empty ?_).symm

Premises used: Set.eq_empty_of_subset_empty, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ⊥ ∈ S
⊢ Subset.{u_1} (α := Set α) (⋂ s ∈ S, (↑s : Set α)) ∅

Tactic:
iInter₂_subset_of_subset _ h Subset.rfl

Premises used: Set.iInter₂_subset_of_subset, Set.Subset.rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
h : ⊥ ∈ S
⊢ Subset.{u_1} (α := Set α) (⋂ s ∈ S, (↑s : Set α)) ∅

Tactic:
exact iInter₂_subset_of_subset _ h Subset.rfl

Premises used: Set.iInter₂_subset_of_subset, Set.Subset.rfl
-- Module: Mathlib.Order.Interval.Basic
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 α)

Tactic:
(not_nonempty_iff_eq_empty.1 ?_).symm

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
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
neg : ¬Set.Nonempty.{u_1} (α := α) (⋂ s ∈ S, (↑s : Set α))
⊢ (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)

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

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp, Eq.symm
-- Module: Mathlib.Order.Interval.Basic
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
⊢ ∀ (i : Interval α) (j : i ∈ S), x ∈ (↑i : Set α)

Tactic:
rw [mem_iInter₂] at hx

Premises used: Set.mem_iInter₂
-- Module: Mathlib.Order.Interval.Basic
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 : ∀ (i : Interval α) (j : i ∈ S), x ∈ (↑i : Set α)
⊢ False

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

Premises used: Interval.coe, And.right, And.left, LE.le.trans
-- Module: Mathlib.Order.Interval.Basic
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 : ∀ (i : Interval α) (j : i ∈ S), x ∈ (↑i : Set α)
⊢ False

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

Premises used: Interval.coe, And.right, And.left, LE.le.trans
-- Module: Mathlib.Order.Interval.Basic
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 α)
neg₂ :
  ∀
    (h :
      ⊥ ∈ S ∨
        ¬∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
    (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
neg₃ : ∀ (h : ⊥ ∈ S), (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
neg₄ neg₅ :
  ∀
    (h :
      ¬∀ ⦃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 α)

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

Premises used: Classical.not_not, Set.not_nonempty_iff_eq_empty, Set.mem_iInter₂, Interval, Set.eq_empty_of_subset_empty, dite, Interval.forall, SetLike.coe, not_and_or, NonemptyInterval.mem_def, Iff.mp, Eq.symm, forall_and
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
inst_1 : DecidableLE α
f : ι → Interval α
⊢ (↑(⨅ (i : ι), f i) : Set α) = ⋂ (i : ι), (↑(f i) : Set α)

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst : CompleteLattice α
inst_1 : DecidableLE α
f : (i : ι) → κ i → Interval α
⊢ (↑(⨅ (i : ι), ⨅ (j : κ i), f i j) : Set α) = ⋂ (i : ι), ⋂ (j : κ i), (↑(f i j) : Set α)

Tactic:
simp_rw [coe_iInf]

Premises used: Interval.coe_iInf
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Icc a b) : Set α).Nonempty ↔ a ≤ b
rw₁ : (Set.Icc a b).Nonempty ↔ a ≤ b
rw₂ rw₃ : a ≤ b ↔ a ≤ b
⊢ (Icc a b).Nonempty ↔ a ≤ b

Tactic:
rw [← coe_nonempty, coe_Icc, Set.nonempty_Icc]

Premises used: Finset.coe_nonempty, Finset.coe_Icc, Set.nonempty_Icc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ico a b) : Set α).Nonempty ↔ a < b
rw₁ : (Set.Ico a b).Nonempty ↔ a < b
rw₂ rw₃ : a < b ↔ a < b
⊢ (Ico a b).Nonempty ↔ a < b

Tactic:
rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]

Premises used: Finset.coe_Ico, Finset.coe_nonempty, Set.nonempty_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ioc a b) : Set α).Nonempty ↔ a < b
rw₁ : (Set.Ioc a b).Nonempty ↔ a < b
rw₂ rw₃ : a < b ↔ a < b
⊢ (Ioc a b).Nonempty ↔ a < b

Tactic:
rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]

Premises used: Set.nonempty_Ioc, Finset.coe_nonempty, Finset.coe_Ioc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
rw : (↑(Ioo a b) : Set α).Nonempty ↔ a < b
rw₁ : (Set.Ioo a b).Nonempty ↔ a < b
rw₂ rw₃ : a < b ↔ a < b
⊢ (Ioo a b).Nonempty ↔ a < b

Tactic:
rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]

Premises used: Finset.coe_nonempty, Set.nonempty_Ioo, Finset.coe_Ioo
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Icc a b) : Set α) = ∅ ↔ ¬a ≤ b
rw₁ : Set.Icc a b = ∅ ↔ ¬a ≤ b
rw₂ rw₃ : ¬a ≤ b ↔ ¬a ≤ b
⊢ Icc a b = ∅ ↔ ¬a ≤ b

Tactic:
rw [← coe_eq_empty, coe_Icc, Set.Icc_eq_empty_iff]

Premises used: Finset.coe_eq_empty, Set.Icc_eq_empty_iff, Finset.coe_Icc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ico a b) : Set α) = ∅ ↔ ¬a < b
rw₁ : Set.Ico a b = ∅ ↔ ¬a < b
rw₂ rw₃ : ¬a < b ↔ ¬a < b
⊢ Ico a b = ∅ ↔ ¬a < b

Tactic:
rw [← coe_eq_empty, coe_Ico, Set.Ico_eq_empty_iff]

Premises used: Finset.coe_Ico, Finset.coe_eq_empty, Set.Ico_eq_empty_iff
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ioc a b) : Set α) = ∅ ↔ ¬a < b
rw₁ : Set.Ioc a b = ∅ ↔ ¬a < b
rw₂ rw₃ : ¬a < b ↔ ¬a < b
⊢ Ioc a b = ∅ ↔ ¬a < b

Tactic:
rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]

Premises used: Finset.coe_eq_empty, Finset.coe_Ioc, Set.Ioc_eq_empty_iff
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
rw : (↑(Ioo a b) : Set α) = ∅ ↔ ¬a < b
rw₁ : Set.Ioo a b = ∅ ↔ ¬a < b
rw₂ rw₃ : ¬a < b ↔ ¬a < b
⊢ Ioo a b = ∅ ↔ ¬a < b

Tactic:
rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]

Premises used: Finset.coe_eq_empty, Finset.coe_Ioo, Set.Ioo_eq_empty_iff
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : ¬a < b
⊢ Ioo a b = ∅

Tactic:
eq_empty_iff_forall_notMem.2 fun _ hx => h ((mem_Ioo.1 hx).1.trans (mem_Ioo.1 hx).2)

Premises used: Iff.mpr, Finset.eq_empty_iff_forall_notMem, Finset.mem_Ioo, And.right, And.left, Iff.mp, LT.lt.trans
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b < a
⊢ Icc a b = ∅

Tactic:
Icc_eq_empty h.not_ge

Premises used: Finset.Icc_eq_empty, LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b ≤ a
⊢ Ico a b = ∅

Tactic:
Ico_eq_empty h.not_gt

Premises used: Finset.Ico_eq_empty, LE.le.not_gt
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b ≤ a
⊢ Ioc a b = ∅

Tactic:
Ioc_eq_empty h.not_gt

Premises used: Finset.Ioc_eq_empty, LE.le.not_gt
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b ≤ a
⊢ Ioo a b = ∅

Tactic:
Ioo_eq_empty h.not_gt

Premises used: LE.le.not_gt, Finset.Ioo_eq_empty
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ a ∈ Icc a b ↔ a ≤ b

Tactic:
simp only [mem_Icc, true_and, le_rfl]

Premises used: le_rfl, Finset.mem_Icc, true_and
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ a ∈ Ico a b ↔ a < b

Tactic:
simp only [mem_Ico, true_and, le_refl]

Premises used: le_refl, true_and, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ b ∈ Icc a b ↔ a ≤ b

Tactic:
simp only [mem_Icc, and_true, le_rfl]

Premises used: le_rfl, and_true, Finset.mem_Icc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ b ∈ Ioc a b ↔ a < b

Tactic:
simp only [mem_Ioc, and_true, le_rfl]

Premises used: le_rfl, and_true, Finset.mem_Ioc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ a ∉ Ioc a b

Tactic:
fun h => lt_irrefl _ (mem_Ioc.1 h).1

Premises used: lt_irrefl, And.left, Iff.mp, Finset.mem_Ioc, Not
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ a ∉ Ioo a b

Tactic:
fun h => lt_irrefl _ (mem_Ioo.1 h).1

Premises used: lt_irrefl, Finset.mem_Ioo, And.left, Iff.mp, Not
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ b ∉ Ico a b

Tactic:
fun h => lt_irrefl _ (mem_Ico.1 h).2

Premises used: lt_irrefl, And.right, Iff.mp, Not, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ b ∉ Ioo a b

Tactic:
fun h => lt_irrefl _ (mem_Ioo.1 h).2

Premises used: lt_irrefl, Finset.mem_Ioo, And.right, Iff.mp, Not
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂

Tactic:
simpa [← coe_subset] using Set.Icc_subset_Icc ha hb

Premises used: Set.Icc_subset_Icc, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂

Tactic:
simpa [← coe_subset] using Set.Ico_subset_Ico ha hb

Premises used: Set.Ico_subset_Ico, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂

Tactic:
simpa [← coe_subset] using Set.Ioc_subset_Ioc ha hb

Premises used: Set.Ioc_subset_Ioc, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ⊆ Ioo a₂ b₂

Tactic:
simpa [← coe_subset] using Set.Ioo_subset_Ioo ha hb

Premises used: Set.Ioo_subset_Ioo, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : a₁ ≤ a₂
⊢ Icc a₂ b ⊆ Icc a₁ b

Tactic:
Icc_subset_Icc h le_rfl

Premises used: le_rfl, Finset.Icc_subset_Icc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : a₁ ≤ a₂
⊢ Ico a₂ b ⊆ Ico a₁ b

Tactic:
Ico_subset_Ico h le_rfl

Premises used: le_rfl, Finset.Ico_subset_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : a₁ ≤ a₂
⊢ Ioc a₂ b ⊆ Ioc a₁ b

Tactic:
Ioc_subset_Ioc h le_rfl

Premises used: le_rfl, Finset.Ioc_subset_Ioc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : a₁ ≤ a₂
⊢ Ioo a₂ b ⊆ Ioo a₁ b

Tactic:
Ioo_subset_Ioo h le_rfl

Premises used: le_rfl, Finset.Ioo_subset_Ioo
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ ≤ b₂
⊢ Icc a b₁ ⊆ Icc a b₂

Tactic:
Icc_subset_Icc le_rfl h

Premises used: le_rfl, Finset.Icc_subset_Icc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ ≤ b₂
⊢ Ico a b₁ ⊆ Ico a b₂

Tactic:
Ico_subset_Ico le_rfl h

Premises used: le_rfl, Finset.Ico_subset_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ ≤ b₂
⊢ Ioc a b₁ ⊆ Ioc a b₂

Tactic:
Ioc_subset_Ioc le_rfl h

Premises used: le_rfl, Finset.Ioc_subset_Ioc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ ≤ b₂
⊢ Ioo a b₁ ⊆ Ioo a b₂

Tactic:
Ioo_subset_Ioo le_rfl h

Premises used: le_rfl, Finset.Ioo_subset_Ioo
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : a₁ < a₂
rw : Set.Ico a₂ b ⊆ Set.Ioo a₁ b
⊢ Ico a₂ b ⊆ Ioo a₁ b

Tactic:
rw [← coe_subset, coe_Ico, coe_Ioo]

Premises used: Finset.coe_Ico, Finset.coe_Ioo, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b

Tactic:
Set.Ico_subset_Ioo_left h

Premises used: Set.Ico_subset_Ioo_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a₁ a₂ b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b

Tactic:
exact Set.Ico_subset_Ioo_left h

Premises used: Set.Ico_subset_Ioo_left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ < b₂
rw : Set.Ioc a b₁ ⊆ Set.Ioo a b₂
⊢ Ioc a b₁ ⊆ Ioo a b₂

Tactic:
rw [← coe_subset, coe_Ioc, coe_Ioo]

Premises used: Finset.coe_Ioc, Finset.coe_Ioo, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Ioc a b₁ ⊆ Set.Ioo a b₂

Tactic:
Set.Ioc_subset_Ioo_right h

Premises used: Set.Ioc_subset_Ioo_right
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Ioc a b₁ ⊆ Set.Ioo a b₂

Tactic:
exact Set.Ioc_subset_Ioo_right h

Premises used: Set.Ioc_subset_Ioo_right
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ < b₂
rw : Set.Icc a b₁ ⊆ Set.Ico a b₂
⊢ Icc a b₁ ⊆ Ico a b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Ico]

Premises used: Finset.coe_Ico, Finset.coe_Icc, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ Set.Ico a b₂

Tactic:
Set.Icc_subset_Ico_right h

Premises used: Set.Icc_subset_Ico_right
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ Set.Ico a b₂

Tactic:
exact Set.Icc_subset_Ico_right h

Premises used: Set.Icc_subset_Ico_right
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : Set.Ioo a b ⊆ Set.Ico a b
⊢ Ioo a b ⊆ Ico a b

Tactic:
rw [← coe_subset, coe_Ioo, coe_Ico]

Premises used: Finset.coe_Ico, Finset.coe_Ioo, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ico a b

Tactic:
Set.Ioo_subset_Ico_self

Premises used: Set.Ioo_subset_Ico_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ico a b

Tactic:
exact Set.Ioo_subset_Ico_self

Premises used: Set.Ioo_subset_Ico_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : Set.Ioo a b ⊆ Set.Ioc a b
⊢ Ioo a b ⊆ Ioc a b

Tactic:
rw [← coe_subset, coe_Ioo, coe_Ioc]

Premises used: Finset.coe_Ioc, Finset.coe_Ioo, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ioc a b

Tactic:
Set.Ioo_subset_Ioc_self

Premises used: Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ioc a b

Tactic:
exact Set.Ioo_subset_Ioc_self

Premises used: Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : Set.Ico a b ⊆ Set.Icc a b
⊢ Ico a b ⊆ Icc a b

Tactic:
rw [← coe_subset, coe_Ico, coe_Icc]

Premises used: Finset.coe_Ico, Finset.coe_Icc, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Set.Ico a b ⊆ Set.Icc a b

Tactic:
Set.Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Set.Ico a b ⊆ Set.Icc a b

Tactic:
exact Set.Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : Set.Ioc a b ⊆ Set.Icc a b
⊢ Ioc a b ⊆ Icc a b

Tactic:
rw [← coe_subset, coe_Ioc, coe_Icc]

Premises used: Finset.coe_Icc, Finset.coe_Ioc, Finset.coe_subset
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Set.Ioc a b ⊆ Set.Icc a b

Tactic:
Set.Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Set.Ioc a b ⊆ Set.Icc a b

Tactic:
exact Set.Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self