awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ Iio a ⊆ Iic b

Tactic:
(Iio_subset_Iio h).trans Iio_subset_Iic_self

Premises used: HasSubset.Subset.trans, Set.Iio_subset_Iio, Set.Iio_subset_Iic_self
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Iio a ⊂ Iic a

Tactic:
⟨Iio_subset_Iic_self, fun h => (h le_rfl).false⟩

Premises used: le_rfl, And.intro, Set.Iio_subset_Iic_self, LT.lt.false
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ⊆ Ioo a₂ b₂

Tactic:
fun _ ⟨hx₁, hx₂⟩ =>
  ⟨ha.trans_lt hx₁, hx₂.trans_le hb⟩

Premises used: _private.0.Set.Ioo_eq_empty.match_1, Membership.mem, Set.Subset, LT.lt.trans_le, And.intro, LE.le.trans_lt, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b : α
h : a₁ ≤ a₂
⊢ Ioo a₂ b ⊆ Ioo a₁ b

Tactic:
Ioo_subset_Ioo h le_rfl

Premises used: le_rfl, Set.Ioo_subset_Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂

Tactic:
fun _ hx =>
  ⟨ha.trans hx.1, hx.2.trans_le hb⟩

Premises used: Set.Mem, setOf, Set.Subset, Set.Ico, And.right, And.left, LT.lt.trans_le, And.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b : α
h : a₁ ≤ a₂
⊢ Ico a₂ b ⊆ Ico a₁ b

Tactic:
Ico_subset_Ico h le_rfl

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

Tactic:
Ioc_subset_Ioc h le_rfl

Premises used: le_rfl, Set.Ioc_subset_Ioc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂

Tactic:
fun _ ⟨hx₁, hx₂⟩ =>
  ⟨ha.trans hx₁, le_trans hx₂ hb⟩

Premises used: Membership.mem, _private.0.Set.Icc_eq_empty.match_1, Set.Subset, Set.Icc, And.intro, LE.le.trans, le_trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b : α
h : a₁ ≤ a₂
⊢ Icc a₂ b ⊆ Icc a₁ b

Tactic:
Icc_subset_Icc h le_rfl

Premises used: le_rfl, Set.Icc_subset_Icc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
h₂ : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
(ssubset_iff_of_subset (Icc_subset_Icc (le_of_lt ha) hb)).mpr
    ⟨a₂, left_mem_Icc.mpr h₂, not_and.mpr fun f _ => lt_irrefl a₂ (ha.trans_le f)⟩

Premises used: Iff.mpr, lt_irrefl, le_of_lt, Set.left_mem_Icc, LT.lt.trans_le, Set.Icc_subset_Icc, And.intro, Exists.intro, Set.ssubset_iff_of_subset, not_and
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ioo a₂ b₂

Tactic:
fun _ hx ↦
  ⟨ha.trans_le hx.1, hx.2.trans_le hb⟩

Premises used: Set.Mem, setOf, Set.Subset, And.right, And.left, LT.lt.trans_le, And.intro, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b : α
h : a₁ < a₂
⊢ Ico a₂ b ⊆ Ioo a₁ b

Tactic:
Ico_subset_Ioo h le_rfl

Premises used: le_rfl, Set.Ico_subset_Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Ioc a₂ b₂

Tactic:
fun _ hx ↦
  ⟨ha.trans_le hx.1, hx.2.trans hb⟩

Premises used: Set.Ioc, Set.Mem, setOf, Set.Subset, And.right, And.left, LT.lt.trans_le, And.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b : α
h : a₁ < a₂
⊢ Icc a₂ b ⊆ Ioc a₁ b

Tactic:
Icc_subset_Ioc h le_rfl

Premises used: le_rfl, Set.Icc_subset_Ioc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
ha : a₂ < a₁
hb : b₁ < b₂
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂

Tactic:
(Icc_subset_Ioc_left ha).trans (Ioc_subset_Ioo_right hb)

Premises used: HasSubset.Subset.trans, Set.Icc_subset_Ioc_left, Set.Ioc_subset_Ioo_right
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ico a b ⊆ Iio b

Tactic:
fun _ => And.right

Premises used: Set.Mem, setOf, Set.Subset, Set.Ico, And.right, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioo a b ⊆ Iio b

Tactic:
fun _ => And.right

Premises used: Set.Mem, setOf, Set.Subset, And.right, Set.Iio, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioc a b ⊆ Iic b

Tactic:
fun _ => And.right

Premises used: Set.Ioc, Set.Mem, setOf, Set.Subset, And.right, Set.Iic
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Icc a b ⊆ Iic b

Tactic:
fun _ => And.right

Premises used: Set.Mem, setOf, Set.Subset, Set.Icc, And.right, Set.Iic
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioo a b ⊆ Ico a b

Tactic:
fun _ => And.imp_left le_of_lt

Premises used: Set.Mem, setOf, le_of_lt, And.imp_left, Set.Subset, Set.Ico, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioc a b ⊆ Icc a b

Tactic:
fun _ => And.imp_left le_of_lt

Premises used: Set.Ioc, Set.Mem, setOf, le_of_lt, And.imp_left, Set.Subset, Set.Icc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioo a b ⊆ Icc a b

Tactic:
Ioo_subset_Ico_self.trans Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, HasSubset.Subset.trans, Set.Ioo_subset_Ico_self
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
⟨fun h => ⟨(h ⟨le_rfl, h₁⟩).1, (h ⟨h₁, le_rfl⟩).2⟩, fun ⟨h, h'⟩ _ hx =>
    ⟨h.trans hx.1, hx.2.trans h'⟩⟩

Premises used: le_rfl, Membership.mem, Set.Icc, And.right, And.left, And.intro, Iff.intro, LE.le.trans, _private.0.Set.Icc_subset_Icc_iff.match_1
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Tactic:
⟨fun h => ⟨(h ⟨le_rfl, h₁⟩).1, (h ⟨h₁, le_rfl⟩).2⟩, fun ⟨h, h'⟩ _ hx =>
    ⟨h.trans_le hx.1, hx.2.trans_lt h'⟩⟩

Premises used: le_rfl, Membership.mem, _private.0.Set.Icc_subset_Ioo_iff.match_1, And.right, And.left, LT.lt.trans_le, And.intro, Iff.intro, LE.le.trans_lt, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Tactic:
⟨fun h => ⟨(h ⟨le_rfl, h₁⟩).1, (h ⟨h₁, le_rfl⟩).2⟩, fun ⟨h, h'⟩ _ hx =>
    ⟨h.trans hx.1, hx.2.trans_lt h'⟩⟩

Premises used: le_rfl, _private.0.Set.Icc_subset_Ico_iff.match_1, Membership.mem, Set.Ico, And.right, And.left, And.intro, Iff.intro, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂

Tactic:
⟨fun h => ⟨(h ⟨le_rfl, h₁⟩).1, (h ⟨h₁, le_rfl⟩).2⟩, fun ⟨h, h'⟩ _ hx =>
    ⟨h.trans_le hx.1, hx.2.trans h'⟩⟩

Premises used: _private.0.Set.Icc_subset_Ioc_iff.match_1, Set.Ioc, le_rfl, Membership.mem, And.right, And.left, LT.lt.trans_le, And.intro, Iff.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioi a₂ ↔ a₂ < a₁

Tactic:
⟨fun h => h ⟨le_rfl, h₁⟩, fun h _ hx => h.trans_le hx.1⟩

Premises used: le_rfl, And.left, LT.lt.trans_le, And.intro, Iff.intro
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a₁ a₂ b₁ : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ici a₂ ↔ a₂ ≤ a₁

Tactic:
⟨fun h => h ⟨le_rfl, h₁⟩, fun h _ hx => h.trans hx.1⟩

Premises used: le_rfl, And.left, And.intro, Iff.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ici a ∩ Iic b = Icc a b

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.inter, Set.Icc, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ici a ∩ Iio b = Ico a b

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.inter, Set.Ico, Set.Iio, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioi a ∩ Iic b = Ioc a b

Tactic:
rfl

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, Set.inter, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioi a ∩ Iio b = Ioo a b

Tactic:
rfl

Premises used: Set.Ioi, Set.Mem, setOf, Set.inter, Set.Iio, Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b x : α
h : x ∈ Ioo a b
⊢ x ∈ Icc a b

Tactic:
Ioo_subset_Icc_self h

Premises used: Set.Ioo_subset_Icc_self
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b x : α
h : x ∈ Ioo a b
⊢ x ∈ Ico a b

Tactic:
Ioo_subset_Ico_self h

Premises used: Set.Ioo_subset_Ico_self
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b x : α
h : x ∈ Ioc a b
⊢ x ∈ Icc a b

Tactic:
Ioc_subset_Icc_self h

Premises used: Set.Ioc_subset_Icc_self
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a x : α
h : x ∈ Iio a
⊢ x ∈ Iic a

Tactic:
Iio_subset_Iic_self h

Premises used: Set.Iio_subset_Iic_self
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
contrapose! : (Icc a b).Nonempty ↔ a ≤ b
⊢ Icc a b = ∅ ↔ ¬a ≤ b

Tactic:
contrapose!
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (Icc a b).Nonempty ↔ a ≤ b

Tactic:
nonempty_Icc

Premises used: Set.nonempty_Icc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (Icc a b).Nonempty ↔ a ≤ b

Tactic:
exact nonempty_Icc

Premises used: Set.nonempty_Icc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
contrapose! : (Ico a b).Nonempty ↔ a < b
⊢ Ico a b = ∅ ↔ ¬a < b

Tactic:
contrapose!
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (Ico a b).Nonempty ↔ a < b

Tactic:
nonempty_Ico

Premises used: Set.nonempty_Ico
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (Ico a b).Nonempty ↔ a < b

Tactic:
exact nonempty_Ico

Premises used: Set.nonempty_Ico
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
inst_1 : DenselyOrdered α
contrapose! : (Ioo a b).Nonempty ↔ a < b
⊢ Ioo a b = ∅ ↔ ¬a < b

Tactic:
contrapose!
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
inst_1 : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b

Tactic:
nonempty_Ioo

Premises used: Set.nonempty_Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
inst_1 : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b

Tactic:
exact nonempty_Ioo

Premises used: Set.nonempty_Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
h : IsTop a
⊢ Iic a = univ

Tactic:
eq_univ_of_forall h

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Iio a = ∅ ↔ IsMin a

Tactic:
simp only [isMin_iff_forall_not_lt, eq_empty_iff_forall_notMem, mem_Iio]

Premises used: Set.mem_Iio, Set.eq_empty_iff_forall_notMem, isMin_iff_forall_not_lt
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
simp [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b c : α
h : a ≤ c
⊢ Iic a ∩ Ioc b c = Ioc b a

Tactic:
ext fun _ => ⟨fun H => ⟨H.2.1, H.1⟩, fun H => ⟨H.2, H.1, H.2.trans h⟩⟩

Premises used: Set.ext, And.right, And.left, And.intro, Iff.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b c : α
ha : c < a
⊢ ¬c ∈ Icc a b

Tactic:
fun h => ha.not_ge h.1

Premises used: And.left, LT.lt.not_ge, Not
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b c : α
ha : c < a
⊢ ¬c ∈ Ico a b

Tactic:
fun h => ha.not_ge h.1

Premises used: And.left, LT.lt.not_ge, Not
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b c : α
ha : c ≤ a
⊢ ¬c ∈ Ioc a b

Tactic:
fun h => lt_irrefl _ <| h.1.trans_le ha

Premises used: lt_irrefl, And.left, LT.lt.trans_le, Not
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b c : α
ha : c ≤ a
⊢ ¬c ∈ Ioo a b

Tactic:
fun h => lt_irrefl _ <| h.1.trans_le ha

Premises used: lt_irrefl, And.left, LT.lt.trans_le, Not
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : Icc a b = Ioc a b
⊢ ¬a ≤ b

Tactic:
simpa using Set.ext_iff.mp h a

Premises used: Iff.mp, Set.ext_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a ≤ b
rw : ∅ = Ioc a b
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ Icc a b = Ioc a b

Tactic:
rw [Icc_eq_empty h, Ioc_eq_empty (mt le_of_lt h)]

Premises used: Set.Icc_eq_empty, le_of_lt, mt, Set.Ioc_eq_empty
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioc a b = Icc a b ↔ ¬a ≤ b

Tactic:
eq_comm.trans Icc_eq_Ioc_same_iff

Premises used: eq_comm, Set.Icc_eq_Ioc_same_iff, Iff.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : Icc a b = Ioo a b
⊢ ¬a ≤ b

Tactic:
simpa using Set.ext_iff.mp h b

Premises used: Iff.mp, Set.ext_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a ≤ b
rw : ∅ = Ioo a b
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ Icc a b = Ioo a b

Tactic:
rw [Icc_eq_empty h, Ioo_eq_empty (mt le_of_lt h)]

Premises used: Set.Icc_eq_empty, le_of_lt, mt, Set.Ioo_eq_empty
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioo a b = Icc a b ↔ ¬a ≤ b

Tactic:
eq_comm.trans Icc_eq_Ioo_same_iff

Premises used: eq_comm, Iff.trans, Set.Icc_eq_Ioo_same_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : Ioc a b = Ico a b
⊢ ¬a < b

Tactic:
simpa using Set.ext_iff.mp h a

Premises used: Iff.mp, Set.ext_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a < b
rw : ∅ = Ico a b
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ Ioc a b = Ico a b

Tactic:
rw [Ioc_eq_empty h, Ico_eq_empty h]

Premises used: Set.Ioc_eq_empty, Set.Ico_eq_empty
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : Ioo a b = Ioc a b
⊢ ¬a < b

Tactic:
simpa using Set.ext_iff.mp h b

Premises used: Iff.mp, Set.ext_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a < b
rw : ∅ = Ioc a b
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ Ioo a b = Ioc a b

Tactic:
rw [Ioo_eq_empty h, Ioc_eq_empty h]

Premises used: Set.Ioc_eq_empty, Set.Ioo_eq_empty
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioc a b = Ioo a b ↔ ¬a < b

Tactic:
eq_comm.trans Ioo_eq_Ioc_same_iff

Premises used: eq_comm, Set.Ioo_eq_Ioc_same_iff, Iff.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ ∀ (x : α), x ∈ Icc a a ↔ Membership.mem (γ := Set α) {a} x

Tactic:
simp [Icc, le_antisymm_iff, and_comm]

Premises used: and_comm, Set.Icc, le_antisymm_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
⊢ a ∈ Icc a a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
y : (↑(Icc a a) : Type u_1)
⊢ (↑y : α) = (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a a) a ⋯) : α)

Tactic:
simpa using y.2

Premises used: Subtype.property
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
refine_1 : ∀ (h : Icc a b = {c}), a = c ∧ b = c
refine_2 : a = c ∧ b = c → Icc a b = {c}
⊢ Icc a b = {c} ↔ a = c ∧ b = c

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a ≤ b

Tactic:
have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : Icc a b = {c}
hab : a ≤ b
⊢ a = c ∧ b = c

Tactic:
⟨eq_of_mem_singleton <| h ▸ left_mem_Icc.2 hab,
        eq_of_mem_singleton <| h ▸ right_mem_Icc.2 hab⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.eq_of_mem_singleton, Eq.rec, Set.left_mem_Icc, And.intro
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : Icc a b = {c}
hab : a ≤ b
⊢ a = c ∧ b = c

Tactic:
exact
      ⟨eq_of_mem_singleton <| h ▸ left_mem_Icc.2 hab,
        eq_of_mem_singleton <| h ▸ right_mem_Icc.2 hab⟩
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
b : α
⊢ Icc b b = {b}

Tactic:
Icc_self _

Premises used: Set.Icc_self
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
b : α
⊢ Icc b b = {b}

Tactic:
exact Icc_self _

Premises used: Set.Icc_self
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hba : b ≤ a
⊢ (Icc a b).Subsingleton

Tactic:
fun _x ⟨hax, hxb⟩ _y ⟨hay, hyb⟩ ↦ le_antisymm
    (le_imp_le_of_le_of_le hxb hay hba) (le_imp_le_of_le_of_le hyb hax hba)

Premises used: _private.0.Set.subsingleton_Icc_of_ge.match_1, le_imp_le_of_le_of_le, le_antisymm, Set.Subsingleton, Eq
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ (Icc a b).Subsingleton ↔ b ≤ a

Tactic:
⟨fun h ↦ ?_, subsingleton_Icc_of_ge⟩

Premises used: Iff.intro, Set.subsingleton_Icc_of_ge
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
refine : ∀ (h : (Icc a b).Subsingleton), b ≤ a
⊢ (Icc a b).Subsingleton ↔ b ≤ a

Tactic:
refine ⟨fun h ↦ ?_, subsingleton_Icc_of_ge⟩
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : (Icc a b).Subsingleton
contrapose! : ∀ (h : a < b), (Icc a b).Nontrivial
⊢ b ≤ a

Tactic:
contrapose! h
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : a < b
⊢ (Icc a b).Nontrivial

Tactic:
⟨a, ⟨le_refl _, h.le⟩, b, ⟨h.le, le_refl _⟩, h.ne⟩

Premises used: le_refl, LT.lt.le, And.intro, Exists.intro, Set.Nontrivial, LT.lt.ne
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : a < b
⊢ (Icc a b).Nontrivial

Tactic:
exact ⟨a, ⟨le_refl _, h.le⟩, b, ⟨h.le, le_refl _⟩, h.ne⟩
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b x : α
⊢ x ∈ Icc a b \ {a} ↔ x ∈ Ioc a b

Tactic:
simp [lt_iff_le_and_ne, eq_comm, and_right_comm]

Premises used: lt_iff_le_and_ne, eq_comm, and_right_comm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b x : α
⊢ x ∈ Ico a b \ {a} ↔ x ∈ Ioo a b

Tactic:
simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm]

Premises used: lt_iff_le_and_ne, eq_comm, and_right_comm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : Icc a b \ ({a} ∪ {b}) = Ioo a b
rw₁ : (Icc a b \ {a}) \ {b} = Ioo a b
rw₂ : Ioc a b \ {b} = Ioo a b
rw₃ rw₄ : Ioo a b = Ioo a b
⊢ Icc a b \ {a, b} = Ioo a b

Tactic:
rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]

Premises used: Set.insert_eq, Set.Icc_diff_left, Set.Ioc_diff_right, Set.diff_diff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a x : α
⊢ x ∈ Iic a \ {a} ↔ x ∈ Iio a

Tactic:
simp [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a < b
rw : Ico a b \ (Ico a b \ {a}) = {a}
rw₁ rw₂ : Eq (α := Set α) {a} {a}
⊢ Ico a b \ Ioo a b = {a}

Tactic:
rw [← Ico_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)]

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.left_mem_Ico, Set.diff_diff_cancel_left, Set.Ico_diff_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
rw : Icc a b \ (Icc a b \ {b}) = {b}
rw₁ rw₂ : Eq (α := Set α) {b} {b}
⊢ Icc a b \ Ico a b = {b}

Tactic:
rw [← Icc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Icc.2 h)]

Premises used: Iff.mpr, Set.right_mem_Icc, Set.singleton_subset_iff, Set.Icc_diff_right, Set.diff_diff_cancel_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
rw : {a, b} ⊆ Icc a b
⊢ Icc a b \ Ioo a b = {a, b}

Tactic:
rw [← Icc_diff_both, diff_diff_cancel_left]

Premises used: Set.Icc_diff_both, Set.diff_diff_cancel_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ {a, b} ⊆ Icc a b

Tactic:
simp [insert_subset_iff, h]

Premises used: Set.insert_subset_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
rw : Iic a \ (Iic a \ {a}) = {a}
rw₁ rw₂ : Eq (α := Set α) {a} {a}
⊢ Iic a \ Iio a = {a}

Tactic:
rw [← Iic_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 self_mem_Iic)]

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.self_mem_Iic, Set.Iic_diff_right, Set.diff_diff_cancel_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ Iio a ∪ {a} = Iic a

Tactic:
ext fun _ => le_iff_lt_or_eq.symm

Premises used: Set.ext, le_iff_lt_or_eq, Iff.symm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hab : a < b
rw : Ico a b \ {a} ∪ {a} = Ico a b
rw₁ : Ico a b ∪ {a} = Ico a b
rw₂ rw₃ : Ico a b = Ico a b
⊢ Ioo a b ∪ {a} = Ico a b

Tactic:
rw [← Ico_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.left_mem_Ico, Set.union_eq_self_of_subset_right, Set.diff_union_self, Set.Ico_diff_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ {a, b} ∪ {a, b} = Icc a b

Tactic:
have : (Icc a b \ {a, b}) ∪ {a, b} = Icc a b := diff_union_of_subset fun
    | x, .inl rfl => left_mem_Icc.mpr h
    | x, .inr rfl => right_mem_Icc.mpr h
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
this : Icc a b \ {a, b} ∪ {a, b} = Icc a b
rw : Ioo a b ∪ {a, b} = Icc a b \ {a, b} ∪ {a, b}
rw₁ rw₂ : Ioo a b ∪ {a, b} = Ioo a b ∪ {a, b}
⊢ Ioo a b ∪ {a, b} = Icc a b

Tactic:
rw [← this, Icc_diff_both]

Premises used: Set.Icc_diff_both
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hab : a ≤ b
rw : Icc a b \ {a} ∪ {a} = Icc a b
rw₁ : Icc a b ∪ {a} = Icc a b
rw₂ rw₃ : Icc a b = Icc a b
⊢ Ioc a b ∪ {a} = Icc a b

Tactic:
rw [← Icc_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.union_eq_self_of_subset_right, Set.Icc_diff_left, Set.diff_union_self, Set.left_mem_Icc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
rw : {b} ∪ Ico a b = Icc a b
rw₁ : Ico a b ∪ {b} = Icc a b
rw₂ rw₃ : Icc a b = Icc a b
⊢ insert b (Ico a b) = Icc a b

Tactic:
rw [insert_eq, union_comm, Ico_union_right h]

Premises used: Set.insert_eq, Set.union_comm, Set.Ico_union_right