awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a < b
rw : {a} ∪ Ioo a b = Ico a b
rw₁ : Ioo a b ∪ {a} = Ico a b
rw₂ rw₃ : Ico a b = Ico a b
⊢ insert a (Ioo a b) = Ico a b

Tactic:
rw [insert_eq, union_comm, Ioo_union_left h]

Premises used: Set.insert_eq, Set.Ioo_union_left, Set.union_comm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ insert a (Iio a) = Iic a

Tactic:
ext fun _ => le_iff_eq_or_lt.symm

Premises used: le_iff_eq_or_lt, Set.ext, Iff.symm
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
rw : Iio a ⊆ s ∧ {a} ⊆ s
⊢ Iic a ⊆ s

Tactic:
rw [← Iio_union_right, union_subset_iff]

Premises used: Set.union_subset_iff, Set.Iio_union_right
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iio a ⊆ s ∧ {a} ⊆ s

Tactic:
simp [*]
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
pos : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
pos : ∀ (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg : ∀ (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
by_cases hb : b ∈ s
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
pos : ∀ (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg : ∀ (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
by_cases hb : b ∈ s
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
Or.inl (Subset.antisymm hc ?_)

Premises used: Set.Subset.antisymm, Set.insert, Set.Mem, setOf, Or.inl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
pos : Icc a b ⊆ s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
refine Or.inl (Subset.antisymm hc ?_)

Premises used: Set.Subset.antisymm, Or.inl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
pos : ∀ (ho : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₁ : ∀ (ho : Ico a b ⊆ insert a s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₂ : ∀ (ho : Ico a b ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₃ : ∀ (ho : Icc a b \ {b} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₄ : ∀ (ho : Icc a b ⊆ insert b s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₅ pos₆ pos₇ pos₈ : ∀ (ho : Icc a b ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
⊢ Icc a b ⊆ s

Tactic:
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
        diff_singleton_subset_iff, insert_eq_of_mem hb] at ho

Premises used: Set.diff_singleton_subset_iff, Set.insert_eq_of_mem, Set.Icc_diff_right, Set.Ico_diff_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
Or.inr <| Or.inl <| Subset.antisymm ?_ ?_

Premises used: Set.Subset.antisymm, Set.insert, Set.Mem, setOf, Or.inl, Or.inr
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
neg : s ⊆ Ico a b
neg₁ : Ico a b ⊆ s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_

Premises used: Set.Subset.antisymm, Or.inl, Or.inr
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
neg : s ⊆ Icc a b \ {b}
⊢ s ⊆ Ico a b

Tactic:
rw [← Icc_diff_right]

Premises used: Set.Icc_diff_right
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Icc a b \ {b}

Tactic:
subset_diff_singleton hc hb

Premises used: Set.subset_diff_singleton
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Icc a b \ {b}

Tactic:
exact subset_diff_singleton hc hb

Premises used: Set.subset_diff_singleton
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
neg : ∀ (ho : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : ¬b ∈ s), Ico a b ⊆ s
neg₁ : ∀ (ho : Ico a b ⊆ insert a s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : ¬b ∈ s), Ico a b ⊆ s
neg₂ neg₃ neg₄ neg₅ : ∀ (ho : Ico a b ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : ¬b ∈ s), Ico a b ⊆ s
⊢ Ico a b ⊆ s

Tactic:
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho

Premises used: Set.diff_singleton_subset_iff, Set.insert_eq_of_mem, Set.Ico_diff_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_

Premises used: Set.Subset.antisymm, Set.insert, Set.Mem, setOf, Or.inl, Or.inr
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
pos : s ⊆ Ioc a b
pos₁ : Ioc a b ⊆ s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_

Premises used: Set.Subset.antisymm, Or.inl, Or.inr
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
pos : s ⊆ Icc a b \ {a}
⊢ s ⊆ Ioc a b

Tactic:
rw [← Icc_diff_left]

Premises used: Set.Icc_diff_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}

Tactic:
subset_diff_singleton hc ha

Premises used: Set.subset_diff_singleton
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}

Tactic:
exact subset_diff_singleton hc ha

Premises used: Set.subset_diff_singleton
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
pos : ∀ (ho : Ioc a b \ {b} ⊆ s) (hc : s ⊆ Icc a b) (ha : ¬a ∈ s) (hb : b ∈ s), Ioc a b ⊆ s
pos₁ : ∀ (ho : Ioc a b ⊆ insert b s) (hc : s ⊆ Icc a b) (ha : ¬a ∈ s) (hb : b ∈ s), Ioc a b ⊆ s
pos₂ pos₃ pos₄ pos₅ : ∀ (ho : Ioc a b ⊆ s) (hc : s ⊆ Icc a b) (ha : ¬a ∈ s) (hb : b ∈ s), Ioc a b ⊆ s
⊢ Ioc a b ⊆ s

Tactic:
rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho

Premises used: Set.diff_singleton_subset_iff, Set.insert_eq_of_mem, Set.Ioc_diff_right
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho

Premises used: Set.Subset.antisymm, Set.insert, Set.Mem, setOf, Or.inr
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
neg : s ⊆ Ioo a b
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho

Premises used: Set.Subset.antisymm, Or.inr
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
neg : s ⊆ (Icc a b \ {b}) \ {a}
⊢ s ⊆ Ioo a b

Tactic:
rw [← Ico_diff_left, ← Icc_diff_right]

Premises used: Set.Icc_diff_right, Set.Ico_diff_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ (Icc a b \ {b}) \ {a}

Tactic:
apply_rules [subset_diff_singleton]

Premises used: Set.subset_diff_singleton
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
pos : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₁ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₁ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₂ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₂ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₃ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₃ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₄ : ∀ (ha : a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₄ : ∀ (ha : a ∈ s) (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₅ : ∀ (ha : ¬a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₅ : ∀ (ha : ¬a ∈ s) (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₆ : ∀ (ha : a ∈ s) (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₆ : ∀ (ha : ¬a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₇ : ∀ (ha : ¬a ∈ s) (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₇ : ∀ (ha : ¬a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₈ neg₉ : ∀ (ha : ¬a ∈ s) (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s

Tactic:
classical
    by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
    · refine Or.inl (Subset.antisymm hc ?_)
      rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
        diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_right]
        exact subset_diff_singleton hc hb
      · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
    · refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_left]
        exact subset_diff_singleton hc ha
      · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
      rw [← Ico_diff_left, ← Icc_diff_right]
      apply_rules [subset_diff_singleton]

Premises used: Set.Subset.antisymm, Set.diff_singleton_subset_iff, Set.Icc_diff_left, Set.Ioc_diff_right, Set.Icc_diff_right, Set.subset_diff_singleton, Or.inl, Or.inr, Set.Ico_diff_left
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b x : α
hmem : x ∈ Ico a b
⊢ x = a ∨ x ∈ Ioo a b

Tactic:
hmem.1.eq_or_lt'.imp_right fun h => ⟨h, hmem.2⟩

Premises used: And.right, And.left, And.intro, LE.le.eq_or_lt', Or.imp_right
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b x : α
hmem : x ∈ Icc a b
⊢ x = a ∨ x = b ∨ x ∈ Ioo a b

Tactic:
hmem.1.eq_or_lt'.imp_right fun h => eq_right_or_mem_Ioo_of_mem_Ioc ⟨h, hmem.2⟩

Premises used: Set.eq_right_or_mem_Ioo_of_mem_Ioc, And.right, And.left, And.intro, LE.le.eq_or_lt', Or.imp_right
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
h : IsMin a
⊢ Iic a = {a}

Tactic:
eq_singleton_iff_unique_mem.2 ⟨self_mem_Ici, fun _ => h.eq_of_le⟩

Premises used: Iff.mpr, And.intro, Set.eq_singleton_iff_unique_mem, IsMin.eq_of_le, Set.self_mem_Ici
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) Iic

Tactic:
fun _ _ =>
  eq_of_forall_le_iff ∘ Set.ext_iff.1

Premises used: Function.comp, Iff.mp, Set.ext_iff, Function.Injective, eq_of_forall_le_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ Iic a = Iic b ↔ a = b

Tactic:
Iic_injective.eq_iff

Premises used: Function.Injective.eq_iff, Set.Iic_injective
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : Ici a ∩ Iic c ∩ Icc b b = {b}
⊢ Icc a b ∩ Icc b c = {b}

Tactic:
rw [← Ici_inter_Iic, ← Iic_inter_Ici, inter_inter_inter_comm, Iic_inter_Ici]

Premises used: Set.inter_inter_inter_comm, Set.Iic_inter_Ici, Set.Ici_inter_Iic
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ici a ∩ Iic c ∩ Icc b b = {b}

Tactic:
simp [hab, hbc]
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
refine : ∀ (heq : Icc a b = Icc c d), a = c ∧ b = d
⊢ Icc a b = Icc c d ↔ a = c ∧ b = d

Tactic:
refine ⟨fun heq ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
by_contra : ∀ (contra : ¬c ≤ d), False
⊢ c ≤ d

Tactic:
by_contra contra
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
contra : ¬c ≤ d
⊢ ¬a ≤ b

Tactic:
rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq

Premises used: Iff.mpr, Set.Icc_eq_empty_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
contra : ¬c ≤ d
heq₁ : ¬a ≤ b
⊢ ¬c ≤ d

Tactic:
rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq

Premises used: Iff.mpr, Set.Icc_eq_empty_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : ¬a ≤ b
contra : ¬c ≤ d
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
⊢ c ≤ d

Tactic:
have h' : c ≤ d := by
    by_contra contra; rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq; contradiction
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
h' : c ≤ d
⊢ ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d

Tactic:
simp only [Set.ext_iff, mem_Icc] at heq

Premises used: Set.mem_Icc, Set.ext_iff
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
⊢ b ≤ d

Tactic:
obtain ⟨-, h₁⟩ := (heq b).mp ⟨h, le_refl _⟩

Premises used: le_refl, And.intro, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
⊢ c ≤ a

Tactic:
obtain ⟨h₂, -⟩ := (heq a).mp ⟨le_refl _, h⟩

Premises used: le_refl, And.intro, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ a ≤ c

Tactic:
obtain ⟨h₃, -⟩ := (heq c).mpr ⟨le_refl _, h'⟩

Premises used: Iff.mpr, le_refl, And.intro
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
h₃ : a ≤ c
⊢ d ≤ b

Tactic:
obtain ⟨-, h₄⟩ := (heq d).mpr ⟨h', le_refl _⟩

Premises used: Iff.mpr, le_refl, And.intro
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
h₃ : a ≤ c
h₄ : d ≤ b
⊢ a = c ∧ b = d

Tactic:
⟨le_antisymm h₃ h₂, le_antisymm h₁ h₄⟩

Premises used: le_antisymm, And.intro
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
h₃ : a ≤ c
h₄ : d ≤ b
⊢ a = c ∧ b = d

Tactic:
exact ⟨le_antisymm h₃ h₂, le_antisymm h₁ h₄⟩
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
⊢ Eq (α := Set α) (Ici ⊤) {⊤}

Tactic:
isMax_top.Ici_eq

Premises used: isMax_top, IsMax.Ici_eq
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
⊢ Eq (α := Set α) (Iio ⊤) {⊤}ᶜ

Tactic:
ext fun _ ↦ lt_top_iff_ne_top

Premises used: Set.ext, lt_top_iff_ne_top
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ Eq.{u_1 + 1} (α := Set α) (Ioi ⊤) ∅

Tactic:
isMax_top.Ioi_eq

Premises used: isMax_top, IsMax.Ioi_eq
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ Eq.{u_1 + 1} (α := Set α) (Iic ⊤) univ

Tactic:
isTop_top.Iic_eq

Premises used: IsTop.Iic_eq, isTop_top
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ Icc a ⊤ = Ici a

Tactic:
simp [← Ici_inter_Iic]

Premises used: Set.Ici_inter_Iic
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ Ioc a ⊤ = Ioi a

Tactic:
simp [← Ioi_inter_Iic]

Premises used: Set.Ioi_inter_Iic
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : BoundedOrder α
⊢ Eq.{u_1 + 1} (α := Set α) (Icc ⊥ ⊤) univ

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : SemilatticeInf α
a b : α
h : ∀ (x : α), x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : SemilatticeInf α
a b x : α
⊢ x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)

Tactic:
simp [Iic]

Premises used: Set.Iic
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : SemilatticeInf α
a b c : α
rw : Ioi a ∩ Iic b ∩ Iic c = Ioc a (b ⊓ c)
rw₁ : Ioi a ∩ Iic b ∩ Iic c = Ioi a ∩ Iic (b ⊓ c)
rw₂ : Ioi a ∩ (Iic b ∩ Iic c) = Ioi a ∩ Iic (b ⊓ c)
rw₃ rw₄ : Ioi a ∩ Iic (b ⊓ c) = Ioi a ∩ Iic (b ⊓ c)
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]

Premises used: Set.Ioi_inter_Iic, Set.Iic_inter_Iic, Set.inter_assoc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Lattice α
a₁ a₂ b₁ b₂ : α
simp : Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]

Premises used: Set.Iic_inter_Iic, Set.Ici_inter_Ici, Eq.symm, Set.Ici_inter_Iic
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
inst : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)

Tactic:
ac_rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
⊢ Iic a ×ˢ Iic b = Iic (a, b)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α × β
⊢ Iic a = Iic a.1 ×ˢ Iic a.2

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h : ∀ (x : α) (y : β), (x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)
⊢ Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
x : α
y : β
⊢ (x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)

Tactic:
simp [and_assoc, and_left_comm]

Premises used: and_left_comm, and_assoc
-- Module: Mathlib.Order.Interval.Set.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α × β
⊢ Icc a b = Icc a.1 b.1 ×ˢ Icc a.2 b.2

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

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

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

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

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

Tactic:
exact ⟨⟨b, mem_Ioo.mpr ⟨hb₁, hb₂.trans ha.2⟩⟩, hb₂⟩
-- 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
rcases :
  ∀ (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
⊢ ∃ (b : (↑(Ioc x y) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioc x y) a ha

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

Premises used: exists_between, And.left