awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hMax : Maximal (fun (x : α) ↦ x ∈ s) a
hb : b ∈ s
obtain : ∀ (z : α) (hz : z ∈ s) (haz : a ≤ z) (hbz : b ≤ z), b ≤ a
⊢ b ≤ a

Tactic:
obtain ⟨z, hz, haz, hbz⟩ := h a hMax.1 b hb

Premises used: And.left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hMax : Maximal (fun (x : α) ↦ x ∈ s) a
hb : b ∈ s
z : α
hz : z ∈ s
haz : a ≤ z
hbz : b ≤ z
⊢ b ≤ a

Tactic:
hbz.trans (hMax.2 hz haz)

Premises used: And.right, LE.le.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hMax : Maximal (fun (x : α) ↦ x ∈ s) a
hb : b ∈ s
z : α
hz : z ∈ s
haz : a ≤ z
hbz : b ≤ z
⊢ b ≤ a

Tactic:
exact hbz.trans (hMax.2 hz haz)

Premises used: And.right, LE.le.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : DirectedOn (fun (x y : α) ↦ y ≤ x) s
⊢ Minimal (fun (x : α) ↦ x ∈ s) a ↔ IsLeast s a

Tactic:
⟨fun hMin ↦ ⟨hMin.1, fun _ hy ↦ h.le_of_minimal hMin hy⟩, fun h ↦ ⟨h.1, fun _ hy _ ↦ h.2 hy⟩⟩

Premises used: DirectedOn.le_of_minimal, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Maximal (fun (x : α) ↦ x ∈ s) a ↔ IsGreatest s a

Tactic:
minimal_iff_isLeast (α := αᵒᵈ) h

Premises used: Set.Mem, setOf, upperBounds, IsGreatest, Maximal, OrderDual, DirectedOn.minimal_iff_isLeast
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a : α
⊢ Minimal (fun (x : α) ↦ x ∈ s) a ↔ IsLeast s a

Tactic:
(Std.Total.directedOn s).minimal_iff_isLeast

Premises used: Std.Total.directedOn, DirectedOn.minimal_iff_isLeast
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a : α
⊢ Maximal (fun (x : α) ↦ x ∈ s) a ↔ IsGreatest s a

Tactic:
(Std.Total.directedOn s).maximal_iff_isGreatest

Premises used: DirectedOn.maximal_iff_isGreatest, Std.Total.directedOn
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s s' : Set α
a b : α
h : (s ∩ s').Nonempty
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds s'
have : ∀ (x : α) (hx : x ∈ s) (hx' : x ∈ s'), a ≤ b
⊢ a ≤ b

Tactic:
have ⟨x, hx, hx'⟩ := h
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s s' : Set α
a b : α
h : (s ∩ s').Nonempty
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds s'
x : α
hx : x ∈ s
hx' : x ∈ s'
⊢ a ≤ b

Tactic:
le_trans (ha hx) (hb hx')

Premises used: le_trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s s' : Set α
a b : α
h : (s ∩ s').Nonempty
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds s'
x : α
hx : x ∈ s
hx' : x ∈ s'
⊢ a ≤ b

Tactic:
exact le_trans (ha hx) (hb hx')

Premises used: le_trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
ha : IsGLB s a
hb : IsLUB s b
hs : s.Nonempty
⊢ a ≤ b

Tactic:
lowerBounds_le_upperBounds ha.1 hb.1 hs

Premises used: And.left, lowerBounds_le_upperBounds
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s s' : Set α
a b : α
h : (s ∩ s').Nonempty
ha : IsGLB s a
hb : IsLUB s' b
⊢ a ≤ b

Tactic:
lowerBounds_le_upperBounds_of_nonempty_inter h ha.left hb.left

Premises used: lowerBounds_le_upperBounds_of_nonempty_inter, And.left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
ha : IsLUB s a
⊢ a < b ↔ ∃ c ∈ upperBounds s, c < b

Tactic:
⟨fun hb => ⟨a, ha.1, hb⟩, fun ⟨_, hcs, hcb⟩ => lt_of_le_of_lt (ha.2 hcs) hcb⟩

Premises used: lt_of_le_of_lt, _private.0.isLUB_lt_iff.match_1, And.right, And.left, And.intro, LT.lt, Iff.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b x y : α
ha : IsGLB s a
hb : IsLUB s b
hab : b ≤ a
hx : x ∈ s
hy : y ∈ s
⊢ x ≤ y

Tactic:
calc
    x ≤ b := hb.1 hx
    _ ≤ a := hab
    _ ≤ y := ha.1 hy

Premises used: Trans.trans, And.left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
h : ∀ (x : α × β), x ∈ upperBounds (s ×ˢ t) ↔ x ∈ upperBounds s ×ˢ upperBounds t
⊢ upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t

Tactic:
ext
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
x : α × β
h :
  ∀ (hs : Nonempty.{u_1 + 1} (↑s : Type u_1)) (ht : Nonempty.{u_2 + 1} (↑t : Type u_2)) (x : α × β),
    x ∈ upperBounds (s ×ˢ t) ↔ x ∈ upperBounds s ×ˢ upperBounds t
⊢ x ∈ upperBounds (s ×ˢ t) ↔ x ∈ upperBounds s ×ˢ upperBounds t

Tactic:
rw [← nonempty_coe_sort] at hs ht

Premises used: Set.nonempty_coe_sort
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
hs : Nonempty.{u_1 + 1} (↑s : Type u_1)
ht : Nonempty.{u_2 + 1} (↑t : Type u_2)
x : α × β
⊢ x ∈ upperBounds (s ×ˢ t) ↔ x ∈ upperBounds s ×ˢ upperBounds t

Tactic:
aesop (add simp [upperBounds, Prod.le_def, forall_and])

Premises used: upperBounds, Prod.le_def, forall_and
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
a : α
b : β
hs : s.Nonempty
ht : t.Nonempty
ha : IsLUB s a
hb : IsLUB t b
⊢ IsLUB (s ×ˢ t) (a, b)

Tactic:
simp_all +contextual [IsLUB, IsLeast, lowerBounds]

Premises used: lowerBounds, IsLeast, IsLUB
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ IsLUB s a ↔ IsLUB s b

Tactic:
simp [isLUB_iff_le_iff, h.le_congr_left]

Premises used: isLUB_iff_le_iff, AntisymmRel.le_congr_left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ IsGLB s a ↔ IsGLB s b

Tactic:
simp [isGLB_iff_le_iff, h.le_congr_right]

Premises used: isGLB_iff_le_iff, AntisymmRel.le_congr_right
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a b : α
Ha : IsLeast s a
Hb : IsLeast s b
⊢ a = b

Tactic:
le_antisymm (Ha.right Hb.left) (Hb.right Ha.left)

Premises used: le_antisymm, And.right, And.left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a b : α
Ha : IsLeast s a
⊢ IsLeast s b ↔ a = b

Tactic:
Iff.intro Ha.unique fun h => h ▸ Ha

Premises used: Eq.rec, Iff.intro, IsLeast.unique
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a b : α
Ha : IsLUB s a
Hb : IsLUB s b
⊢ a = b

Tactic:
IsLeast.unique Ha Hb

Premises used: IsLeast.unique
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a b : α
Ha : IsGLB s a
Hb : IsLUB s b
hab : b ≤ a
⊢ s.Subsingleton

Tactic:
fun _ hx _ hy =>
  le_antisymm (le_of_isLUB_le_isGLB Ha Hb hab hx hy) (le_of_isLUB_le_isGLB Ha Hb hab hy hx)

Premises used: le_of_isLUB_le_isGLB, le_antisymm, Set.Subsingleton
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a b : α
Ha : IsGLB s a
Hb : IsLUB s b
x y : α
Hx : x ∈ s
Hy : y ∈ s
Hxy : x ≠ y
⊢ a < b

Tactic:
lt_iff_le_not_ge.2
    ⟨lowerBounds_le_upperBounds Ha.1 Hb.1 ⟨x, Hx⟩, fun hab =>
      Hxy <| Set.subsingleton_of_isLUB_le_isGLB Ha Hb hab Hx Hy⟩

Premises used: Iff.mpr, lt_iff_le_not_ge, And.left, And.intro, Exists.intro, lowerBounds_le_upperBounds, Set.subsingleton_of_isLUB_le_isGLB
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
simp_rw : ¬a ≤ b ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₁ : b ∉ upperBounds s ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₂ : (¬∀ x ∈ s, x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₃ : (∃ (x : α) (_ : x ∈ s), ¬x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₄ : (∃ (x : α) (_ : x ∈ s), b < x) ↔ ∃ c ∈ s, b < c
⊢ b < a ↔ ∃ c ∈ s, b < c

Tactic:
simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]

Premises used: not_le, exists_prop, isLUB_le_iff, Classical.not_forall, mem_upperBounds
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
hb : b < a
⊢ ∃ c ∈ s, b < c ∧ c ≤ a

Tactic:
let ⟨c, hcs, hbc⟩ := (lt_isLUB_iff h).1 hb
  ⟨c, hcs, hbc, h.1 hcs⟩

Premises used: lt_isLUB_iff, Membership.mem, Exists, LE.le, _private.0.IsLUB.exists_between.match_1, And, And.left, And.intro, LT.lt, Exists.intro, Iff.mp
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
h' : a ∉ s
hb : b < a
⊢ ∃ c ∈ s, b < c ∧ c < a

Tactic:
let ⟨c, hcs, hbc, hca⟩ := h.exists_between hb
  ⟨c, hcs, hbc, hca.lt_of_ne fun hac => h' <| hac ▸ hcs⟩

Premises used: IsLUB.exists_between, _private.0.IsLUB.exists_between'.match_1, Membership.mem, Exists, Eq.rec, LE.le.lt_of_ne, And, And.intro, LT.lt, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsGLB s a
hb : a < b
⊢ ∃ c ∈ s, a ≤ c ∧ c < b

Tactic:
let ⟨c, hcs, hbc⟩ := (isGLB_lt_iff h).1 hb
  ⟨c, hcs, h.1 hcs, hbc⟩

Premises used: Membership.mem, Exists, isGLB_lt_iff, LE.le, And, And.left, And.intro, LT.lt, Exists.intro, Iff.mp, _private.0.IsGLB.exists_between.match_1
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsGLB s a
h' : a ∉ s
hb : a < b
⊢ ∃ c ∈ s, a < c ∧ c < b

Tactic:
let ⟨c, hcs, hac, hcb⟩ := h.exists_between hb
  ⟨c, hcs, hac.lt_of_ne fun hac => h' <| hac.symm ▸ hcs, hcb⟩

Premises used: Membership.mem, Exists, Eq.rec, IsGLB.exists_between, LE.le.lt_of_ne, And, And.intro, LT.lt, Exists.intro, Eq.symm, _private.0.IsGLB.exists_between'.match_1
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ IsGreatest {w : α | w ⊓ a ≤ b} (a ⇨ b)

Tactic:
simp [IsGreatest, mem_upperBounds]

Premises used: IsGreatest, mem_upperBounds
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ IsLeast {w : α | a ≤ b ⊔ w} (a \ b)

Tactic:
simp [IsLeast, mem_lowerBounds]

Premises used: mem_lowerBounds, IsLeast
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : HeytingAlgebra α
a : α
⊢ IsGreatest {w : α | Disjoint w a} aᶜ

Tactic:
simpa only [himp_bot, disjoint_iff_inf_le] using isGreatest_himp a ⊥

Premises used: himp_bot, isGreatest_himp, Bot.bot, disjoint_iff_inf_le
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ IsLeast {w : α | Codisjoint a w} (￢a)

Tactic:
simpa only [CoheytingAlgebra.top_sdiff, codisjoint_iff_le_sup] using isLeast_sdiff ⊤ a

Premises used: isLeast_sdiff, codisjoint_iff_le_sup, Top.top, CoheytingAlgebra.top_sdiff
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℕ → Prop
n : ℕ
inst : DecidablePred p
⊢ (∀ k < n, ¬p k) ↔ Membership.mem (γ := Set ℕ) (lowerBounds {n : ℕ | p n}) n

Tactic:
simp [mem_lowerBounds, @imp_not_comm _ (p _)]

Premises used: mem_lowerBounds, imp_not_comm
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s t : Set α
a : α
Hf : MonotoneOn f t
Hst : s ⊆ t
Has : a ∈ upperBounds s
Hat : a ∈ t
⊢ f a ∈ upperBounds (f '' s)

Tactic:
forall_mem_image.2 fun _ H => Hf (Hst H) Hat (Has H)

Premises used: Iff.mpr, Set.Mem, setOf, upperBounds, Set.forall_mem_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
t : Set α
a : α
Hf : MonotoneOn f t
⊢ a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t)

Tactic:
Hf.mem_upperBounds_image subset_rfl

Premises used: MonotoneOn.mem_upperBounds_image, subset_rfl
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
Hst : s ⊆ t
a : α
ha : a ∈ upperBounds s ∩ t
⊢ f a ∈ upperBounds (f '' s)

Tactic:
Hf.mem_upperBounds_image Hst ha.1 ha.2

Premises used: And.right, And.left, MonotoneOn.mem_upperBounds_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
Hst : s ⊆ t
a : α
ha : a ∈ upperBounds s ∩ t
⊢ f a ∈ upperBounds (f '' s)

Tactic:
exact Hf.mem_upperBounds_image Hst ha.1 ha.2

Premises used: And.right, And.left, MonotoneOn.mem_upperBounds_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
Hst : s ⊆ t
⊢ (upperBounds s ∩ t).Nonempty → BddAbove (f '' s)

Tactic:
fun ⟨C, hs, ht⟩ =>
  ⟨f C, Hf.mem_upperBounds_image Hst hs ht⟩

Premises used: BddAbove, _private.0.MonotoneOn.map_bddAbove.match_1, Exists.intro, MonotoneOn.mem_upperBounds_image, Set.image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
t : Set α
a : α
Hf : MonotoneOn f t
Ha : IsLeast t a
⊢ IsLeast (f '' t) (f a)

Tactic:
⟨mem_image_of_mem _ Ha.1, Hf.mem_lowerBounds_image_self Ha.2 Ha.1⟩

Premises used: IsLeast, And.right, And.left, Set.mem_image_of_mem, And.intro, MonotoneOn.mem_lowerBounds_image_self
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s t : Set α
a : α
Hf : AntitoneOn f t
Hst : s ⊆ t
Has : a ∈ lowerBounds s
⊢ a ∈ t → f a ∈ upperBounds (f '' s)

Tactic:
Hf.dual_right.mem_lowerBounds_image Hst Has

Premises used: Set.Mem, setOf, upperBounds, AntitoneOn.dual_right, OrderDual, MonotoneOn.mem_lowerBounds_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
t : Set α
a : α
Hf : AntitoneOn f t
⊢ a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t)

Tactic:
Hf.dual_right.mem_lowerBounds_image_self

Premises used: Set.Mem, setOf, upperBounds, AntitoneOn.dual_right, OrderDual, MonotoneOn.mem_lowerBounds_image_self
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s t : Set α
Hf : AntitoneOn f t
Hst : s ⊆ t
⊢ f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s)

Tactic:
Hf.dual_right.image_lowerBounds_subset_lowerBounds_image Hst

Premises used: Set.Mem, setOf, upperBounds, AntitoneOn.dual_right, MonotoneOn.image_lowerBounds_subset_lowerBounds_image, OrderDual
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s t : Set α
Hf : AntitoneOn f t
Hst : s ⊆ t
⊢ (upperBounds s ∩ t).Nonempty → BddBelow (f '' s)

Tactic:
Hf.dual_right.map_bddAbove Hst

Premises used: lowerBounds, MonotoneOn.map_bddAbove, Set.Mem, setOf, AntitoneOn.dual_right, BddBelow, OrderDual
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
t : Set α
a : α
Hf : AntitoneOn f t
⊢ IsGreatest t a → IsLeast (f '' t) (f a)

Tactic:
Hf.dual_right.map_isGreatest

Premises used: lowerBounds, MonotoneOn.map_isGreatest, Set.Mem, setOf, AntitoneOn.dual_right, IsLeast, OrderDual
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
Hf : Monotone f
a : α
s : Set α
Ha : a ∈ upperBounds s
⊢ f a ∈ upperBounds (f '' s)

Tactic:
forall_mem_image.2 fun _ H => Hf (Ha H)

Premises used: Iff.mpr, Set.Mem, setOf, upperBounds, Set.forall_mem_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
Hf : Monotone f
s : Set α
a : α
ha : a ∈ upperBounds s
⊢ f a ∈ upperBounds (f '' s)

Tactic:
Hf.mem_upperBounds_image ha

Premises used: Monotone.mem_upperBounds_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
Hf : Monotone f
s : Set α
a : α
ha : a ∈ upperBounds s
⊢ f a ∈ upperBounds (f '' s)

Tactic:
exact Hf.mem_upperBounds_image ha

Premises used: Monotone.mem_upperBounds_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
Hf : Monotone f
a : α
s : Set α
Ha : IsLeast s a
⊢ IsLeast (f '' s) (f a)

Tactic:
⟨mem_image_of_mem _ Ha.1, Hf.mem_lowerBounds_image Ha.2⟩

Premises used: Monotone.mem_lowerBounds_image, IsLeast, And.right, And.left, Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
a : α
s : Set α
⊢ a ∈ lowerBounds s → f a ∈ upperBounds (f '' s)

Tactic:
hf.dual_right.mem_lowerBounds_image

Premises used: Monotone.mem_lowerBounds_image, Antitone.dual_right, Set.Mem, setOf, upperBounds, OrderDual
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
s : Set α
⊢ f '' lowerBounds s ⊆ upperBounds (f '' s)

Tactic:
hf.dual_right.image_lowerBounds_subset_lowerBounds_image

Premises used: Antitone.dual_right, Set.Mem, setOf, upperBounds, Monotone.image_lowerBounds_subset_lowerBounds_image, OrderDual
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
s : Set α
⊢ BddAbove s → BddBelow (f '' s)

Tactic:
hf.dual_right.map_bddAbove

Premises used: Antitone.dual_right, lowerBounds, Set.Mem, setOf, Monotone.map_bddAbove, BddBelow, OrderDual
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
a : α
s : Set α
⊢ IsGreatest s a → IsLeast (f '' s) (f a)

Tactic:
hf.dual_right.map_isGreatest

Premises used: Antitone.dual_right, lowerBounds, Set.Mem, setOf, IsLeast, Monotone.map_isGreatest, OrderDual
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ f a ∈ upperBounds (f '' s) ↔ a ∈ upperBounds s

Tactic:
simp [upperBounds, hf.le_iff_le]

Premises used: upperBounds, StrictMono.le_iff_le
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ f a ∈ lowerBounds (f '' s) ↔ a ∈ lowerBounds s

Tactic:
simp [lowerBounds, hf.le_iff_le]

Premises used: lowerBounds, StrictMono.le_iff_le
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ IsLeast (f '' s) (f a) ↔ IsLeast s a

Tactic:
simp [IsLeast, hf.injective.eq_iff, hf.mem_lowerBounds_image]

Premises used: Function.Injective.eq_iff, IsLeast, StrictMono.mem_lowerBounds_image, StrictMono.injective
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ IsGreatest (f '' s) (f a) ↔ IsGreatest s a

Tactic:
simp [IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]

Premises used: Function.Injective.eq_iff, StrictMono.injective, IsGreatest, StrictMono.mem_upperBounds_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ f a ∈ upperBounds (f '' s) ↔ a ∈ lowerBounds s

Tactic:
simp [upperBounds, lowerBounds, hf.le_iff_ge]

Premises used: lowerBounds, upperBounds, StrictAnti.le_iff_ge
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s

Tactic:
simp [upperBounds, lowerBounds, hf.le_iff_ge]

Premises used: lowerBounds, upperBounds, StrictAnti.le_iff_ge
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ IsLeast (f '' s) (f a) ↔ IsGreatest s a

Tactic:
simp [IsLeast, IsGreatest, hf.injective.eq_iff, hf.mem_lowerBounds_image]

Premises used: Function.Injective.eq_iff, StrictAnti.mem_lowerBounds_image, IsLeast, IsGreatest, StrictAnti.injective
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ IsGreatest (f '' s) (f a) ↔ IsLeast s a

Tactic:
simp [IsLeast, IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]

Premises used: StrictAnti.mem_upperBounds_image, Function.Injective.eq_iff, IsLeast, IsGreatest, StrictAnti.injective
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
ha : a ∈ upperBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ upperBounds (image2 f s t)

Tactic:
forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy

Premises used: Iff.mpr, Set.forall_mem_image2, Set.Mem, setOf, upperBounds, LE.le.trans
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)

Tactic:
image2_subset_iff.2 fun _ ha _ hb ↦ mem_upperBounds_image2 h₀ h₁ ha hb

Premises used: Iff.mpr, Set.image2_subset_iff, mem_upperBounds_image2
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

Tactic:
⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro, mem_upperBounds_image2
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
ha : IsGreatest s a
hb : IsGreatest t b
⊢ IsGreatest (image2 f s t) (f a b)

Tactic:
⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2 h₀ h₁ ha.2 hb.2⟩

Premises used: IsGreatest, And.right, And.left, And.intro, Set.mem_image2_of_mem, mem_upperBounds_image2
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Antitone (f a)
ha : a ∈ upperBounds s
hb : b ∈ lowerBounds t
⊢ f a b ∈ upperBounds (image2 f s t)

Tactic:
forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy

Premises used: Iff.mpr, Set.forall_mem_image2, Set.Mem, setOf, upperBounds, LE.le.trans
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t)

Tactic:
image2_subset_iff.2 fun _ ha _ hb ↦
    mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb

Premises used: Iff.mpr, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds, Set.image2_subset_iff