awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
c : α
bc : b < c
ca : c < a
⊢ False

Tactic:
exact lt_irrefl _ (ca.trans_le (h bc))

Premises used: lt_irrefl, LT.lt.trans_le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Iic b ∪ Ioi a = univ

Tactic:
eq_univ_of_forall fun x => (h.gt_or_le x).symm

Premises used: Or.symm, LE.le.gt_or_le, Set.eq_univ_of_forall
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Iio b ∪ Ici a = univ

Tactic:
eq_univ_of_forall fun x => (h.ge_or_lt x).symm

Premises used: Or.symm, Set.eq_univ_of_forall, LE.le.ge_or_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Iic b ∪ Ici a = univ

Tactic:
eq_univ_of_forall fun x => (h.ge_or_le x).symm

Premises used: LE.le.ge_or_le, Or.symm, Set.eq_univ_of_forall
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ Iio b ∪ Ioi a = univ

Tactic:
eq_univ_of_forall fun x => (h.gt_or_lt x).symm

Premises used: LT.lt.gt_or_lt, Or.symm, Set.eq_univ_of_forall
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Iic a ∪ Ici a = univ

Tactic:
Iic_union_Ici_of_le le_rfl

Premises used: le_rfl, Set.Iic_union_Ici_of_le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Iio a ∪ Ici a = univ

Tactic:
Iio_union_Ici_of_le le_rfl

Premises used: le_rfl, Set.Iio_union_Ici_of_le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Iic a ∪ Ioi a = univ

Tactic:
Iic_union_Ioi_of_le le_rfl

Premises used: le_rfl, Set.Iic_union_Ioi_of_le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Iio a ∪ Ioi a = {a}ᶜ

Tactic:
ext fun _ => lt_or_lt_iff_ne

Premises used: Set.ext, lt_or_lt_iff_ne
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : c < max a b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c < b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)

Tactic:
Ioo_union_Ioi (h₁.trans_le (le_max_right ..))

Premises used: le_max_right, Set.Ioo_union_Ioi, LT.lt.trans_le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi a ⊆ Ioo a b ∪ Ici b

Tactic:
fun x hx =>
  (lt_or_ge x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

Premises used: Set.Subset, And.intro, Or.inl, lt_or_ge, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ Ioo a b ∪ Ici b = Ioi a

Tactic:
Subset.antisymm (fun _ hx => hx.elim And.left h.trans_le) Ioi_subset_Ioo_union_Ici

Premises used: Set.Subset.antisymm, Set.Ioi_subset_Ioo_union_Ici, And.left, LT.lt.trans_le, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ici a ⊆ Ico a b ∪ Ici b

Tactic:
fun x hx =>
  (lt_or_ge x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

Premises used: Set.Subset, And.intro, Or.inl, lt_or_ge, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Ico a b ∪ Ici b = Ici a

Tactic:
Subset.antisymm (fun _ hx => hx.elim And.left h.trans) Ici_subset_Ico_union_Ici

Premises used: Set.Subset.antisymm, And.left, Set.Ici_subset_Ico_union_Ici, LE.le.trans, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : c ≤ max a b
⊢ Ico a b ∪ Ici c = Ici (min a c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (min a c)

Tactic:
Ico_union_Ici (h₁.trans (le_max_right ..))

Premises used: le_max_right, LE.le.trans, Set.Ico_union_Ici
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi a ⊆ Ioc a b ∪ Ioi b

Tactic:
fun x hx =>
  (le_or_gt x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

Premises used: Set.Subset, le_or_gt, And.intro, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Ioc a b ∪ Ioi b = Ioi a

Tactic:
Subset.antisymm (fun _ hx => hx.elim And.left h.trans_lt) Ioi_subset_Ioc_union_Ioi

Premises used: Set.Subset.antisymm, Set.Ioi_subset_Ioc_union_Ioi, And.left, Or.elim, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : c ≤ max a b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)

Tactic:
Ioc_union_Ioi (h₁.trans (le_max_right ..))

Premises used: le_max_right, Set.Ioc_union_Ioi, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ici a ⊆ Icc a b ∪ Ioi b

Tactic:
fun x hx =>
  (le_or_gt x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

Premises used: Set.Subset, le_or_gt, And.intro, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Icc a b ∪ Ioi b = Ici a

Tactic:
Subset.antisymm (fun _ hx => (hx.elim And.left) fun hx' => h.trans <| le_of_lt hx')
    Ici_subset_Icc_union_Ioi

Premises used: Set.Subset.antisymm, le_of_lt, And.left, Set.Ici_subset_Icc_union_Ioi, LE.le.trans, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi a ⊆ Ioc a b ∪ Ici b

Tactic:
Subset.trans Ioi_subset_Ioo_union_Ici (union_subset_union_left _ Ioo_subset_Ioc_self)

Premises used: Set.Ioi_subset_Ioo_union_Ici, Set.Subset.trans, Set.Ioo_subset_Ioc_self, Set.union_subset_union_left
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ Ioc a b ∪ Ici b = Ioi a

Tactic:
Subset.antisymm (fun _ hx => hx.elim And.left h.trans_le) Ioi_subset_Ioc_union_Ici

Premises used: Set.Subset.antisymm, And.left, LT.lt.trans_le, Or.elim, Set.Ioi_subset_Ioc_union_Ici
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ici a ⊆ Icc a b ∪ Ici b

Tactic:
Subset.trans Ici_subset_Ico_union_Ici (union_subset_union_left _ Ico_subset_Icc_self)

Premises used: Set.Ico_subset_Icc_self, Set.Subset.trans, Set.Ici_subset_Ico_union_Ici, Set.union_subset_union_left
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Icc a b ∪ Ici b = Ici a

Tactic:
Subset.antisymm (fun _ hx => hx.elim And.left h.trans) Ici_subset_Icc_union_Ici

Premises used: Set.Subset.antisymm, Set.Ici_subset_Icc_union_Ici, And.left, LE.le.trans, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : c ≤ max a b
⊢ Icc a b ∪ Ici c = Ici (min a c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)

Tactic:
Icc_union_Ici (h₁.trans (le_max_right ..))

Premises used: le_max_right, Set.Icc_union_Ici, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Iic b ⊆ Iio a ∪ Icc a b

Tactic:
fun x hx =>
  (lt_or_ge x a).elim (fun hxa => Or.inl hxa) fun hxa => Or.inr ⟨hxa, hx⟩

Premises used: Set.Subset, And.intro, Or.inl, lt_or_ge, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Iio a ∪ Icc a b = Iic b

Tactic:
Subset.antisymm (fun _ hx => hx.elim (fun hx => (le_of_lt hx).trans h) And.right)
    Iic_subset_Iio_union_Icc

Premises used: Set.Subset.antisymm, le_of_lt, And.right, LE.le.trans, Set.Iic_subset_Iio_union_Icc, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Iio b ⊆ Iio a ∪ Ico a b

Tactic:
fun x hx =>
  (lt_or_ge x a).elim (fun hxa => Or.inl hxa) fun hxa => Or.inr ⟨hxa, hx⟩

Premises used: Set.Subset, And.intro, Or.inl, lt_or_ge, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Iio a ∪ Ico a b = Iio b

Tactic:
Subset.antisymm (fun _ hx => hx.elim (fun hx' => lt_of_lt_of_le hx' h) And.right)
    Iio_subset_Iio_union_Ico

Premises used: Set.Subset.antisymm, And.right, Set.Iio_subset_Iio_union_Ico, Or.elim, lt_of_lt_of_le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
b c d : α
h : min c d ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
b c d : α
h₁ : c ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)

Tactic:
Iio_union_Ico ((min_le_left ..).trans h₁)

Premises used: Set.Iio_union_Ico, min_le_left, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Iic b ⊆ Iic a ∪ Ioc a b

Tactic:
fun x hx =>
  (le_or_gt x a).elim (fun hxa => Or.inl hxa) fun hxa => Or.inr ⟨hxa, hx⟩

Premises used: Set.Subset, le_or_gt, And.intro, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Iic a ∪ Ioc a b = Iic b

Tactic:
Subset.antisymm (fun _ hx => hx.elim (fun hx' => le_trans hx' h) And.right)
    Iic_subset_Iic_union_Ioc

Premises used: Set.Subset.antisymm, Set.Iic_subset_Iic_union_Ioc, And.right, Or.elim, le_trans
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
b c d : α
h : min c d < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
b c d : α
h₁ : c < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)

Tactic:
Iic_union_Ioc ((min_le_left ..).trans_lt h₁)

Premises used: Set.Iic_union_Ioc, min_le_left, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Iio b ⊆ Iic a ∪ Ioo a b

Tactic:
fun x hx =>
  (le_or_gt x a).elim (fun hxa => Or.inl hxa) fun hxa => Or.inr ⟨hxa, hx⟩

Premises used: Set.Subset, le_or_gt, And.intro, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ Iic a ∪ Ioo a b = Iio b

Tactic:
Subset.antisymm (fun _ hx => hx.elim (fun hx' => lt_of_le_of_lt hx' h) And.right)
    Iio_subset_Iic_union_Ioo

Premises used: Set.Subset.antisymm, lt_of_le_of_lt, And.right, Or.elim, Set.Iio_subset_Iic_union_Ioo
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
b c d : α
h : min c d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
b c d : α
h₁ : c < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)

Tactic:
Iio_union_Ioo ((min_le_left ..).trans_lt h₁)

Premises used: Set.Iio_union_Ioo, min_le_left, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Iic b ⊆ Iic a ∪ Icc a b

Tactic:
Subset.trans Iic_subset_Iic_union_Ioc (union_subset_union_right _ Ioc_subset_Icc_self)

Premises used: Set.Subset.trans, Set.Ioc_subset_Icc_self, Set.union_subset_union_right, Set.Iic_subset_Iic_union_Ioc
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ Iic a ∪ Icc a b = Iic b

Tactic:
Subset.antisymm (fun _ hx => hx.elim (fun hx' => le_trans hx' h) And.right)
    Iic_subset_Iic_union_Icc

Premises used: Set.Subset.antisymm, Set.Iic_subset_Iic_union_Icc, And.right, Or.elim, le_trans
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
b c d : α
h : min c d ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
b c d : α
h₁ : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)

Tactic:
Iic_union_Icc ((min_le_left ..).trans h₁)

Premises used: min_le_left, Set.Iic_union_Icc, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Iio b ⊆ Iic a ∪ Ico a b

Tactic:
Subset.trans Iio_subset_Iic_union_Ioo (union_subset_union_right _ Ioo_subset_Ico_self)

Premises used: Set.Subset.trans, Set.union_subset_union_right, Set.Ioo_subset_Ico_self, Set.Iio_subset_Iic_union_Ioo
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ Iic a ∪ Ico a b = Iio b

Tactic:
Subset.antisymm (fun _ hx => hx.elim (fun hx' => lt_of_le_of_lt hx' h) And.right)
    Iio_subset_Iic_union_Ico

Premises used: Set.Subset.antisymm, lt_of_le_of_lt, And.right, Set.Iio_subset_Iic_union_Ico, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioo a c ⊆ Ioo a b ∪ Ico b c

Tactic:
fun x hx =>
  (lt_or_ge x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Premises used: Set.Subset, And.right, And.left, And.intro, Or.inl, lt_or_ge, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a < b
h₂ : b ≤ c
⊢ Ioo a b ∪ Ico b c = Ioo a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_le h₂⟩) fun hx => ⟨h₁.trans_le hx.1, hx.2⟩)
    Ioo_subset_Ioo_union_Ico

Premises used: Set.Ioo_subset_Ioo_union_Ico, Set.Subset.antisymm, And.right, And.left, LT.lt.trans_le, And.intro, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c

Tactic:
fun x hx =>
  (lt_or_ge x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Premises used: Set.Subset, And.right, And.left, And.intro, Or.inl, lt_or_ge, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ico a b ∪ Ico b c = Ico a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_le h₂⟩) fun hx => ⟨h₁.trans hx.1, hx.2⟩)
    Ico_subset_Ico_union_Ico

Premises used: Set.Subset.antisymm, Set.Ico_subset_Ico_union_Ico, And.right, And.left, LT.lt.trans_le, And.intro, LE.le.trans, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Tactic:
Ico_union_Ico
    ((min_le_left ..).trans (h₂.trans (le_max_right ..)))
    ((min_le_left ..).trans (h₁.trans (le_max_right ..)))

Premises used: le_max_right, Set.Ico_union_Ico, min_le_left, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Icc a c ⊆ Ico a b ∪ Icc b c

Tactic:
fun x hx =>
  (lt_or_ge x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Premises used: Set.Subset, And.right, And.left, And.intro, Or.inl, lt_or_ge, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ico a b ∪ Icc b c = Icc a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.le.trans h₂⟩) fun hx => ⟨h₁.trans hx.1, hx.2⟩)
    Icc_subset_Ico_union_Icc

Premises used: Set.Subset.antisymm, Set.Icc_subset_Ico_union_Icc, LT.lt.le, And.right, And.left, And.intro, LE.le.trans, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioc a c ⊆ Ioo a b ∪ Icc b c

Tactic:
fun x hx =>
  (lt_or_ge x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Premises used: Set.Subset, And.right, And.left, And.intro, Or.inl, lt_or_ge, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a < b
h₂ : b ≤ c
⊢ Ioo a b ∪ Icc b c = Ioc a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.le.trans h₂⟩) fun hx => ⟨h₁.trans_le hx.1, hx.2⟩)
    Ioc_subset_Ioo_union_Icc

Premises used: Set.Subset.antisymm, LT.lt.le, And.right, And.left, LT.lt.trans_le, And.intro, Set.Ioc_subset_Ioo_union_Icc, LE.le.trans, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioo a c ⊆ Ioc a b ∪ Ioo b c

Tactic:
fun x hx =>
  (le_or_gt x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Premises used: Set.Subset, le_or_gt, And.right, And.left, And.intro, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a ≤ b
h₂ : b < c
⊢ Ioc a b ∪ Ioo b c = Ioo a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_lt h₂⟩) fun hx => ⟨h₁.trans_lt hx.1, hx.2⟩)
    Ioo_subset_Ioc_union_Ioo

Premises used: Set.Subset.antisymm, Set.Ioo_subset_Ioc_union_Ioo, And.right, And.left, And.intro, Or.elim, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ico a c ⊆ Icc a b ∪ Ioo b c

Tactic:
fun x hx =>
  (le_or_gt x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Premises used: Set.Subset, le_or_gt, And.right, And.left, And.intro, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a ≤ b
h₂ : b < c
⊢ Icc a b ∪ Ioo b c = Ico a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_lt h₂⟩) fun hx => ⟨h₁.trans hx.1.le, hx.2⟩)
    Ico_subset_Icc_union_Ioo

Premises used: Set.Subset.antisymm, LT.lt.le, And.right, And.left, And.intro, Set.Ico_subset_Icc_union_Ioo, LE.le.trans, Or.elim, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Icc a c ⊆ Icc a b ∪ Ioc b c

Tactic:
fun x hx =>
  (le_or_gt x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Premises used: Set.Subset, le_or_gt, And.right, And.left, And.intro, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Icc a b ∪ Ioc b c = Icc a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans h₂⟩) fun hx => ⟨h₁.trans hx.1.le, hx.2⟩)
    Icc_subset_Icc_union_Ioc

Premises used: Set.Subset.antisymm, Set.Icc_subset_Icc_union_Ioc, LT.lt.le, And.right, And.left, And.intro, LE.le.trans, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioc a c ⊆ Ioc a b ∪ Ioc b c

Tactic:
fun x hx =>
  (le_or_gt x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Premises used: Set.Subset, le_or_gt, And.right, And.left, And.intro, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ioc a b ∪ Ioc b c = Ioc a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans h₂⟩) fun hx => ⟨h₁.trans_lt hx.1, hx.2⟩)
    Ioc_subset_Ioc_union_Ioc

Premises used: Set.Subset.antisymm, Set.Ioc_subset_Ioc_union_Ioc, And.right, And.left, And.intro, LE.le.trans, Or.elim, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)

Tactic:
Ioc_union_Ioc
    ((min_le_left ..).trans (h₂.trans (le_max_right ..)))
    ((min_le_left ..).trans (h₁.trans (le_max_right ..)))

Premises used: le_max_right, min_le_left, Set.Ioc_union_Ioc, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioo a c ⊆ Ioc a b ∪ Ico b c

Tactic:
Subset.trans Ioo_subset_Ioc_union_Ioo (union_subset_union_right _ Ioo_subset_Ico_self)

Premises used: Set.Subset.trans, Set.union_subset_union_right, Set.Ioo_subset_Ico_self, Set.Ioo_subset_Ioc_union_Ioo
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a < b
h₂ : b < c
⊢ Ioc a b ∪ Ico b c = Ioo a c

Tactic:
Subset.antisymm
    (fun _ hx =>
      hx.elim (fun hx' => ⟨hx'.1, hx'.2.trans_lt h₂⟩) fun hx' => ⟨h₁.trans_le hx'.1, hx'.2⟩)
    Ioo_subset_Ioc_union_Ico

Premises used: Set.Subset.antisymm, Set.Ioo_subset_Ioc_union_Ico, And.right, And.left, LT.lt.trans_le, And.intro, Or.elim, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ico a c ⊆ Icc a b ∪ Ico b c

Tactic:
Subset.trans Ico_subset_Icc_union_Ioo (union_subset_union_right _ Ioo_subset_Ico_self)

Premises used: Set.Subset.trans, Set.union_subset_union_right, Set.Ioo_subset_Ico_self, Set.Ico_subset_Icc_union_Ioo
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a ≤ b
h₂ : b < c
⊢ Icc a b ∪ Ico b c = Ico a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_lt h₂⟩) fun hx => ⟨h₁.trans hx.1, hx.2⟩)
    Ico_subset_Icc_union_Ico

Premises used: Set.Subset.antisymm, Set.Ico_subset_Icc_union_Ico, And.right, And.left, And.intro, LE.le.trans, Or.elim, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Icc a c ⊆ Icc a b ∪ Icc b c

Tactic:
Subset.trans Icc_subset_Icc_union_Ioc (union_subset_union_right _ Ioc_subset_Icc_self)

Premises used: Set.Subset.trans, Set.Icc_subset_Icc_union_Ioc, Set.Ioc_subset_Icc_self, Set.union_subset_union_right
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Icc a b ∪ Icc b c = Icc a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans h₂⟩) fun hx => ⟨h₁.trans hx.1, hx.2⟩)
    Icc_subset_Icc_union_Icc

Premises used: Set.Subset.antisymm, And.right, And.left, And.intro, LE.le.trans, Or.elim, Set.Icc_subset_Icc_union_Icc
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioc a c ⊆ Ioc a b ∪ Icc b c

Tactic:
Subset.trans Ioc_subset_Ioc_union_Ioc (union_subset_union_right _ Ioc_subset_Icc_self)

Premises used: Set.Subset.trans, Set.Ioc_subset_Icc_self, Set.Ioc_subset_Ioc_union_Ioc, Set.union_subset_union_right
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a < b
h₂ : b ≤ c
⊢ Ioc a b ∪ Icc b c = Ioc a c

Tactic:
Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans h₂⟩) fun hx => ⟨h₁.trans_le hx.1, hx.2⟩)
    Ioc_subset_Ioc_union_Icc

Premises used: Set.Subset.antisymm, Set.Ioc_subset_Ioc_union_Icc, And.right, And.left, LT.lt.trans_le, And.intro, LE.le.trans, Or.elim
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h₁ : c < b
h₂ : a < d
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Tactic:
grind