awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
x y : α
x_1 : (↑(Ioc x y) : Type u_1)
a : α
ha : a ∈ Ioc x y
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ (b : (↑(Ioc x y) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioc x y) a ha

Tactic:
⟨⟨b, mem_Ioc.mpr ⟨hb₁, hb₂.le.trans ha.2⟩⟩, hb₂⟩

Premises used: Iff.mpr, LT.lt.le, Subtype.mk, And.right, And.intro, Exists.intro, Set.mem_Ioc, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
x y : α
x_1 : (↑(Ioc x y) : Type u_1)
a : α
ha : a ∈ Ioc x y
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ (b : (↑(Ioc x y) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioc x y) a ha

Tactic:
exact ⟨⟨b, mem_Ioc.mpr ⟨hb₁, hb₂.le.trans ha.2⟩⟩, hb₂⟩
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
x y : α
x_1 : (↑(Ioi x) : Type u_1)
a : α
ha : a ∈ Ioi x
rcases :
  ∀ (b : α) (hb₁ : x < b) (hb₂ : b < a),
    ∃ (b : (↑(Ioi x) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioi x) a ha
⊢ ∃ (b : (↑(Ioi x) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioi x) a ha

Tactic:
rcases exists_between ha with ⟨b, hb₁, hb₂⟩

Premises used: exists_between
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
x y : α
x_1 : (↑(Ioi x) : Type u_1)
a : α
ha : a ∈ Ioi x
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ (b : (↑(Ioi x) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioi x) a ha

Tactic:
⟨⟨b, hb₁⟩, hb₂⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
x y : α
x_1 : (↑(Ioi x) : Type u_1)
a : α
ha : a ∈ Ioi x
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ (b : (↑(Ioi x) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioi x) a ha

Tactic:
exact ⟨⟨b, hb₁⟩, hb₂⟩
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
⊢ Iic False = {False}

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
⊢ Iic True = univ

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
⊢ Ici False = univ

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
⊢ Ici True = {True}

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
⊢ Iio False = ∅

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
⊢ Iio True = {False}

Tactic:
aesop (add simp [Ioi, lt_iff_le_not_ge])

Premises used: Set.Ioi, lt_iff_le_not_ge
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
⊢ Ioi False = {True}

Tactic:
aesop (add simp [Ioi, lt_iff_le_not_ge])

Premises used: Set.Ioi, lt_iff_le_not_ge
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
⊢ Ioi True = ∅

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
b x : α
⊢ x ∈ Iio b ↔ x < b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ {x : α | x < a} = Iio a

Tactic:
rfl

Premises used: Set.Iio, rfl
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
b x : α
⊢ x ∈ Iic b ↔ x ≤ b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Iic
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
b : α
⊢ {x : α | x ≤ b} = Iic b

Tactic:
rfl

Premises used: Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | b < x ∧ x < a} {x : α | x < a ∧ b < x}

Tactic:
simp only [and_comm]

Premises used: and_comm
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b x : α
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ {x : α | a < x ∧ x < b} = Ioo a b

Tactic:
rfl

Premises used: Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | b < x ∧ x ≤ a} {x : α | x ≤ a ∧ b < x}

Tactic:
simp only [and_comm]

Premises used: and_comm
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | b ≤ x ∧ x < a} {x : α | x < a ∧ b ≤ x}

Tactic:
simp only [and_comm]

Premises used: and_comm
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b x : α
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Ico
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ {x : α | a ≤ x ∧ x < b} = Ico a b

Tactic:
rfl

Premises used: Set.Ico, rfl
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b x : α
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
.rfl

Premises used: Set.Ioc, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ {x : α | a < x ∧ x ≤ b} = Ioc a b

Tactic:
rfl

Premises used: Set.Ioc, rfl
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | b ≤ x ∧ x ≤ a} {x : α | x ≤ a ∧ b ≤ x}

Tactic:
simp only [and_comm]

Premises used: and_comm
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b x : α
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Icc
-- Module: Mathlib.Order.Interval.Set.Defs
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ {x : α | a ≤ x ∧ x ≤ b} = Icc a b

Tactic:
rfl

Premises used: Set.Icc, rfl
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b : α
h : a ≤ b
⊢ Disjoint (Iic a) (Ioi b)

Tactic:
disjoint_left.mpr fun _ ha hb => (h.trans_lt hb).not_ge ha

Premises used: Iff.mpr, Set.disjoint_left, LT.lt.not_ge, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b : α
h : a ≤ b
⊢ Disjoint (Iio a) (Ici b)

Tactic:
disjoint_left.mpr fun _ ha hb => (h.trans_lt' ha).not_ge hb

Premises used: Iff.mpr, Set.disjoint_left, LE.le.trans_lt', LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b c : α
h : a ≤ b
⊢ Disjoint (Iic a) (Ioc b c)

Tactic:
(Iic_disjoint_Ioi h).mono le_rfl Ioc_subset_Ioi_self

Premises used: le_rfl, Set.Iic_disjoint_Ioi, Set.Ioc_subset_Ioi_self, Disjoint.mono
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b c d : α
h : b ≤ c
⊢ Disjoint (Ioc a b) (Ioc c d)

Tactic:
(Iic_disjoint_Ioc h).mono Ioc_subset_Iic_self le_rfl

Premises used: le_rfl, Set.Ioc_subset_Iic_self, Set.Iic_disjoint_Ioc, Disjoint.mono
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b c : α
⊢ Disjoint (Ico a b) (Ico b c)

Tactic:
disjoint_left.mpr fun _ hab hbc => hab.2.not_ge hbc.1

Premises used: Iff.mpr, Set.disjoint_left, And.right, And.left, LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b : α
rw : Ici a ∩ Iic b = ∅ ↔ ¬a ≤ b
rw₁ : Icc a b = ∅ ↔ ¬a ≤ b
rw₂ rw₃ : ¬a ≤ b ↔ ¬a ≤ b
⊢ Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b

Tactic:
rw [Set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]

Premises used: Set.Icc_eq_empty_iff, Set.disjoint_iff_inter_eq_empty, Set.Ici_inter_Iic
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b c : α
h : b ≤ c
⊢ Disjoint (Ioc a b) (Ioi c)

Tactic:
disjoint_left.mpr (fun _ hx hy ↦ (hx.2.trans h).not_gt hy)

Premises used: Iff.mpr, Set.disjoint_left, And.right, LE.le.not_gt, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b : α
⊢ Disjoint (Ioc a b) (Ioi b)

Tactic:
Ioc_disjoint_Ioi le_rfl

Premises used: le_rfl, Set.Ioc_disjoint_Ioi
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b : α
h : ¬a < b
⊢ Disjoint (Ioi a) (Iio b)

Tactic:
disjoint_left.mpr fun _ hx hy ↦ h (hx.trans hy)

Premises used: Iff.mpr, Set.disjoint_left, LT.lt.trans
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b : α
h : a ≤ b
⊢ Disjoint (Ioi b) (Iio a)

Tactic:
Ioi_disjoint_Iio_of_not_lt (not_lt_of_ge h)

Premises used: Set.Ioi_disjoint_Iio_of_not_lt, not_lt_of_ge
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a : α
⊢ Disjoint (Ioi a) (Iio a)

Tactic:
Ioi_disjoint_Iio_of_le le_rfl

Premises used: le_rfl, Set.Ioi_disjoint_Iio_of_le
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a b : α
inst_1 : DenselyOrdered α
⊢ Disjoint (Ioi a) (Iio b) ↔ ¬a < b

Tactic:
⟨fun h hab ↦ (exists_between hab).elim
    fun _ hc ↦ h.notMem_of_mem_left hc.left hc.right,
    Ioi_disjoint_Iio_of_not_lt⟩

Premises used: exists_between, Set.Ioi_disjoint_Iio_of_not_lt, And.right, And.left, Iff.intro, Disjoint.notMem_of_mem_left, Exists.elim
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
⊢ Eq.{v + 1} (α := Set α) (⋃ (a : α), Iic a) univ

Tactic:
iUnion_eq_univ_iff.2 fun x => ⟨x, self_mem_Iic⟩

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff, Set.self_mem_Iic, Exists.intro
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a : α
⊢ ⋃ (b : α), Icc a b = Ici a

Tactic:
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]

Premises used: Set.iUnion_Iic, Set.inter_univ, Set.inter_iUnion, Set.Ici_inter_Iic
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
a : α
⊢ ⋃ (b : α), Ioc a b = Ioi a

Tactic:
simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]

Premises used: Set.Ioi_inter_Iic, Set.iUnion_Iic, Set.inter_univ, Set.inter_iUnion
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
inst_1 : NoMaxOrder α
⊢ Eq.{v + 1} (α := Set α) (⋃ (a : α), Iio a) univ

Tactic:
iUnion_eq_univ_iff.2 exists_gt

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff, NoMaxOrder.exists_gt
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
⊢ ⋃ (b : α), Ico a b = Ici a

Tactic:
simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]

Premises used: Set.Ici_inter_Iio, Set.iUnion_Iio, Set.inter_univ, Set.inter_iUnion
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
⊢ ⋃ (b : α), Ioo a b = Ioi a

Tactic:
simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]

Premises used: Set.iUnion_Iio, Set.inter_univ, Set.Ioi_inter_Iio, Set.inter_iUnion
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
simp_rw : Ico a₁ a₂ ∩ Ico b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
simp_rw₁ : Ico (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
simp_rw₂ : ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁
⊢ Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
simp_rw [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, not_lt]

Premises used: Set.Ico_inter_Ico, Set.disjoint_iff_inter_eq_empty, not_lt, Set.Ico_eq_empty_iff
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (α := Set αᵒᵈ) (Ico ((toDual : (a : α) → αᵒᵈ) a₂) ((toDual : (a : α) → αᵒᵈ) a₁) : Set αᵒᵈ)
      (Ico ((toDual : (a : α) → αᵒᵈ) b₂) ((toDual : (a : α) → αᵒᵈ) b₁) : Set αᵒᵈ) ↔
    LE.le (α := αᵒᵈ) (min ((toDual : (a : α) → αᵒᵈ) a₁) ((toDual : (a : α) → αᵒᵈ) b₁) : αᵒᵈ)
      (max ((toDual : (a : α) → αᵒᵈ) a₂) ((toDual : (a : α) → αᵒᵈ) b₂) : αᵒᵈ)

Tactic:
have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h :
  Disjoint (α := Set αᵒᵈ) (Ico ((toDual : (a : α) → αᵒᵈ) a₂) ((toDual : (a : α) → αᵒᵈ) a₁) : Set αᵒᵈ)
      (Ico ((toDual : (a : α) → αᵒᵈ) b₂) ((toDual : (a : α) → αᵒᵈ) b₁) : Set αᵒᵈ) ↔
    LE.le (α := αᵒᵈ) (min ((toDual : (a : α) → αᵒᵈ) a₁) ((toDual : (a : α) → αᵒᵈ) b₁) : αᵒᵈ)
      (max ((toDual : (a : α) → αᵒᵈ) a₂) ((toDual : (a : α) → αᵒᵈ) b₂) : αᵒᵈ)
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
simpa only [Ico_toDual] using h

Premises used: Set.Ico_toDual
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
simp_rw : Ioo a₁ a₂ ∩ Ioo b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
simp_rw₁ : Ioo (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
simp_rw₂ : ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁
⊢ Disjoint (Ioo a₁ a₂) (Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
simp_rw [Set.disjoint_iff_inter_eq_empty, Ioo_inter_Ioo, Ioo_eq_empty_iff, not_lt]

Premises used: Set.disjoint_iff_inter_eq_empty, not_lt, Set.Ioo_eq_empty_iff, Set.Ioo_inter_Ioo
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ x₁ ∨ x₂ ≤ y₁

Tactic:
rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h

Premises used: le_of_lt, Set.Ico_disjoint_Ico, min_eq_left, And.right, le_max_iff
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
h₁ : x₂ ≤ x₁ ∨ x₂ ≤ y₁
⊢ x₁ < x₂

Tactic:
rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h

Premises used: le_of_lt, Set.Ico_disjoint_Ico, min_eq_left, And.right, le_max_iff
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
h₁ : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx₁ : x₁ < x₂
⊢ x₂ ∈ Ico y₁ y₂

Tactic:
rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h

Premises used: le_of_lt, Set.Ico_disjoint_Ico, min_eq_left, And.right, le_max_iff
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
apply : x₂ ≤ y₁
⊢ y₁ = x₂

Tactic:
apply le_antisymm h2.1

Premises used: le_antisymm, And.left
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁

Tactic:
h.elim (fun h => absurd hx (not_lt_of_ge h)) id

Premises used: id, absurd, Or.elim, not_lt_of_ge
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁

Tactic:
exact h.elim (fun h => absurd hx (not_lt_of_ge h)) id

Premises used: id, absurd, Or.elim, not_lt_of_ge
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
a : α
⊢ ⋃ (i : ι), Ico (f i) a = Iio a ↔ ∀ x < a, ∃ (i : ι), f i ≤ x

Tactic:
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

Premises used: Set.Ici_inter_Iio, Set.subset_def, Set.iUnion_inter
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
a : α
⊢ ⋃ (i : ι), Ioc a (f i) = Ioi a ↔ ∀ (x : α), a < x → ∃ (i : ι), x ≤ f i

Tactic:
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]

Premises used: Set.Ioi_inter_Iic, Set.subset_def, Set.inter_iUnion
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ (i : ι), ⋃ (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ x < a, ∃ (i : ι) (hi : p i), f i hi ≤ x

Tactic:
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

Premises used: Set.Ici_inter_Iio, Set.subset_def, Set.iUnion_inter
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ (i : ι), ⋃ (hi : p i), Ioc a (f i hi) = Ioi a ↔ ∀ (x : α), a < x → ∃ (i : ι) (hi : p i), x ≤ f i hi

Tactic:
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]

Premises used: Set.Ioi_inter_Iic, Set.subset_def, Set.inter_iUnion
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
⊢ ⋃ x ∈ s, Ioi x = Ioi a

Tactic:
(iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_

Premises used: Set.iUnion₂_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
refine_1 : ∀ (x : α) (hx : x ∈ s), Ioi x ⊆ Ioi a
refine_2 : ∀ (x : α) (hx : x ∈ Ioi a), Membership.mem (γ := Set α) (⋃ i ∈ s, Ioi i) x
⊢ ⋃ x ∈ s, Ioi x = Ioi a

Tactic:
refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_

Premises used: Set.iUnion₂_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ s
⊢ Ioi x ⊆ Ioi a

Tactic:
Ioi_subset_Ioi (h.1 hx)

Premises used: And.left, Set.Ioi_subset_Ioi
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ s
⊢ Ioi x ⊆ Ioi a

Tactic:
exact Ioi_subset_Ioi (h.1 hx)

Premises used: And.left, Set.Ioi_subset_Ioi
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
refine_2 : ∀ (y : α) (hys : y ∈ s), a ≤ y → ∀ (hyx : y < x), Membership.mem (γ := Set α) (⋃ i ∈ s, Ioi i) x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ioi i) x

Tactic:
rcases h.exists_between hx with ⟨y, hys, _, hyx⟩

Premises used: IsGLB.exists_between
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left : a ≤ y
hyx : y < x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ioi i) x

Tactic:
mem_biUnion hys hyx

Premises used: Set.mem_biUnion
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left : a ≤ y
hyx : y < x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ioi i) x

Tactic:
exact mem_biUnion hys hyx

Premises used: Set.mem_biUnion
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
a : α
f : ι → α
h : IsGLB (range f) a
⊢ ⋃ (x : ι), Ioi (f x) = Ioi a

Tactic:
biUnion_range.symm.trans h.biUnion_Ioi_eq

Premises used: Set.biUnion_range, IsGLB.biUnion_Ioi_eq, Eq.symm, Eq.trans
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsLUB s a
⊢ ⋃ x ∈ s, Iio x = Iio a

Tactic:
h.dual.biUnion_Ioi_eq

Premises used: Set.Mem, setOf, IsGLB.biUnion_Ioi_eq, Set.preimage, IsLUB.dual, OrderDual, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
a : α
f : ι → α
h : IsLUB (range f) a
⊢ ⋃ (x : ι), Iio (f x) = Iio a

Tactic:
h.dual.iUnion_Ioi_eq

Premises used: setOf, IsLUB.dual, OrderDual, Set.Iio, IsGLB.iUnion_Ioi_eq
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
⊢ ⋃ x ∈ s, Ici x = Ioi a

Tactic:
(iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_

Premises used: Set.iUnion₂_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
refine_1 : ∀ (x : α) (hx : x ∈ s), Ici x ⊆ Ioi a
refine_2 : ∀ (x : α) (hx : x ∈ Ioi a), Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x
⊢ ⋃ x ∈ s, Ici x = Ioi a

Tactic:
refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_

Premises used: Set.iUnion₂_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ioi a

Tactic:
Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_notMem) hx)

Premises used: Iff.mpr, And.left, Set.Ici_subset_Ioi, lt_of_le_of_ne
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ioi a

Tactic:
exact Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_notMem) hx)

Premises used: Iff.mpr, And.left, Set.Ici_subset_Ioi, lt_of_le_of_ne
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
refine_2 : ∀ (y : α) (hys : y ∈ s), a ≤ y → ∀ (hyx : y < x), Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x

Tactic:
rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩

Premises used: IsGLB.exists_between
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left : a ≤ y
hyx : y < x
refine_2 : ∃ (i : α) (_ : i ∈ s), x ∈ Ici i
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x

Tactic:
rw [mem_iUnion₂]

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left : a ≤ y
hyx : y < x
⊢ ∃ (i : α) (_ : i ∈ s), x ∈ Ici i

Tactic:
⟨y, hys, hyx.le⟩

Premises used: LT.lt.le, Exists.intro
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left : a ≤ y
hyx : y < x
⊢ ∃ (i : α) (_ : i ∈ s), x ∈ Ici i

Tactic:
exact ⟨y, hys, hyx.le⟩
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
⊢ ⋃ x ∈ s, Ici x = Ici a

Tactic:
(iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_

Premises used: Set.iUnion₂_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
refine_1 : ∀ (x : α) (hx : x ∈ s), Ici x ⊆ Ici a
refine_2 : ∀ (x : α) (hx : x ∈ Ici a), Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x
⊢ ⋃ x ∈ s, Ici x = Ici a

Tactic:
refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_

Premises used: Set.iUnion₂_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ici a

Tactic:
Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)

Premises used: Iff.mpr, mem_lowerBounds, Set.Ici_subset_Ici, And.left, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ici a

Tactic:
exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)

Premises used: Iff.mpr, mem_lowerBounds, Set.Ici_subset_Ici, And.left, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x

Tactic:
mem_iUnion₂.mpr ⟨a, a_mem, hx⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x

Tactic:
exact mem_iUnion₂.mpr ⟨a, a_mem, hx⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_lub : IsLUB s a
a_notMem : a ∉ s
⊢ ⋃ x ∈ s, Iic x = Iio a

Tactic:
a_lub.dual.biUnion_Ici_eq_Ioi a_notMem

Premises used: Set.Mem, setOf, Set.preimage, IsLUB.dual, Set.Iic, OrderDual, Set.Iio, IsGLB.biUnion_Ici_eq_Ioi
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_lub : IsLUB s a
a_mem : a ∈ s
⊢ ⋃ x ∈ s, Iic x = Iic a

Tactic:
a_lub.dual.biUnion_Ici_eq_Ici a_mem

Premises used: IsGLB.biUnion_Ici_eq_Ici, Set.Mem, setOf, Set.preimage, IsLUB.dual, Set.Iic, OrderDual