awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidablePred fun (x : α) ↦ b ≤ x
rw : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) ∅
⊢ filter (fun (x : α) ↦ b ≤ x) (Ico a b) = ∅

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_right_le]

Premises used: Finset.Ico_filter_le_of_right_le, Multiset.Ico, Finset.filter_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidablePred fun (x : α) ↦ b ≤ x
⊢ Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) ∅

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ c ≤ x
hac : a ≤ c
rw : (Finset.Ico c b).val = Ico c b
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico c b

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_left_le hac]

Premises used: Finset.Ico_filter_le_of_left_le, Multiset.Ico, Finset.filter_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ c ≤ x
hac : a ≤ c
⊢ (Finset.Ico c b).val = Ico c b

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Icc a a).val = {a}
rw₁ : Eq (α := Multiset α) (Finset.val {a}) {a}
rw₂ rw₃ : Eq (α := Multiset α) {a} {a}
⊢ Icc a a = {a}

Tactic:
rw [Icc, Finset.Icc_self, Finset.singleton_val]

Premises used: Multiset.Icc, Finset.singleton_val, Finset.Icc_self
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : (Finset.Icc a b).val = Icc a b
⊢ b ::ₘ Ico a b = Icc a b

Tactic:
rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]

Premises used: Finset.insert_val_of_notMem, Finset.Ico_insert_right, Multiset.right_notMem_Ico, Multiset.Ico
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ (Finset.Icc a b).val = Icc a b

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : b ::ₘ (Finset.Ico a b).val = Icc a b
rw₁ : (insert b (Finset.Ico a b)).val = Icc a b
rw₂ rw₃ rw₄ : (Finset.Icc a b).val = Icc a b
⊢ b ::ₘ Ico a b = Icc a b

Tactic:
classical
    rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]
    rfl

Premises used: Finset.insert_val_of_notMem, Multiset.right_notMem_Ico, Multiset.Ico
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
rw : (Finset.Ico a b).val = Ico a b
⊢ a ::ₘ Ioo a b = Ico a b

Tactic:
rw [Ioo, ← Finset.insert_val_of_notMem left_notMem_Ioo, Finset.Ioo_insert_left h]

Premises used: Multiset.left_notMem_Ioo, Finset.insert_val_of_notMem, Multiset.Ioo, Finset.Ioo_insert_left
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
⊢ (Finset.Ico a b).val = Ico a b

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
rw : a ::ₘ (Finset.Ioo a b).val = Ico a b
rw₁ : (insert a (Finset.Ioo a b)).val = Ico a b
rw₂ rw₃ rw₄ : (Finset.Ico a b).val = Ico a b
⊢ a ::ₘ Ioo a b = Ico a b

Tactic:
classical
    rw [Ioo, ← Finset.insert_val_of_notMem left_notMem_Ioo, Finset.Ioo_insert_left h]
    rfl

Premises used: Multiset.left_notMem_Ioo, Finset.insert_val_of_notMem, Multiset.Ioo
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a_1 : α
hab : a_1 ∈ Ico a b
hbc : a_1 ∈ Ico c d
⊢ a ≤ a_1 ∧ a_1 < b

Tactic:
rw [mem_Ico] at hab hbc

Premises used: Multiset.mem_Ico
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a_1 : α
hab : a_1 ∈ Ico a b
hbc : a_1 ∈ Ico c d
hab₁ : a ≤ a_1 ∧ a_1 < b
⊢ c ≤ a_1 ∧ a_1 < d

Tactic:
rw [mem_Ico] at hab hbc

Premises used: Multiset.mem_Ico
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a_1 : α
hab : a ≤ a_1 ∧ a_1 < b
hbc : c ≤ a_1 ∧ a_1 < d
⊢ False

Tactic:
hab.2.not_ge (h.trans hbc.1)

Premises used: And.right, And.left, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a_1 : α
hab : a ≤ a_1 ∧ a_1 < b
hbc : c ≤ a_1 ∧ a_1 < d
⊢ False

Tactic:
exact hab.2.not_ge (h.trans hbc.1)

Premises used: And.right, And.left, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
a b c d : α
h : b ≤ c
⊢ Ico a b ∩ Ico c d = 0

Tactic:
Multiset.inter_eq_zero_iff_disjoint.2 <| Ico_disjoint_Ico h

Premises used: Iff.mpr, Multiset.Ico_disjoint_Ico, Multiset.inter_eq_zero_iff_disjoint
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidablePred fun (x : α) ↦ x ≤ a
hab : a < b
rw : Eq (α := Multiset α) (Finset.val {a}) {a}
⊢ filter (fun (x : α) ↦ x ≤ a) (Ico a b) = {a}

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]

Premises used: Finset.Ico_filter_le_left, Multiset.Ico, Finset.filter_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidablePred fun (x : α) ↦ x ≤ a
hab : a < b
⊢ Eq (α := Multiset α) (Finset.val {a}) {a}

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Ico a b).card = (Icc a b).card - 1

Tactic:
Finset.card_Ico_eq_card_Icc_sub_one _ _

Premises used: Multiset.Icc, Multiset.Ico, Finset.card_Ico_eq_card_Icc_sub_one, Finset.card
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Ioc a b).card = (Icc a b).card - 1

Tactic:
Finset.card_Ioc_eq_card_Icc_sub_one _ _

Premises used: Multiset.Icc, Finset.card_Ioc_eq_card_Icc_sub_one, Finset.card, Multiset.Ioc
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Ioo a b).card = (Ico a b).card - 1

Tactic:
Finset.card_Ioo_eq_card_Ico_sub_one _ _

Premises used: Multiset.Ioo, Multiset.Ico, Finset.card_Ioo_eq_card_Ico_sub_one, Finset.card
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (Ioo a b).card = (Icc a b).card - 2

Tactic:
Finset.card_Ioo_eq_card_Icc_sub_two _ _

Premises used: Multiset.Icc, Finset.card_Ioo_eq_card_Icc_sub_two, Multiset.Ioo, Finset.card
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
Finset.Ico_subset_Ico_iff h

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.Ico, Finset.Ico_subset_Ico_iff, Multiset.Subset
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : Ico a b ∪ Ico b c = Ico a c
rw₁ : (Finset.Ico a b).val ∪ Ico b c = Ico a c
rw₂ : (Finset.Ico a b).val ∪ (Finset.Ico b c).val = Ico a c
rw₃ : (Finset.Ico a b).val ∪ (Finset.Ico b c).val = (Finset.Ico a c).val
rw₄ : (Finset.Ico a b ∪ Finset.Ico b c).val = (Finset.Ico a c).val
rw₅ rw₆ : (Finset.Ico a c).val = (Finset.Ico a c).val
⊢ Ico a b + Ico b c = Ico a c

Tactic:
rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]

Premises used: Iff.mpr, le_rfl, Multiset.add_eq_union_iff_disjoint, Finset.Ico_union_Ico_eq_Ico, Multiset.Ico, Multiset.Ico_disjoint_Ico, Finset.union_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (Finset.Ico a b).val ∩ Ico c d = Ico (max a c) (min b d)
rw₁ : (Finset.Ico a b).val ∩ (Finset.Ico c d).val = Ico (max a c) (min b d)
rw₂ : (Finset.Ico a b).val ∩ (Finset.Ico c d).val = (Finset.Ico (max a c) (min b d)).val
rw₃ : (Finset.Ico a b ∩ Finset.Ico c d).val = (Finset.Ico (max a c) (min b d)).val
rw₄ rw₅ : (Finset.Ico (max a c) (min b d)).val = (Finset.Ico (max a c) (min b d)).val
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)

Tactic:
rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]

Premises used: Finset.Ico_inter_Ico, Multiset.Ico, Finset.inter_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = Ico a (min b c)
rw₁ : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = (Finset.Ico a (min b c)).val
rw₂ : {x ∈ Finset.Ico a b | x < c}.val = (Finset.Ico a (min b c)).val
rw₃ rw₄ : (Finset.Ico a (min b c)).val = (Finset.Ico a (min b c)).val
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a (min b c)

Tactic:
rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_lt]

Premises used: Multiset.Ico, Finset.filter_val, Finset.Ico_filter_lt
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = Ico (max a c) b
rw₁ : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = (Finset.Ico (max a c) b).val
rw₂ : {x ∈ Finset.Ico a b | c ≤ x}.val = (Finset.Ico (max a c) b).val
rw₃ rw₄ : (Finset.Ico (max a c) b).val = (Finset.Ico (max a c) b).val
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico (max a c) b

Tactic:
rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]

Premises used: Multiset.Ico, Finset.Ico_filter_le, Finset.filter_val
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : (Finset.Ico a b).val - Ico a c = Ico (max a c) b
rw₁ : (Finset.Ico a b).val - (Finset.Ico a c).val = Ico (max a c) b
rw₂ : (Finset.Ico a b).val - (Finset.Ico a c).val = (Finset.Ico (max a c) b).val
rw₃ : (Finset.Ico a b \ Finset.Ico a c).val = (Finset.Ico (max a c) b).val
rw₄ rw₅ : (Finset.Ico (max a c) b).val = (Finset.Ico (max a c) b).val
⊢ Ico a b - Ico a c = Ico (max a c) b

Tactic:
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]

Premises used: Finset.sdiff_val, Finset.Ico_diff_Ico_left, Multiset.Ico
-- Module: Mathlib.Order.Interval.Multiset
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : (Finset.Ico a b).val - Ico c b = Ico a (min b c)
rw₁ : (Finset.Ico a b).val - (Finset.Ico c b).val = Ico a (min b c)
rw₂ : (Finset.Ico a b).val - (Finset.Ico c b).val = (Finset.Ico a (min b c)).val
rw₃ : (Finset.Ico a b \ Finset.Ico c b).val = (Finset.Ico a (min b c)).val
rw₄ rw₅ : (Finset.Ico a (min b c)).val = (Finset.Ico a (min b c)).val
⊢ Ico a b - Ico c b = Ico a (min b c)

Tactic:
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_right]

Premises used: Finset.sdiff_val, Multiset.Ico, Finset.Ico_diff_Ico_right
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst_1 : Decidable (x < b)
⊢ Decidable (x ∈ Iio b)

Tactic:
assumption
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst_1 : Decidable (x ≤ b)
⊢ Decidable (x ∈ Iic b)

Tactic:
assumption
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ ¬a ∈ Iio a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ a ∈ Iic a

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ ¬a ∈ Ioo a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ ¬a ∈ Ioc a b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a ∈ Ioo a b ↔ False

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a ∈ Ioc a b ↔ False

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a ∈ Ico a b ↔ a < b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a ∈ Icc a b ↔ a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ b ∈ Ioo a b ↔ False

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ b ∈ Ico a b ↔ False

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := Set αᵒᵈ) (Iio ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioi a : Set αᵒᵈ)

Tactic:
rfl

Premises used: Set.Ioi, Set.Mem, setOf, Set.preimage, Set.Iio, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := Set αᵒᵈ) (Iic ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Ici a : Set αᵒᵈ)

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.preimage, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Eq (α := Set αᵒᵈ) (Icc ((toDual : (a : α) → αᵒᵈ) a) ((toDual : (a : α) → αᵒᵈ) b) : Set αᵒᵈ)
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc b a : Set αᵒᵈ)

Tactic:
Set.ext fun _ => and_comm

Premises used: Set.ext, and_comm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Eq (α := Set αᵒᵈ) (Ico ((toDual : (a : α) → αᵒᵈ) a) ((toDual : (a : α) → αᵒᵈ) b) : Set αᵒᵈ)
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc b a : Set αᵒᵈ)

Tactic:
Set.ext fun _ => and_comm

Premises used: Set.ext, and_comm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Eq (α := Set αᵒᵈ) (Ioo ((toDual : (a : α) → αᵒᵈ) a) ((toDual : (a : α) → αᵒᵈ) b) : Set αᵒᵈ)
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioo b a : Set αᵒᵈ)

Tactic:
Set.ext fun _ => and_comm

Premises used: Set.ext, and_comm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
x : αᵒᵈ
⊢ Eq (α := Set α) (Iio ((ofDual : (a : αᵒᵈ) → α) x) : Set α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' Ioi x : Set α)

Tactic:
rfl

Premises used: Set.Ioi, Set.Mem, setOf, Set.preimage, Set.Iio, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
x : αᵒᵈ
⊢ Eq (α := Set α) (Iic ((ofDual : (a : αᵒᵈ) → α) x) : Set α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' Ici x : Set α)

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.preimage, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
x y : αᵒᵈ
⊢ Eq (α := Set α) (Icc ((ofDual : (a : αᵒᵈ) → α) y) ((ofDual : (a : αᵒᵈ) → α) x) : Set α)
    ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' Icc x y : Set α)

Tactic:
Set.ext fun _ => and_comm

Premises used: Set.ext, and_comm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
x y : αᵒᵈ
⊢ Eq (α := Set α) (Ico ((ofDual : (a : αᵒᵈ) → α) y) ((ofDual : (a : αᵒᵈ) → α) x) : Set α)
    ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' Ioc x y : Set α)

Tactic:
Set.ext fun _ => and_comm

Premises used: Set.ext, and_comm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
x y : αᵒᵈ
⊢ Eq (α := Set α) (Ioo ((ofDual : (a : αᵒᵈ) → α) y) ((ofDual : (a : αᵒᵈ) → α) x) : Set α)
    ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' Ioo x y : Set α)

Tactic:
Set.ext fun _ => and_comm

Premises used: Set.ext, and_comm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
inst_1 : NoMinOrder α
⊢ (Iio a).Nonempty

Tactic:
exists_lt a

Premises used: Set.Mem, setOf, Set.Nonempty, NoMinOrder.exists_lt, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (Iic a).Nonempty

Tactic:
⟨a, self_mem_Iic⟩

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

Tactic:
⟨fun ⟨_, hx⟩ => hx.1.trans hx.2, fun h => ⟨a, left_mem_Icc.2 h⟩⟩

Premises used: Iff.mpr, LE.le, And.right, And.left, Set.left_mem_Icc, _private.0.Set.nonempty_Icc.match_1, Iff.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (Ico a b).Nonempty ↔ a < b

Tactic:
⟨fun ⟨_, hx⟩ => hx.1.trans_lt hx.2, fun h => ⟨a, left_mem_Ico.2 h⟩⟩

Premises used: Iff.mpr, _private.0.Set.nonempty_Ico.match_1, Set.left_mem_Ico, And.right, And.left, LT.lt, Iff.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
inst_1 : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b

Tactic:
⟨fun ⟨_, ha, hb⟩ => ha.trans hb, exists_between⟩

Premises used: exists_between, _private.0.Set.nonempty_Ioo.match_1, LT.lt, Iff.intro, LT.lt.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst_1 : NoMinOrder α
⊢ Nonempty.{u_1 + 1} (↑(Iio a) : Type u_1)

Tactic:
Nonempty.to_subtype nonempty_Iio

Premises used: Set.Nonempty.to_subtype, Set.nonempty_Iio
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Nonempty.{u_1 + 1} (↑(Iic a) : Type u_1)

Tactic:
Nonempty.to_subtype nonempty_Iic

Premises used: Set.Nonempty.to_subtype, Set.nonempty_Iic
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ Nonempty.{u_1 + 1} (↑(Icc a b) : Type u_1)

Tactic:
Nonempty.to_subtype (nonempty_Icc.mpr h)

Premises used: Iff.mpr, Set.Nonempty.to_subtype, Set.nonempty_Icc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ Nonempty.{u_1 + 1} (↑(Ioc a b) : Type u_1)

Tactic:
Nonempty.to_subtype (nonempty_Ioc.mpr h)

Premises used: Iff.mpr, Set.nonempty_Ioc, Set.Nonempty.to_subtype
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
inst_1 : DenselyOrdered α
h : a < b
⊢ Nonempty.{u_1 + 1} (↑(Ioo a b) : Type u_1)

Tactic:
Nonempty.to_subtype (nonempty_Ioo.mpr h)

Premises used: Iff.mpr, Set.Nonempty.to_subtype, Set.nonempty_Ioo
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : One α
inst_2 : IsBotOneClass α
h : ∀ (x : α), Membership.mem (γ := Set α) (Iio 1) x ↔ Membership.mem (γ := Set α) ∅ x
⊢ Eq.{u_1 + 1} (α := Set α) (Iio 1) ∅

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : One α
inst_2 : IsBotOneClass α
x : α
⊢ Membership.mem (γ := Set α) (Iio 1) x ↔ Membership.mem (γ := Set α) ∅ x

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst_1 : One α
inst_2 : IsBotOneClass α
⊢ IsEmpty.{u_1 + 1} (↑(Iio 1) : Type u_1)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst_1 : NoMinOrder α
⊢ NoMinOrder.{u_1} (↑(Iio a) : Type u_1)

Tactic:
⟨fun a =>
    let ⟨b, hb⟩ := exists_lt (a : α)
    ⟨⟨b, lt_trans hb a.2⟩, hb⟩⟩

Premises used: lt_trans, Exists, NoMinOrder.mk, Subtype.mk, _private.0.Set.instNoMinOrderElemIio.match_1, LT.lt, Exists.intro, NoMinOrder.exists_lt, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst_1 : NoMinOrder α
⊢ NoMinOrder.{u_1} (↑(Iic a) : Type u_1)

Tactic:
⟨fun a =>
    let ⟨b, hb⟩ := exists_lt (a : α)
    ⟨⟨b, hb.le.trans a.2⟩, hb⟩⟩

Premises used: Exists, LT.lt.le, NoMinOrder.mk, Subtype.mk, LT.lt, Exists.intro, NoMinOrder.exists_lt, _private.0.Set.instNoMinOrderElemIic.match_1, LE.le.trans, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a ≤ b
⊢ Icc a b = ∅

Tactic:
eq_empty_iff_forall_notMem.2 fun _ ⟨ha, hb⟩ => h (ha.trans hb)

Premises used: Iff.mpr, False, _private.0.Set.Icc_eq_empty.match_1, Set.eq_empty_iff_forall_notMem, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a < b
⊢ Ico a b = ∅

Tactic:
eq_empty_iff_forall_notMem.2 fun _ hab => h (hab.1.trans_lt hab.2)

Premises used: Iff.mpr, And.right, And.left, Set.eq_empty_iff_forall_notMem, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a < b
⊢ Ioo a b = ∅

Tactic:
eq_empty_iff_forall_notMem.2 fun _ ⟨ha, hb⟩ => h (ha.trans hb)

Premises used: Iff.mpr, _private.0.Set.Ioo_eq_empty.match_1, False, Set.eq_empty_iff_forall_notMem, LT.lt.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : b < a
⊢ Icc a b = ∅

Tactic:
Icc_eq_empty h.not_ge

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

Tactic:
Ico_eq_empty h.not_gt

Premises used: LE.le.not_gt, Set.Ico_eq_empty
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : b ≤ a
⊢ Ioo a b = ∅

Tactic:
Ioo_eq_empty h.not_gt

Premises used: LE.le.not_gt, Set.Ioo_eq_empty
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Ico a a = ∅

Tactic:
Ico_eq_empty <| lt_irrefl _

Premises used: lt_irrefl, Set.Ico_eq_empty
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Ioo a a = ∅

Tactic:
Ioo_eq_empty <| lt_irrefl _

Premises used: lt_irrefl, Set.Ioo_eq_empty
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ Iio a ⊆ Iio b

Tactic:
fun _ hx => lt_of_lt_of_le hx h

Premises used: Set.Mem, setOf, Set.Subset, Set.Iio, lt_of_lt_of_le
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ Iio a ⊂ Iio b

Tactic:
(ssubset_iff_of_subset (Iio_subset_Iio h.le)).mpr ⟨a, h, lt_irrefl a⟩

Premises used: Iff.mpr, lt_irrefl, LT.lt.le, Set.Iio_subset_Iio, And.intro, Exists.intro, Set.ssubset_iff_of_subset
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Iic a ⊆ Iic b ↔ a ≤ b

Tactic:
⟨fun h => h self_mem_Ici, fun h _ hx ↦ hx.trans h⟩

Premises used: Iff.intro, LE.le.trans, Set.self_mem_Ici
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : Iic a ⊂ Iic b
obtain : ∀ (ab : Iic a ⊆ Iic b) (c : α) (cb : c ∈ Iic b) (ac : ¬c ∈ Iic a), a < b
⊢ a < b

Tactic:
obtain ⟨ab, c, cb, ac⟩ := ssubset_iff_exists.mp h

Premises used: Set.ssubset_iff_exists, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : Iic a ⊂ Iic b
ab : Iic a ⊆ Iic b
c : α
cb : c ∈ Iic b
ac : ¬c ∈ Iic a
⊢ a < b

Tactic:
lt_of_le_not_ge (Iic_subset_Iic.mp ab) (fun h' ↦ ac (cb.trans h'))

Premises used: Set.Iic_subset_Iic, lt_of_le_not_ge, Iff.mp, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : Iic a ⊂ Iic b
ab : Iic a ⊆ Iic b
c : α
cb : c ∈ Iic b
ac : ¬c ∈ Iic a
⊢ a < b

Tactic:
exact lt_of_le_not_ge (Iic_subset_Iic.mp ab) (fun h' ↦ ac (cb.trans h'))

Premises used: Set.Iic_subset_Iic, lt_of_le_not_ge, Iff.mp, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Iic a ⊆ Iio b ↔ a < b

Tactic:
⟨fun h => h self_mem_Iic, fun h _ hx => lt_of_le_of_lt hx h⟩

Premises used: lt_of_le_of_lt, Set.self_mem_Iic, Iff.intro
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Iio a ⊆ Iic a

Tactic:
fun _ hx => le_of_lt hx

Premises used: Set.Mem, setOf, le_of_lt, Set.Subset, Set.Iic