awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)

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

Premises used: mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds, BddAbove, Set.Nonempty, Exists.intro
-- 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)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds 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 : α), Antitone (f a)
ha : IsGreatest s a
hb : IsLeast t b
⊢ IsGreatest (image2 f s t) (f a b)

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

Premises used: mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds, IsGreatest, And.right, And.left, And.intro, Set.mem_image2_of_mem
-- 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Antitone (f a)
ha : a ∈ lowerBounds 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t)

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

Premises used: Iff.mpr, mem_upperBounds_image2_of_mem_lowerBounds, Set.image2_subset_iff
-- 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)

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

Premises used: mem_upperBounds_image2_of_mem_lowerBounds, BddAbove, Set.Nonempty, Exists.intro
-- 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2_of_mem_lowerBounds 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Antitone (f a)
ha : IsLeast s a
hb : IsLeast t b
⊢ IsGreatest (image2 f s t) (f a b)

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

Premises used: mem_upperBounds_image2_of_mem_lowerBounds, IsGreatest, And.right, And.left, And.intro, Set.mem_image2_of_mem
-- 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
ha : a ∈ lowerBounds 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)

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

Premises used: Iff.mpr, Set.image2_subset_iff, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds
-- 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

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

Premises used: BddAbove, Set.Nonempty, Exists.intro, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds
-- 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds 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 : β), Antitone (swap (φ := fun (x : α) (y : β) ↦ γ) f b)
h₁ : ∀ (a : α), Monotone (f a)
ha : IsLeast 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_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩

Premises used: IsGreatest, And.right, And.left, And.intro, Set.mem_image2_of_mem, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
simp : ∀ ⦃x : α⦄, x ∈ s → ∃ x_1 ∈ t, f x ≤ f x_1
⊢ IsCofinalFor (f '' s) (f '' t)

Tactic:
simp only [IsCofinalFor, forall_mem_image, exists_mem_image]

Premises used: IsCofinalFor, Set.exists_mem_image, Set.forall_mem_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
a : α
ha : a ∈ s
obtain : ∀ (b : α) (hb : b ∈ t) (hab : a ≤ b), ∃ x ∈ t, f a ≤ f x
⊢ ∃ x ∈ t, f a ≤ f x

Tactic:
obtain ⟨b, hb, hab⟩ := hst ha
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : a ≤ b
⊢ ∃ x ∈ t, f a ≤ f x

Tactic:
⟨b, hb, hf hab⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : a ≤ b
⊢ ∃ x ∈ t, f a ≤ f x

Tactic:
exact ⟨b, hb, hf hab⟩
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
simp : ∀ ⦃x : α⦄, x ∈ s → ∃ x_1 ∈ t, f x_1 ≤ f x
⊢ IsCoinitialFor (f '' s) (f '' t)

Tactic:
simp only [IsCoinitialFor, forall_mem_image, exists_mem_image]

Premises used: IsCoinitialFor, Set.exists_mem_image, Set.forall_mem_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
a : α
ha : a ∈ s
obtain : ∀ (b : α) (hb : b ∈ t) (hab : a ≤ b), ∃ x ∈ t, f x ≤ f a
⊢ ∃ x ∈ t, f x ≤ f a

Tactic:
obtain ⟨b, hb, hab⟩ := hst ha
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : a ≤ b
⊢ ∃ x ∈ t, f x ≤ f a

Tactic:
⟨b, hb, hf hab⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : a ≤ b
⊢ ∃ x ∈ t, f x ≤ f a

Tactic:
exact ⟨b, hb, hf hab⟩
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
⊢ BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s)

Tactic:
⟨fun ⟨p, hp⟩ ↦ ⟨⟨p.1, forall_mem_image.2 fun _q hq ↦ (hp hq).1⟩,
    ⟨p.2, forall_mem_image.2 fun _q hq ↦ (hp hq).2⟩⟩,
    fun ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ ↦ ⟨⟨x, y⟩, fun _p hp ↦
      ⟨hx <| mem_image_of_mem _ hp, hy <| mem_image_of_mem _ hp⟩⟩⟩

Premises used: Iff.mpr, Prod.mk, Prod.fst, BddAbove, And, And.right, And.left, Set.mem_image_of_mem, And.intro, Iff.intro, Exists.intro, Set.image, _private.0.bddAbove_prod.match_2, Prod.snd, _private.0.bddAbove_prod.match_1, Set.forall_mem_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
ι : Sort x
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
F : ι → α × β
⊢ BddAbove (range F) ↔ BddAbove (range (Prod.fst ∘ F)) ∧ BddAbove (range (Prod.snd ∘ F))

Tactic:
simp only [bddAbove_prod, ← range_comp]

Premises used: Set.range_comp, bddAbove_prod
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2

Tactic:
⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩

Premises used: monotone_fst, And.left, Monotone.mem_upperBounds_image, And.intro, Iff.intro, monotone_snd
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
refine_1 : ∀ (H : IsLUB s p) (a : α) (ha : a ∈ upperBounds (Prod.fst '' s)), p.1 ≤ a
refine_2 : ∀ (H : IsLUB s p) (a : β) (ha : a ∈ upperBounds (Prod.snd '' s)), p.2 ≤ a
refine_3 : ∀ (H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2), p ∈ upperBounds s
refine_4 : ∀ (H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2), p ∈ lowerBounds (upperBounds s)
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2

Tactic:
refine
    ⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
refine_1 : (a, p.2) ∈ upperBounds s
⊢ p.1 ≤ a

Tactic:
suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ (a, p.2) ∈ upperBounds s

Tactic:
fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩

Premises used: Set.Mem, setOf, upperBounds, Prod.fst, And.right, And.left, Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ (a, p.2) ∈ upperBounds s

Tactic:
exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
refine_2 : (p.1, a) ∈ upperBounds s
⊢ p.2 ≤ a

Tactic:
suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ (p.1, a) ∈ upperBounds s

Tactic:
fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩

Premises used: Set.Mem, setOf, upperBounds, And.left, Set.mem_image_of_mem, And.intro, Prod.snd
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ (p.1, a) ∈ upperBounds s

Tactic:
exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ upperBounds s

Tactic:
fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩

Premises used: Set.Mem, setOf, upperBounds, Prod.fst, And.right, And.left, Set.mem_image_of_mem, And.intro, Prod.snd
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ upperBounds s

Tactic:
exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ lowerBounds (upperBounds s)

Tactic:
fun q hq =>
      ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq,
        H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩

Premises used: monotone_fst, lowerBounds, Set.Mem, setOf, And.right, And.left, Monotone.mem_upperBounds_image, And.intro, monotone_snd
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ lowerBounds (upperBounds s)

Tactic:
exact fun q hq =>
      ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq,
        H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
γ : Type u_3
inst_2 : Preorder γ
g : α × β → γ
hg : Monotone g
d : Set (α × β)
hd : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
⊢ upperBounds (g '' d) = upperBounds (g '' (Prod.fst '' d) ×ˢ (Prod.snd '' d))

Tactic:
le_antisymm
  (upperBounds_mono_of_isCofinalFor (hd.isCofinalFor_fst_image_prod_snd_image.image_of_monotone hg))
  (upperBounds_mono_set (image_mono subset_fst_image_prod_snd_image))

Premises used: upperBounds_mono_set, IsCofinalFor.image_of_monotone, DirectedOn.isCofinalFor_fst_image_prod_snd_image, Set.image_mono, Set.subset_fst_image_prod_snd_image, le_antisymm, upperBounds_mono_of_isCofinalFor
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
⊢ BddAbove s ↔ ∀ (a : α), BddAbove (eval (β := π) a '' s)

Tactic:
⟨fun ⟨f, hf⟩ a ↦ ⟨f a, forall_mem_image.2 fun _ hg ↦ hf hg a⟩,
    fun h ↦ ⟨fun a ↦ (h a).some, fun _ hg a ↦ (h a).some_mem <| mem_image_of_mem _ hg⟩⟩

Premises used: Iff.mpr, Set.Nonempty.some_mem, Function.eval, BddAbove, Set.mem_image_of_mem, _private.0.bddAbove_pi.match_1, Iff.intro, Exists.intro, Set.image, Set.forall_mem_image, Set.Nonempty.some
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
ι : Sort x
π : α → Type u_1
inst : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
simp :
  (∀ (a : α), BddAbove (range (eval (β := π) a ∘ F))) ↔ ∀ (a : α), BddAbove.{u_1} (α := π a) (range fun (i : ι) ↦ F i a)
⊢ BddAbove (range F) ↔ ∀ (a : α), BddAbove.{u_1} (α := π a) (range fun (i : ι) ↦ F i a)

Tactic:
simp only [bddAbove_pi, ← range_comp]

Premises used: Set.range_comp, bddAbove_pi
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
ι : Sort x
π : α → Type u_1
inst : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ (∀ (a : α), BddAbove (range (eval (β := π) a ∘ F))) ↔ ∀ (a : α), BddAbove.{u_1} (α := π a) (range fun (i : ι) ↦ F i a)

Tactic:
rfl
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)

Tactic:
⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩

Premises used: Function.monotone_eval, And.left, Monotone.mem_upperBounds_image, And.intro, Iff.intro
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
refine_1 : ∀ (H : IsLUB s f) (a : α) (b : π a) (hb : b ∈ upperBounds (eval (β := π) a '' s)), f a ≤ b
refine_2 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ upperBounds s
refine_3 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ lowerBounds (upperBounds s)
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)

Tactic:
refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval (β := π) a '' s)
refine_1 : update (β := π) f a b ∈ upperBounds s
⊢ f a ≤ b

Tactic:
suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval (β := π) a '' s)
⊢ update (β := π) f a b ∈ upperBounds s

Tactic:
fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩

Premises used: Iff.mpr, Set.Mem, setOf, upperBounds, Function.eval, le_update_iff, And.left, Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval (β := π) a '' s)
⊢ update (β := π) f a b ∈ upperBounds s

Tactic:
exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩

Premises used: Iff.mpr, Function.eval, le_update_iff, And.left, Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
⊢ f ∈ upperBounds s

Tactic:
fun g hg a => (H a).1 (mem_image_of_mem _ hg)

Premises used: Set.Mem, setOf, upperBounds, Function.eval, And.left, Set.mem_image_of_mem
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
⊢ f ∈ upperBounds s

Tactic:
exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)

Premises used: Function.eval, And.left, Set.mem_image_of_mem
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)

Tactic:
fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)

Premises used: Function.monotone_eval, lowerBounds, Set.Mem, setOf, And.right, Monotone.mem_upperBounds_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)

Tactic:
exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)

Premises used: Function.monotone_eval, And.right, Monotone.mem_upperBounds_image
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
refine_1 : ∀ (H : IsLUB s f) (a : α) (b : π a) (hb : b ∈ upperBounds (eval (β := π) a '' s)), f a ≤ b
refine_2 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ upperBounds s
refine_3 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ lowerBounds (upperBounds s)
refine_2₁ : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ upperBounds s
refine_3₁ refine_3₂ : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ lowerBounds (upperBounds s)
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)

Tactic:
classical
    refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
    · suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
    · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
    · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
s : Set α
x : α
hx : IsGLB (f '' s) (f x)
⊢ IsGLB s x

Tactic:
⟨fun _ hy => hf.1 <| hx.1 <| mem_image_of_mem _ hy, fun _ hy =>
    hf.1 <| hx.2 <| Monotone.mem_lowerBounds_image (fun _ _ => hf.2) hy⟩

Premises used: Iff.mpr, Monotone.mem_lowerBounds_image, IsGreatest, And.right, And.left, Set.mem_image_of_mem, IsGLB, And.intro, Iff.mp
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
hbdd : BddAbove (range g)
obtain : ∀ (C : β) (hC : C ∈ upperBounds (range g)), BddAbove (range f)
⊢ BddAbove (range f)

Tactic:
obtain ⟨C, hC⟩ := hbdd
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
h₁ : C ∈ upperBounds (range f)
⊢ BddAbove (range f)

Tactic:
use C
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
x : α
⊢ f x ≤ C

Tactic:
(h x).trans (hC <| mem_range_self x)

Premises used: Set.mem_range_self, LE.le.trans
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
inst : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
x : α
⊢ f x ≤ C

Tactic:
exact (h x).trans (hC <| mem_range_self x)

Premises used: Set.mem_range_self, LE.le.trans
-- Module: Mathlib.Order.Bounds.Image
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : Preorder β
inst_1 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
change : BddAbove (range (g ∘ f))
⊢ BddAbove.{u_1} (α := γ) (range fun (x : α) ↦ g (f x))

Tactic:
change BddAbove (range (g ∘ f))

Premises used: Function.comp, BddAbove, Set.range