awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ BddBelow (f '' t)

Tactic:
exacts [ht, hs.image f]

Premises used: Set.Nonempty.image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
inr : sInf (f '' s) ≤ sInf (f '' t)
⊢ sInf (f '' s) = sInf (f '' t)

Tactic:
refine le_antisymm ?_ (by gcongr; exacts [ht, hs.image f])

Premises used: le_antisymm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) ≤ sInf (f '' t)

Tactic:
le_csInf ((hs.mono hst).image f) ?_

Premises used: le_csInf, Set.Nonempty.mono, Set.Nonempty.image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
inr : ∀ b ∈ f '' t, sInf (f '' s) ≤ b
⊢ sInf (f '' s) ≤ sInf (f '' t)

Tactic:
refine le_csInf ((hs.mono hst).image f) ?_

Premises used: le_csInf, Set.Nonempty.mono, Set.Nonempty.image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
inr : ∀ a ∈ t, sInf (f '' s) ≤ f a
⊢ ∀ b ∈ f '' t, sInf (f '' s) ≤ b

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Premises used: and_imp, Set.mem_image, forall_exists_index, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
inr : ∀ (x : α) (hxs : x ∈ s) (hxa : x ≤ a), sInf (f '' s) ≤ f a
⊢ sInf (f '' s) ≤ f a

Tactic:
obtain ⟨x, hxs, hxa⟩ := h a ha
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
x : α
hxs : x ∈ s
hxa : x ≤ a
⊢ sInf (f '' s) ≤ f a

Tactic:
csInf_le_of_le (ht.mono (image_mono hst)) ⟨x, hxs, rfl⟩ (hf (hst hxs) ha hxa)

Premises used: Set.image_mono, csInf_le_of_le, BddBelow.mono, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
x : α
hxs : x ∈ s
hxa : x ≤ a
⊢ sInf (f '' s) ≤ f a

Tactic:
exact csInf_le_of_le (ht.mono (image_mono hst)) ⟨x, hxs, rfl⟩ (hf (hst hxs) ha hxa)

Premises used: Set.image_mono, csInf_le_of_le, BddBelow.mono, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddAbove (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
⊢ sSup (f '' s) = sSup (f '' t)

Tactic:
MonotoneOn.csInf_eq_of_subset_of_forall_exists_le (α := αᵒᵈ) (β := βᵒᵈ) ht hf.dual hst h

Premises used: MonotoneOn.csInf_eq_of_subset_of_forall_exists_le, MonotoneOn.dual, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f a

Tactic:
IsGLB.csInf_eq ?_ ((nonempty_Icc.mpr hab).image f)

Premises used: Iff.mpr, Set.nonempty_Icc, IsGLB.csInf_eq, Set.Nonempty.image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
refine : IsGLB (f '' Icc a b) (f a)
⊢ sInf (f '' Icc a b) = f a

Tactic:
refine IsGLB.csInf_eq ?_ ((nonempty_Icc.mpr hab).image f)

Premises used: Iff.mpr, Set.nonempty_Icc, IsGLB.csInf_eq, Set.Nonempty.image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ IsGLB (f '' Icc a b) (f a)

Tactic:
isGLB_iff_le_iff.mpr (fun b' ↦ ⟨?_, ?_⟩)

Premises used: Iff.mpr, isGLB_iff_le_iff, Iff.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
refine_1 : ∀ b' ≤ f a, b' ∈ lowerBounds (f '' Icc a b)
refine_2 : ∀ b' ∈ lowerBounds (f '' Icc a b), b' ≤ f a
⊢ IsGLB (f '' Icc a b) (f a)

Tactic:
refine isGLB_iff_le_iff.mpr (fun b' ↦ ⟨?_, ?_⟩)

Premises used: Iff.mpr, isGLB_iff_le_iff, Iff.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
hb' : b' ≤ f a
x : α
hx : x ∈ Icc a b
⊢ b' ≤ f x

Tactic:
hb'.trans <| h' (left_mem_Icc.mpr hab) hx hx.1

Premises used: Iff.mpr, And.left, Set.left_mem_Icc, LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
hb' : b' ≤ f a
x : α
hx : x ∈ Icc a b
⊢ b' ≤ f x

Tactic:
exact hb'.trans <| h' (left_mem_Icc.mpr hab) hx hx.1

Premises used: Iff.mpr, And.left, Set.left_mem_Icc, LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
hb' : b' ∈ lowerBounds (f '' Icc a b)
⊢ a ∈ Icc a b ∧ f a = f a

Tactic:
simp [hab]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ∈ lowerBounds (f '' Icc a b) → b' ≤ f a

Tactic:
exact fun hb' ↦ hb' ⟨a, by simp [hab]⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
rw : Icc a b = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc a b
⊢ Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)

Tactic:
rw [Icc_toDual]

Premises used: Set.Icc_toDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ Icc a b = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc a b

Tactic:
rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)

Tactic:
have : Icc a b = Icc (α := αᵒᵈ) (toDual b) (toDual a) := by rw [Icc_toDual]; rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
rw :
  ∀ (h' : MonotoneOn f (Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)))
    (this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)),
    sSup (f '' Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)) = f b
⊢ sSup (f '' Icc a b) = f b

Tactic:
rw [this] at h' ⊢
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a))
this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
⊢ sSup (f '' Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)) = f b

Tactic:
h'.dual_right.dual_left.sInf_image_Icc (β := βᵒᵈ) (α := αᵒᵈ) hab

Premises used: AntitoneOn.dual_left, MonotoneOn.sInf_image_Icc, MonotoneOn.dual_right, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a))
this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
⊢ sSup (f '' Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)) = f b

Tactic:
exact h'.dual_right.dual_left.sInf_image_Icc (β := βᵒᵈ) (α := αᵒᵈ) hab
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
rw : Icc a b = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc a b
⊢ Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)

Tactic:
rw [Icc_toDual]

Premises used: Set.Icc_toDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ Icc a b = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc a b

Tactic:
rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)

Tactic:
have : Icc a b = Icc (α := αᵒᵈ) (toDual b) (toDual a) := by rw [Icc_toDual]; rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
rw :
  ∀ (h' : AntitoneOn f (Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)))
    (this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)),
    sInf (f '' Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)) = f b
⊢ sInf (f '' Icc a b) = f b

Tactic:
rw [this] at h' ⊢
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a))
this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
⊢ sInf (f '' Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)) = f b

Tactic:
h'.dual_left.sInf_image_Icc (α := αᵒᵈ) hab

Premises used: AntitoneOn.dual_left, MonotoneOn.sInf_image_Icc, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a))
this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
⊢ sInf (f '' Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)) = f b

Tactic:
exact h'.dual_left.sInf_image_Icc (α := αᵒᵈ) hab
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ sSup (f '' Icc a b) = f a

Tactic:
h'.dual_right.sInf_image_Icc hab

Premises used: AntitoneOn.dual_right, MonotoneOn.sInf_image_Icc, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : ConditionallyCompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sSup (image2 l s t) = l (sSup s) (sSup t)

Tactic:
isLUB_image2_of_isLUB_isLUB h₁ h₂ (isLUB_csSup hs₀ hs₁) (isLUB_csSup ht₀ ht₁)
    |>.csSup_eq (hs₀.image2 ht₀)

Premises used: Set.Nonempty.image2, IsLUB.csSup_eq, isLUB_csSup, isLUB_image2_of_isLUB_isLUB
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : ConditionallyCompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (α := βᵒᵈ) (l a ∘ (⇑ofDual : (a : βᵒᵈ) → β)) ((⇑toDual : (a : β) → βᵒᵈ) ∘ u₂ a)
⊢ s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (image2 l s t) = l (sSup s) (sInf t)

Tactic:
csSup_image2_eq_csSup_csSup (β := βᵒᵈ) h₁ h₂

Premises used: lowerBounds, Set.Mem, csSup_image2_eq_csSup_csSup, setOf, BddBelow, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : ConditionallyCompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ :
  ∀ (b : β),
    GaloisConnection (α := αᵒᵈ) (swap (φ := fun (x : α) (y : β) ↦ γ) l b ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑toDual : (a : α) → αᵒᵈ) ∘ u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
⊢ s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sSup (image2 l s t) = l (sInf s) (sSup t)

Tactic:
csSup_image2_eq_csSup_csSup (α := αᵒᵈ) h₁ h₂

Premises used: lowerBounds, Set.Mem, csSup_image2_eq_csSup_csSup, setOf, BddBelow, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : ConditionallyCompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ :
  ∀ (b : β),
    GaloisConnection (α := αᵒᵈ) (swap (φ := fun (x : α) (y : β) ↦ γ) l b ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑toDual : (a : α) → αᵒᵈ) ∘ u₁ b)
h₂ : ∀ (a : α), GaloisConnection (α := βᵒᵈ) (l a ∘ (⇑ofDual : (a : βᵒᵈ) → β)) ((⇑toDual : (a : β) → βᵒᵈ) ∘ u₂ a)
⊢ s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sSup (image2 l s t) = l (sInf s) (sInf t)

Tactic:
csSup_image2_eq_csSup_csSup (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂

Premises used: lowerBounds, Set.Mem, csSup_image2_eq_csSup_csSup, setOf, BddBelow, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : ConditionallyCompleteLattice γ
s : Set α
t : Set β
u : α → β → γ
l₁ : β → γ → α
l₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (l₁ b) (swap (φ := fun (x : α) (y : β) ↦ γ) u b)
h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddBelow t
⊢ sInf (image2 u s t) = u (sInf s) (sInf t)

Tactic:
isGLB_image2_of_isGLB_isGLB h₁ h₂ (isGLB_csInf hs₀ hs₁) (isGLB_csInf ht₀ ht₁)
    |>.csInf_eq (hs₀.image2 ht₀)

Premises used: Set.Nonempty.image2, IsGLB.csInf_eq, isGLB_csInf, isGLB_image2_of_isGLB_isGLB
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : ConditionallyCompleteLattice γ
s : Set α
t : Set β
u : α → β → γ
l₁ : β → γ → α
l₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (l₁ b) (swap (φ := fun (x : α) (y : β) ↦ γ) u b)
h₂ : ∀ (a : α), GaloisConnection (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ l₂ a) (u a ∘ (⇑ofDual : (a : βᵒᵈ) → β))
⊢ s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (image2 u s t) = u (sInf s) (sSup t)

Tactic:
csInf_image2_eq_csInf_csInf (β := βᵒᵈ) h₁ h₂

Premises used: Set.Mem, setOf, upperBounds, BddAbove, OrderDual, csInf_image2_eq_csInf_csInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : ConditionallyCompleteLattice γ
s : Set α
t : Set β
u : α → β → γ
l₁ : β → γ → α
l₂ : α → γ → β
h₁ :
  ∀ (b : β),
    GaloisConnection (β := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ l₁ b)
      (swap (φ := fun (x : α) (y : β) ↦ γ) u b ∘ (⇑ofDual : (a : αᵒᵈ) → α))
h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)
⊢ s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sInf (image2 u s t) = u (sSup s) (sInf t)

Tactic:
csInf_image2_eq_csInf_csInf (α := αᵒᵈ) h₁ h₂

Premises used: Set.Mem, setOf, upperBounds, BddAbove, OrderDual, csInf_image2_eq_csInf_csInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : ConditionallyCompleteLattice γ
s : Set α
t : Set β
u : α → β → γ
l₁ : β → γ → α
l₂ : α → γ → β
h₁ :
  ∀ (b : β),
    GaloisConnection (β := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ l₁ b)
      (swap (φ := fun (x : α) (y : β) ↦ γ) u b ∘ (⇑ofDual : (a : αᵒᵈ) → α))
h₂ : ∀ (a : α), GaloisConnection (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ l₂ a) (u a ∘ (⇑ofDual : (a : βᵒᵈ) → β))
⊢ s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sInf (image2 u s t) = u (sSup s) (sSup t)

Tactic:
csInf_image2_eq_csInf_csInf (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂

Premises used: Set.Mem, setOf, upperBounds, BddAbove, OrderDual, csInf_image2_eq_csInf_csInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
inst : CompleteLattice α
s : Set (WithBot α)
x : WithBot α
hsa : x ∈ upperBounds s
h : s = ∅
⊢ ⊥ ≤ x

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
inst : CompleteLattice α
s : Set (WithBot α)
x : WithBot α
has : x ∈ lowerBounds s
h : s = ∅
⊢ x ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
inl : ∀ (h : S = ∅), sSup S ≤ a
inr : ∀ (h : S.Nonempty), sSup S ≤ a
⊢ sSup S ≤ a

Tactic:
rcases S.eq_empty_or_nonempty with h | h

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S = ∅
inl :
  (if ⊤ ∈ S then ⊤
    else
      if BddAbove (α := WithBot α) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) then
        (↑(sSup ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))
      else ⊤) ≤
    a
⊢ sSup S ≤ a

Tactic:
change ite _ _ _ ≤ a

Premises used: ite
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S = ∅
⊢ (if ⊤ ∈ S then ⊤
    else
      if BddAbove (α := WithBot α) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) then
        (↑(sSup ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))
      else ⊤) ≤
    a

Tactic:
simp [h]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S.Nonempty
⊢ sSup S ≤ a

Tactic:
(WithTop.isLUB_sSup' h).2 ha

Premises used: And.right, WithTop.isLUB_sSup'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S.Nonempty
⊢ sSup S ≤ a

Tactic:
exact (WithTop.isLUB_sSup' h).2 ha

Premises used: And.right, WithTop.isLUB_sSup'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
simp :
  (if S ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))) ≤
    a
⊢ (if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤
    else (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))) ≤
    a

Tactic:
simp only [OrderBot.bddBelow, not_true_eq_false, or_false]

Premises used: not_true_eq_false, or_false, OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
pos : ∀ (h₁ : S ⊆ {⊤}), ⊤ ≤ a
neg : ∀ (h₁ : ¬S ⊆ {⊤}), (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ≤ a
⊢ (if S ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))) ≤
    a

Tactic:
split_ifs with h₁
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : S ⊆ {⊤}
pos : ∀ (haS : ⊤ ∈ S), LE.le.{u_5} (α := WithTop (WithBot α)) ⊤ ⊤
pos₁ : ∀ (a : WithBot α) (haS : (↑a : WithTop (WithBot α)) ∈ S), ⊤ ≤ (↑a : WithTop (WithBot α))
⊢ ⊤ ≤ a

Tactic:
cases a
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : S ⊆ {⊤}
haS : ⊤ ∈ S
⊢ LE.le.{u_5} (α := WithTop (WithBot α)) ⊤ ⊤

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : S ⊆ {⊤}
haS : ⊤ ∈ S
⊢ LE.le.{u_5} (α := WithTop (WithBot α)) ⊤ ⊤

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : S ⊆ {⊤}
a : WithBot α
haS : (↑a : WithTop (WithBot α)) ∈ S
⊢ ⊤ ≤ (↑a : WithTop (WithBot α))

Tactic:
cases h₁ haS