awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
h : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
obtain : ∀ (a : α) (ha : ∀ (b : α), b ∈ s → (fun (x1 x2 : α) ↦ x1 ≤ x2) b a), Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
obtain ⟨a, ha⟩ := h
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
ha : ∀ (b : α), b ∈ s → (fun (x1 x2 : α) ↦ x1 ≤ x2) b a
obtain : ∀ (b : α) (hb : a < b), Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
obtain ⟨b, hb⟩ := exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
ha : ∀ (b : α), b ∈ s → (fun (x1 x2 : α) ↦ x1 ≤ x2) b a
b : α
hb : a < b
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
⟨b, fun c hc => lt_of_le_of_lt (ha c hc) hb⟩

Premises used: lt_of_le_of_lt, Set.Bounded, Exists.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
ha : ∀ (b : α), b ∈ s → (fun (x1 x2 : α) ↦ x1 ≤ x2) b a
b : α
hb : a < b
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
exact ⟨b, fun c hc => lt_of_le_of_lt (ha c hc) hb⟩
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
simp_rw : ¬Bounded (fun (x1 x2 : α) ↦ x1 < x2) s ↔ ¬Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
simp_rw [← not_bounded_iff, bounded_le_iff_bounded_lt]

Premises used: Set.not_bounded_iff, Set.bounded_le_iff_bounded_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
h : Bounded (fun (x1 x2 : α) ↦ x1 > x2) s
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
let ⟨a, ha⟩ := h
  ⟨a, fun b hb => le_of_lt (ha b hb)⟩

Premises used: _private.0.Set.bounded_ge_of_bounded_gt.match_1, Set.Bounded, le_of_lt, GE.ge, Exists.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
h : Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) s

Tactic:
fun a =>
  let ⟨b, hb, hba⟩ := h a
  ⟨b, hb, fun hba' => hba (le_of_lt hba')⟩

Premises used: le_of_lt, Membership.mem, Exists, _private.0.Set.unbounded_gt_of_unbounded_ge.match_1, GT.gt, And, And.intro, Set.Unbounded, Exists.intro, Not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMinOrder α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s ↔ Bounded (fun (x1 x2 : α) ↦ x1 > x2) s

Tactic:
@bounded_le_iff_bounded_lt αᵒᵈ _ _ _

Premises used: OrderDual, Set.bounded_le_iff_bounded_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMinOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) s ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
@unbounded_lt_iff_unbounded_le αᵒᵈ _ _ _

Premises used: Set.unbounded_lt_iff_unbounded_le, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : LE α
inst_1 : NoTopOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) univ

Tactic:
fun a =>
  let ⟨b, hb⟩ := exists_not_le a
  ⟨b, ⟨⟩, hb⟩

Premises used: Set.univ, Membership.mem, Exists, LE.le, And, NoTopOrder.exists_not_le, And.intro, Set.Unbounded, Exists.intro, _private.0.Set.unbounded_le_univ.match_1, Not, True.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoTopOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) univ

Tactic:
unbounded_lt_of_unbounded_le unbounded_le_univ

Premises used: Set.unbounded_le_univ, Set.unbounded_lt_of_unbounded_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : LE α
inst_1 : NoBotOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) univ

Tactic:
fun a =>
  let ⟨b, hb⟩ := exists_not_ge a
  ⟨b, ⟨⟩, hb⟩

Premises used: Set.univ, Membership.mem, Exists, GE.ge, And, _private.0.Set.unbounded_ge_univ.match_1, And.intro, Set.Unbounded, Exists.intro, NoBotOrder.exists_not_ge, Not, True.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoBotOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) univ

Tactic:
unbounded_gt_of_unbounded_ge unbounded_ge_univ

Premises used: Set.unbounded_ge_univ, Set.unbounded_gt_of_unbounded_ge
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
a : α
⊢ Bounded r {b : α | r b a}

Tactic:
⟨a, fun _ => id⟩

Premises used: Set.Bounded, id, Exists.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (Iio a)

Tactic:
bounded_self a

Premises used: Set.Iio, Set.bounded_self
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (Iio a)

Tactic:
bounded_le_of_bounded_lt (bounded_lt_Iio a)

Premises used: Set.bounded_lt_Iio, Set.bounded_le_of_bounded_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (Iic a)

Tactic:
bounded_self a

Premises used: Set.Iic, Set.bounded_self
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (Iic a)

Tactic:
simp only [← bounded_le_iff_bounded_lt, bounded_le_Iic]

Premises used: Set.bounded_le_Iic, Set.bounded_le_iff_bounded_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 > x2) (Ioi a)

Tactic:
bounded_self a

Premises used: Set.Ioi, setOf, Set.bounded_self
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (Ioi a)

Tactic:
bounded_ge_of_bounded_gt (bounded_gt_Ioi a)

Premises used: Set.bounded_gt_Ioi, Set.bounded_ge_of_bounded_gt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (Ici a)

Tactic:
bounded_self a

Premises used: Set.Ici, setOf, Set.bounded_self
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMinOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 > x2) (Ici a)

Tactic:
simp only [← bounded_ge_iff_bounded_gt, bounded_ge_Ici]

Premises used: Set.bounded_ge_Ici, Set.bounded_ge_iff_bounded_gt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (Ioo a b)

Tactic:
(bounded_lt_Iio b).mono Set.Ioo_subset_Iio_self

Premises used: Set.bounded_lt_Iio, Set.Ioo_subset_Iio_self, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (Ico a b)

Tactic:
(bounded_lt_Iio b).mono Set.Ico_subset_Iio_self

Premises used: Set.bounded_lt_Iio, Set.Ico_subset_Iio_self, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (Ioc a b)

Tactic:
(bounded_lt_Iic b).mono Set.Ioc_subset_Iic_self

Premises used: Set.Ioc_subset_Iic_self, Set.bounded_lt_Iic, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (Icc a b)

Tactic:
(bounded_lt_Iic b).mono Set.Icc_subset_Iic_self

Premises used: Set.Icc_subset_Iic_self, Set.bounded_lt_Iic, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (Ioo a b)

Tactic:
(bounded_le_Iio b).mono Set.Ioo_subset_Iio_self

Premises used: Set.Ioo_subset_Iio_self, Set.bounded_le_Iio, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (Ico a b)

Tactic:
(bounded_le_Iio b).mono Set.Ico_subset_Iio_self

Premises used: Set.Ico_subset_Iio_self, Set.bounded_le_Iio, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (Ioc a b)

Tactic:
(bounded_le_Iic b).mono Set.Ioc_subset_Iic_self

Premises used: Set.Ioc_subset_Iic_self, Set.bounded_le_Iic, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (Icc a b)

Tactic:
(bounded_le_Iic b).mono Set.Icc_subset_Iic_self

Premises used: Set.Icc_subset_Iic_self, Set.bounded_le_Iic, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 > x2) (Ioo a b)

Tactic:
(bounded_gt_Ioi a).mono Set.Ioo_subset_Ioi_self

Premises used: Set.bounded_gt_Ioi, Set.Ioo_subset_Ioi_self, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 > x2) (Ioc a b)

Tactic:
(bounded_gt_Ioi a).mono Set.Ioc_subset_Ioi_self

Premises used: Set.bounded_gt_Ioi, Set.Ioc_subset_Ioi_self, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMinOrder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 > x2) (Ico a b)

Tactic:
(bounded_gt_Ici a).mono Set.Ico_subset_Ici_self

Premises used: Set.bounded_gt_Ici, Set.Ico_subset_Ici_self, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMinOrder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 > x2) (Icc a b)

Tactic:
(bounded_gt_Ici a).mono Set.Icc_subset_Ici_self

Premises used: Set.bounded_gt_Ici, Set.Icc_subset_Ici_self, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (Ioo a b)

Tactic:
(bounded_ge_Ioi a).mono Set.Ioo_subset_Ioi_self

Premises used: Set.Ioo_subset_Ioi_self, Set.Bounded.mono, Set.bounded_ge_Ioi
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (Ioc a b)

Tactic:
(bounded_ge_Ioi a).mono Set.Ioc_subset_Ioi_self

Premises used: Set.Ioc_subset_Ioi_self, Set.Bounded.mono, Set.bounded_ge_Ioi
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (Ico a b)

Tactic:
(bounded_ge_Ici a).mono Set.Ico_subset_Ici_self

Premises used: Set.bounded_ge_Ici, Set.Ico_subset_Ici_self, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (Icc a b)

Tactic:
(bounded_ge_Ici a).mono Set.Icc_subset_Ici_self

Premises used: Set.bounded_ge_Ici, Set.Icc_subset_Ici_self, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : NoMaxOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (Ioi a)

Tactic:
fun b =>
  let ⟨c, hc⟩ := exists_gt (a ⊔ b)
  ⟨c, le_sup_left.trans_lt hc, (le_sup_right.trans_lt hc).not_ge⟩

Premises used: Set.Ioi, _private.0.Set.unbounded_le_Ioi.match_1, le_sup_left, Membership.mem, Exists, le_sup_right, NoMaxOrder.exists_gt, LE.le, And, Max.max, And.intro, Set.Unbounded, Exists.intro, LT.lt.not_ge, LE.le.trans_lt, Not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : NoMaxOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (Ici a)

Tactic:
(unbounded_le_Ioi a).mono Set.Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, Set.unbounded_le_Ioi, Set.Unbounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : NoMaxOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) (Ioi a)

Tactic:
unbounded_lt_of_unbounded_le (unbounded_le_Ioi a)

Premises used: Set.unbounded_le_Ioi, Set.unbounded_lt_of_unbounded_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
inst : SemilatticeSup α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) (Ici a)

Tactic:
fun b =>
  ⟨a ⊔ b, le_sup_left, le_sup_right.not_gt⟩

Premises used: le_sup_left, le_sup_right, LE.le.not_gt, Max.max, And.intro, Set.Unbounded, Exists.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Bounded r (s ∩ {b : α | ¬r b a}) ↔ Bounded r s

Tactic:
⟨?_, Bounded.mono inter_subset_left⟩

Premises used: Set.inter_subset_left, Iff.intro, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m
a : α
refine : Bounded r (s ∩ {b : α | ¬r b a}) → Bounded r s
⊢ Bounded r (s ∩ {b : α | ¬r b a}) ↔ Bounded r s

Tactic:
refine ⟨?_, Bounded.mono inter_subset_left⟩
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ (b_1 : α), b_1 ∈ s ∩ {b : α | ¬r b a} → r b_1 b
obtain : ∀ (m : α) (hm : ∀ (c : α), r c a ∨ r c b → r c m), Bounded r s
⊢ Bounded r s

Tactic:
obtain ⟨m, hm⟩ := H a b
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ (b_1 : α), b_1 ∈ s ∩ {b : α | ¬r b a} → r b_1 b
m : α
hm : ∀ (c : α), r c a ∨ r c b → r c m
⊢ Bounded r s

Tactic:
⟨m, fun c hc => hm c (or_iff_not_imp_left.2 fun hca => hb c ⟨hc, hca⟩)⟩

Premises used: Iff.mpr, Set.Bounded, Classical.or_iff_not_imp_left, And.intro, Exists.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ (b_1 : α), b_1 ∈ s ∩ {b : α | ¬r b a} → r b_1 b
m : α
hm : ∀ (c : α), r c a ∨ r c b → r c m
⊢ Bounded r s

Tactic:
exact ⟨m, fun c hc => hm c (or_iff_not_imp_left.2 fun hca => hb c ⟨hc, hca⟩)⟩
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m
a : α
simp_rw : ¬Bounded r (s ∩ {b : α | ¬r b a}) ↔ ¬Bounded r s
⊢ Unbounded r (s ∩ {b : α | ¬r b a}) ↔ Unbounded r s

Tactic:
simp_rw [← not_bounded_iff, bounded_inter_not H]

Premises used: Set.not_bounded_iff, Set.bounded_inter_not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
bounded_inter_not (fun x y => ⟨x ⊔ y, fun _ h => h.elim le_sup_of_le_left le_sup_of_le_right⟩) a

Premises used: Max.max, Exists.intro, Or.elim, Set.bounded_inter_not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
rw : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]

Premises used: not_iff_not, Set.not_bounded_iff
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
bounded_le_inter_not_le a

Premises used: Set.bounded_le_inter_not_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
exact bounded_le_inter_not_le a

Premises used: Set.bounded_le_inter_not_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
simp_rw : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
simp_rw [← not_le, bounded_le_inter_not_le]

Premises used: not_le, Set.bounded_le_inter_not_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
@unbounded_le_inter_not_le _ s _ a

Premises used: Set.unbounded_le_inter_not_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
h : ∀ (x : α), a < x ↔ ¬x ≤ a
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
convert! @unbounded_le_inter_not_le _ s _ a

Premises used: Set.unbounded_le_inter_not_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a x : α
⊢ a < x ↔ ¬x ≤ a

Tactic:
lt_iff_not_ge

Premises used: lt_iff_not_ge
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a x : α
⊢ a < x ↔ ¬x ≤ a

Tactic:
exact lt_iff_not_ge

Premises used: lt_iff_not_ge
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
⟨?_, Bounded.mono Set.inter_subset_left⟩

Premises used: Set.inter_subset_left, Iff.intro, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
refine : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) → Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
refine ⟨?_, Bounded.mono Set.inter_subset_left⟩
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
rw :
  Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) → Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b})
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) → Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
rw [← @bounded_le_inter_lt _ s _ a]

Premises used: Set.bounded_le_inter_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) → Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b})

Tactic:
Bounded.mono fun x ⟨hx, hx'⟩ => ⟨hx, le_of_lt hx'⟩

Premises used: setOf, le_of_lt, Membership.mem, _private.0.Set.bounded_le_inter_le.match_1, LE.le, Inter.inter, And.intro, Set.Bounded.mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) → Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b})

Tactic:
exact Bounded.mono fun x ⟨hx, hx'⟩ => ⟨hx, le_of_lt hx'⟩
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
rw : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]

Premises used: not_iff_not, Set.not_bounded_iff
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
bounded_le_inter_le a

Premises used: Set.bounded_le_inter_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
exact bounded_le_inter_le a

Premises used: Set.bounded_le_inter_le
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
bounded_inter_not (fun x y => ⟨x ⊔ y, fun _ h => h.elim lt_sup_of_lt_left lt_sup_of_lt_right⟩) a

Premises used: Max.max, Exists.intro, Or.elim, Set.bounded_inter_not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
rw : Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]

Premises used: not_iff_not, Set.not_bounded_iff
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
bounded_lt_inter_not_lt a

Premises used: Set.bounded_lt_inter_not_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
exact bounded_lt_inter_not_lt a

Premises used: Set.bounded_lt_inter_not_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
@bounded_lt_inter_not_lt _ s _ a

Premises used: Set.bounded_lt_inter_not_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
h : ∀ (x : α), a ≤ x ↔ ¬x < a
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
convert! @bounded_lt_inter_not_lt _ s _ a

Premises used: Set.bounded_lt_inter_not_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a x : α
⊢ a ≤ x ↔ ¬x < a

Tactic:
not_lt.symm

Premises used: not_lt, Iff.symm
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a x : α
⊢ a ≤ x ↔ ¬x < a

Tactic:
exact not_lt.symm

Premises used: not_lt, Iff.symm
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
@unbounded_lt_inter_not_lt _ s _ a

Premises used: Set.unbounded_lt_inter_not_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
h : ∀ (x : α), a ≤ x ↔ ¬x < a
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a ≤ b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
convert! @unbounded_lt_inter_not_lt _ s _ a

Premises used: Set.unbounded_lt_inter_not_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMaxOrder α
a : α
rw : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
rw [← bounded_le_iff_bounded_lt, ← bounded_le_iff_bounded_lt]

Premises used: Set.bounded_le_iff_bounded_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMaxOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
bounded_le_inter_lt a

Premises used: Set.bounded_le_inter_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMaxOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
exact bounded_le_inter_lt a

Premises used: Set.bounded_le_inter_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMaxOrder α
a : α
rw : Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a < b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]

Premises used: not_iff_not, Set.not_bounded_iff
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMaxOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
bounded_lt_inter_lt a

Premises used: Set.bounded_lt_inter_lt
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMaxOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
exact bounded_lt_inter_lt a

Premises used: Set.bounded_lt_inter_lt