awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hexists : ∃ (M : α), P M
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
contrapose! : ∀ (hexists : ¬P ⊤) (M : α), ¬P M
⊢ P ⊤

Tactic:
contrapose! hexists
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
pos : ∀ (hx : x = ⊤), ¬P x
neg : ∀ (hx : ¬x = ⊤), ¬P x
⊢ ¬P x

Tactic:
by_cases hx : x = ⊤
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : x = ⊤
⊢ ¬P x

Tactic:
hx ▸ hexists

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : x = ⊤
⊢ ¬P x

Tactic:
exact hx ▸ hexists
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
hx' : P x
neg : ∀ (M : α) (hM : M > x) (hM' : P M), False
⊢ False

Tactic:
obtain ⟨M, hM, hM'⟩ := hind x hx hx'
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
hx' : P x
M : α
hM : M > x
hM' : P M
⊢ False

Tactic:
IH _ hM hM'
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
hx' : P x
M : α
hM : M > x
hM' : P M
⊢ False

Tactic:
exact IH _ hM hM'
-- Module: Mathlib.Order.BoundedOrder.Lattice
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
M : α
ind : ∀ (x : α) (IH : ∀ (y : α), x < y → ¬P y), ¬P x
⊢ ¬P M

Tactic:
induction M using WellFoundedGT.induction with
  | ind x IH =>
    by_cases hx : x = ⊤
    · exact hx ▸ hexists
    · intro hx'
      obtain ⟨M, hM, hM'⟩ := hind x hx hx'
      exact IH _ hM hM'

Premises used: WellFoundedGT.induction
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : Preorder β
f : α → β
a : α
hf : StrictMono f
⊢ f a = f ⊤ ↔ a = ⊤

Tactic:
⟨fun h => not_lt_top_iff.1 fun ha => (hf ha).ne h, congr_arg _⟩

Premises used: not_lt_top_iff, congr_arg, Iff.intro, Iff.mp, LT.lt.ne
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : Preorder β
f : α → β
a : α
hf : StrictAnti f
⊢ f a = f ⊤ ↔ a = ⊤

Tactic:
⟨fun h => not_lt_top_iff.1 fun ha => (hf ha).ne' h, congr_arg _⟩

Premises used: not_lt_top_iff, congr_arg, LT.lt.ne', Iff.intro, Iff.mp
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
inst_2 : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
rw : p ≤ ⊤
⊢ p ≤ f a

Tactic:
rw [h_top]
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
inst_2 : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
inst_2 : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : Preorder β
f : α → β
a : α
hf : StrictMono f
⊢ f a = f ⊥ ↔ a = ⊥

Tactic:
hf.dual.apply_eq_top_iff

Premises used: StrictMono.dual, StrictMono.apply_eq_top_iff, OrderDual
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : Preorder β
f : α → β
a : α
hf : StrictAnti f
⊢ f a = f ⊥ ↔ a = ⊥

Tactic:
hf.dual.apply_eq_top_iff

Premises used: StrictAnti.apply_eq_top_iff, StrictAnti.dual, OrderDual
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
inst_2 : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
rw : ⊥ ≤ p
⊢ f a ≤ p

Tactic:
rw [h_bot]
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
inst_2 : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
inst_2 : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
inst : Preorder α
p q : α → Prop
m_p : Monotone p
m_q : Monotone q
⊢ Monotone (β := Prop) fun (x : α) ↦ p x ∧ q x

Tactic:
fun _ _ h => And.imp (m_p h) (m_q h)

Premises used: And.imp, Monotone
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
inst : Preorder α
p q : α → Prop
m_p : Monotone p
m_q : Monotone q
⊢ Monotone (β := Prop) fun (x : α) ↦ p x ∨ q x

Tactic:
fun _ _ h => Or.imp (m_p h) (m_q h)

Premises used: Monotone, Or.imp
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
inst : Preorder α
x : α
⊢ Monotone (β := Prop) fun (x_1 : α) ↦ x ≤ x_1

Tactic:
fun _ _ h' h => h.trans h'

Premises used: Monotone, LE.le.trans
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
inst : Preorder α
x : α
⊢ Monotone (β := Prop) fun (x_1 : α) ↦ x < x_1

Tactic:
fun _ _ h' h => h.trans_le h'

Premises used: Monotone, LT.lt.trans_le
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
inst : Preorder α
x : α
⊢ Antitone (β := Prop) fun (x_1 : α) ↦ x_1 ≤ x

Tactic:
fun _ _ h' h => h'.trans h

Premises used: Antitone, LE.le.trans
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
inst : Preorder α
x : α
⊢ Antitone (β := Prop) fun (x_1 : α) ↦ x_1 < x

Tactic:
fun _ _ h' h => h'.trans_lt h

Premises used: Antitone, LE.le.trans_lt
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : Preorder α
P : β → α → Prop
hP : ∀ (x : β), Monotone (P x)
⊢ Monotone (β := Prop) fun (y : α) ↦ ∀ (x : β), P x y

Tactic:
fun _ _ hy h x => hP x hy <| h x

Premises used: Monotone
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : Preorder α
P : β → α → Prop
hP : ∀ (x : β), Antitone (P x)
⊢ Antitone (β := Prop) fun (y : α) ↦ ∀ (x : β), P x y

Tactic:
fun _ _ hy h x => hP x hy (h x)

Premises used: Antitone
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : Preorder α
P : β → α → Prop
s : Set β
hP : ∀ (x : β), x ∈ s → Monotone (P x)
⊢ Monotone (β := Prop) fun (y : α) ↦ ∀ (x : β), x ∈ s → P x y

Tactic:
fun _ _ hy h x hx => hP x hx hy (h x hx)

Premises used: Monotone
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : Preorder α
P : β → α → Prop
s : Set β
hP : ∀ (x : β), x ∈ s → Antitone (P x)
⊢ Antitone (β := Prop) fun (y : α) ↦ ∀ (x : β), x ∈ s → P x y

Tactic:
fun _ _ hy h x hx => hP x hx hy (h x hx)

Premises used: Antitone
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : Preorder α
P : β → α → Prop
hP : ∀ (x : β), Monotone (P x)
⊢ Monotone (β := Prop) fun (y : α) ↦ ∃ (x : β), P x y

Tactic:
fun _ _ hy ⟨x, hx⟩ ↦ ⟨x, hP x hy hx⟩

Premises used: _private.0.Monotone.exists.match_1, Monotone, Exists, Exists.intro
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
β : Type v
inst : Preorder α
P : β → α → Prop
hP : ∀ (x : β), Antitone (P x)
⊢ Antitone (β := Prop) fun (y : α) ↦ ∃ (x : β), P x y

Tactic:
fun _ _ hy ⟨x, hx⟩ ↦ ⟨x, hP x hy hx⟩

Premises used: _private.0.Monotone.exists.match_1, Exists, Antitone, Exists.intro
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
inst : Preorder α
P : α → Prop
x₀ : α
hP : Monotone P
⊢ (∀ (x : α), x ≥ x₀ → P x) ↔ P x₀

Tactic:
⟨fun H ↦ H x₀ le_rfl, fun H _ hx ↦ hP hx H⟩

Premises used: le_rfl, Iff.intro
-- Module: Mathlib.Order.BoundedOrder.Monotone
Goal:
α : Type u
inst : Preorder α
P : α → Prop
x₀ : α
hP : Antitone P
⊢ (∀ (x : α), x ≤ x₀ → P x) ↔ P x₀

Tactic:
⟨fun H ↦ H x₀ le_rfl, fun H _ hx ↦ hP hx H⟩

Premises used: le_rfl, Iff.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
⊢ a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, upperBounds
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
⊢ a ∈ upperBounds s ↔ s ⊆ Iic a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, upperBounds, Set.Subset, Set.Iic
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ BddAbove s ↔ ∃ (x : α), ∀ y ∈ s, y ≤ x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, upperBounds, BddAbove, Set.Nonempty
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
s : Set α
⊢ ⊤ ∈ upperBounds s

Tactic:
fun _ _ => le_top

Premises used: Set.Mem, setOf, upperBounds, le_top
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : OrderBot α
⊢ IsLeast s ⊥ ↔ ⊥ ∈ s

Tactic:
and_iff_left <| bot_mem_lowerBounds _

Premises used: and_iff_left, IsLeast, bot_mem_lowerBounds
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, ¬y ≤ x

Tactic:
simp [BddAbove, upperBounds, Set.Nonempty]

Premises used: upperBounds, BddAbove, Set.Nonempty
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_4
inst : LinearOrder α
s : Set α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, x < y

Tactic:
simp only [not_bddAbove_iff', not_le]

Premises used: not_le, not_bddAbove_iff'
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ BddAbove (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔ BddBelow s

Tactic:
Iff.rfl

Premises used: lowerBounds, Set.Mem, Iff.rfl, setOf, Set.preimage, BddBelow, OrderDual
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set αᵒᵈ
⊢ BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ BddBelow s

Tactic:
Iff.rfl

Premises used: lowerBounds, Set.Mem, Iff.rfl, setOf, Set.preimage, BddBelow, OrderDual
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : BddAbove s
⊢ BddBelow (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)

Tactic:
h

Premises used: lowerBounds, Set.Mem, setOf, Set.preimage, BddBelow, OrderDual
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : IsLeast s a
⊢ IsGreatest (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s : Set αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)

Tactic:
h

Premises used: Set.Mem, setOf, upperBounds, IsGreatest, Set.preimage, OrderDual
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : IsLUB s a
⊢ IsGLB (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s : Set αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)

Tactic:
h

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsGreatest, Set.preimage, IsGLB, OrderDual
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
rw : IsLeast (upperBounds s) a ↔ IsLUB t a
rw₁ : IsLeast (upperBounds s) a ↔ IsLeast (upperBounds t) a
rw₂ rw₃ : IsLeast (upperBounds t) a ↔ IsLeast (upperBounds t) a
⊢ IsLUB s a ↔ IsLUB t a

Tactic:
rw [IsLUB, IsLUB, h]

Premises used: IsLUB
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hst : s ⊆ t
⊢ IsCofinalFor s t

Tactic:
fun a ha ↦ ⟨a, hst ha, le_rfl⟩

Premises used: IsCofinalFor, le_rfl, And.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ IsCofinalFor s s

Tactic:
.of_subset .rfl

Premises used: IsCofinalFor.of_subset, Set.Subset.rfl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t u : Set α
hst : IsCofinalFor s t
htu : IsCofinalFor t u
⊢ IsCofinalFor s u

Tactic:
fun _a ha ↦ let ⟨_b, hb, hab⟩ := hst ha; let ⟨c, hc, hbc⟩ := htu hb; ⟨c, hc, hab.trans hbc⟩

Premises used: IsCofinalFor, Membership.mem, Exists, LE.le, _private.0.IsCofinalFor.trans.match_1, And, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t u : Set α
hst : s ⊆ t
htu : IsCofinalFor t u
⊢ IsCofinalFor s u

Tactic:
hst.isCofinalFor.trans htu

Premises used: HasSubset.Subset.isCofinalFor, IsCofinalFor.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t u : Set α
htu : t ⊆ u
hst : IsCofinalFor s t
⊢ IsCofinalFor s u

Tactic:
hst.trans htu.isCofinalFor

Premises used: HasSubset.Subset.isCofinalFor, IsCofinalFor.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
β : Type u_4
inst_1 : Preorder β
s : Set (α × β)
hs : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) s
x : α × β
hx : x ∈ s
y : α × β
hy : y ∈ s
obtain : ∀ (z : α × β) (hz : z ∈ s) (hxz : x ≤ z) (hyz : y ≤ z), ∃ b ∈ s, (x.1, y.2) ≤ b
⊢ ∃ b ∈ s, (x.1, y.2) ≤ b

Tactic:
obtain ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
β : Type u_4
inst_1 : Preorder β
s : Set (α × β)
hs : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) s
x : α × β
hx : x ∈ s
y : α × β
hy : y ∈ s
z : α × β
hz : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ s, (x.1, y.2) ≤ b

Tactic:
⟨z, hz, hxz.1, hyz.2⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
β : Type u_4
inst_1 : Preorder β
s : Set (α × β)
hs : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) s
x : α × β
hx : x ∈ s
y : α × β
hy : y ∈ s
z : α × β
hz : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ s, (x.1, y.2) ≤ b

Tactic:
exact ⟨z, hz, hxz.1, hyz.2⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hc : IsCofinalFor s t
a : α
has : a ∈ s
⊢ ∃ b ∈ t, a ≤ b

Tactic:
hc has
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hc : IsCofinalFor s t
a : α
has : a ∈ s
⊢ ∃ b ∈ t, a ≤ b

Tactic:
exact hc has
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hc : IsCofinalFor s t
a : α
hat : a ∈ t
⊢ ∃ b ∈ t, a ≤ b

Tactic:
⟨a, hat, le_rfl⟩

Premises used: le_rfl, And.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hc : IsCofinalFor s t
a : α
hat : a ∈ t
⊢ ∃ b ∈ t, a ≤ b

Tactic:
exact ⟨a, hat, le_rfl⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hc : IsCofinalFor s t
rw : IsCofinalFor (s ∪ t) t
⊢ IsCofinalFor (t ∪ s) t

Tactic:
rw [union_comm]

Premises used: Set.union_comm
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (s ∪ t) t

Tactic:
hc.union_left

Premises used: IsCofinalFor.union_left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (s ∪ t) t

Tactic:
exact hc.union_left

Premises used: IsCofinalFor.union_left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
obtain :
  ∀ (z : α) (hz : z ∈ t) (hxz : x ≤ z) (hyz : y ≤ z),
    ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨z, hz, hxz, hyz⟩ := hd x (hst hx) y (hst hy)
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
obtain :
  ∀ (w : α) (hw : w ∈ s) (hzw : z ≤ w), ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨w, hw, hzw⟩ := hc hz
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
w : α
hw : w ∈ s
hzw : z ≤ w
⊢ ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
⟨w, hw, hxz.trans hzw, hyz.trans hzw⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
w : α
hw : w ∈ s
hzw : z ≤ w
⊢ ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
exact ⟨w, hw, hxz.trans hzw, hyz.trans hzw⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
rw : ¬IsCofinalFor t s → IsCofinalFor s t
⊢ IsCofinalFor t s ∨ IsCofinalFor s t

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
hts : ¬IsCofinalFor t s
x : α
hx : x ∈ s
⊢ ∃ (x : α) (_ : x ∈ t), ∀ x_1 ∈ s, ¬x ≤ x_1

Tactic:
simp only [IsCofinalFor, not_forall, not_exists, not_and] at hts

Premises used: IsCofinalFor, not_exists, not_and, Classical.not_forall
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
hts : ∃ (x : α) (_ : x ∈ t), ∀ x_1 ∈ s, ¬x ≤ x_1
obtain : ∀ (y : α) (hy : y ∈ t) (hys : ∀ x ∈ s, ¬y ≤ x), ∃ b ∈ t, x ≤ b
⊢ ∃ b ∈ t, x ≤ b

Tactic:
obtain ⟨y, hy, hys⟩ := hts
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
inl : ∀ (z : α) (hzs : z ∈ s) (hxz : x ≤ z) (hyz : y ≤ z), ∃ b ∈ t, x ≤ b
inr : ∀ (z : α) (hzt : z ∈ t) (hxz : x ≤ z) (hyz : y ≤ z), ∃ b ∈ t, x ≤ b
⊢ ∃ b ∈ t, x ≤ b

Tactic:
obtain ⟨z, (hzs | hzt), hxz, hyz⟩ := h x (.inl hx) y (.inr hy)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ t, x ≤ b

Tactic:
cases hys z hzs hyz
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
z : α
hzt : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ t, x ≤ b

Tactic:
⟨z, hzt, hxz⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
z : α
hzt : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ t, x ≤ b

Tactic:
exact ⟨z, hzt, hxz⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t) ↔
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
      DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
refine_1 :
  ∀ (h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
      DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
refine_2 :
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
      DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t →
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t) ↔
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
      DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
refine_1 :
  ∀ (hts : IsCofinalFor t s),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
      DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
refine_1₁ :
  ∀ (hst : IsCofinalFor s t),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
      DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
rcases isCofinalFor_or_isCofinalFor_of_directedOn_union h with hts | hst

Premises used: isCofinalFor_or_isCofinalFor_of_directedOn_union
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
hts : IsCofinalFor t s
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
.inl ⟨DirectedOn.of_isCofinalFor h subset_union_left hts.union_right, hts⟩

Premises used: Set.subset_union_left, DirectedOn.of_isCofinalFor, IsCofinalFor.union_right, And.intro, Or.inl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
hts : IsCofinalFor t s
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
exact .inl ⟨DirectedOn.of_isCofinalFor h subset_union_left hts.union_right, hts⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
hst : IsCofinalFor s t
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
.inr ⟨DirectedOn.of_isCofinalFor h subset_union_right hst.union_left, hst⟩

Premises used: Set.subset_union_right, DirectedOn.of_isCofinalFor, And.intro, IsCofinalFor.union_left, Or.inr
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
hst : IsCofinalFor s t
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
exact .inr ⟨DirectedOn.of_isCofinalFor h subset_union_right hst.union_left, hst⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
refine_2 :
  ∀ (x' : α) (hx' : x' ∈ s) (hxx' : x ≤ x'),
    ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨x', hx', hxx'⟩ := hts.union_right hx

Premises used: IsCofinalFor.union_right