awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ BddAbove (range (g ∘ f))

Tactic:
simpa only [Set.range_comp] using hg.map_bddAbove hf

Premises used: Set.range_comp, Monotone.map_bddAbove
-- Module: Mathlib.Order.Bounds.Lattice
Goal:
α : Type u_1
inst : Preorder α
⊢ GaloisConnection.{u_1, u_1} (α := Set α) (β := (Set α)ᵒᵈ)
    ((⇑OrderDual.toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ upperBounds)
    (lowerBounds ∘ (⇑OrderDual.ofDual : (a : (Set α)ᵒᵈ) → Set α))

Tactic:
simpa [GaloisConnection, subset_def, mem_upperBounds, mem_lowerBounds]
    using fun S T ↦ forall₂_comm

Premises used: Set.subset_def, mem_lowerBounds, forall₂_comm, mem_upperBounds, GaloisConnection
-- Module: Mathlib.Order.Bounds.Lattice
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (upperBounds (⋃ (i : ι), s i)) (⋂ (i : ι), upperBounds (s i))

Tactic:
gc_upperBounds_lowerBounds.l_iSup

Premises used: iInf, Set.Mem, Set.iInter, gc_upperBounds_lowerBounds, setOf, upperBounds, GaloisConnection.l_iSup, OrderDual, Set.iUnion
-- Module: Mathlib.Order.Bounds.Lattice
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (lowerBounds (⋃ (i : ι), s i)) (⋂ (i : ι), lowerBounds (s i))

Tactic:
gc_upperBounds_lowerBounds.u_iInf

Premises used: iInf, lowerBounds, Set.Mem, iSup, Set.iInter, gc_upperBounds_lowerBounds, setOf, GaloisConnection.u_iInf, OrderDual, Set.iUnion
-- Module: Mathlib.Order.Bounds.Lattice
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ IsLUB (range u) c ↔ IsLUB (⋃ (i : ι), s i) c

Tactic:
isLUB_congr ?_

Premises used: isLUB_congr
-- Module: Mathlib.Order.Bounds.Lattice
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
refine : upperBounds (range u) = upperBounds (⋃ (i : ι), s i)
⊢ IsLUB (range u) c ↔ IsLUB (⋃ (i : ι), s i) c

Tactic:
refine isLUB_congr ?_

Premises used: isLUB_congr
-- Module: Mathlib.Order.Bounds.Lattice
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
simp_rw : Eq.{u_1 + 1} (α := Set α) (upperBounds (⋃ (i : ι), {u i})) (upperBounds (⋃ (i : ι), s i))
simp_rw₁ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), upperBounds {u i}) (⋂ (i : ι), upperBounds (s i))
simp_rw₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), Ici (u i)) (⋂ (i : ι), upperBounds (s i))
⊢ upperBounds (range u) = upperBounds (⋃ (i : ι), s i)

Tactic:
simp_rw [range_eq_iUnion, upperBounds_iUnion, upperBounds_singleton, (hs _).upperBounds_eq]

Premises used: upperBounds_iUnion, IsLUB.upperBounds_eq, upperBounds_singleton, Set.range_eq_iUnion
-- Module: Mathlib.Order.Bounds.Lattice
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ IsGLB (range u) c ↔ IsGLB (⋃ (i : ι), s i) c

Tactic:
isGLB_congr ?_

Premises used: isGLB_congr
-- Module: Mathlib.Order.Bounds.Lattice
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
refine : lowerBounds (range u) = lowerBounds (⋃ (i : ι), s i)
⊢ IsGLB (range u) c ↔ IsGLB (⋃ (i : ι), s i) c

Tactic:
refine isGLB_congr ?_

Premises used: isGLB_congr
-- Module: Mathlib.Order.Bounds.Lattice
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
simp_rw : Eq.{u_1 + 1} (α := Set α) (lowerBounds (⋃ (i : ι), {u i})) (lowerBounds (⋃ (i : ι), s i))
simp_rw₁ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), lowerBounds {u i}) (⋂ (i : ι), lowerBounds (s i))
simp_rw₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), Iic (u i)) (⋂ (i : ι), lowerBounds (s i))
⊢ lowerBounds (range u) = lowerBounds (⋃ (i : ι), s i)

Tactic:
simp_rw [range_eq_iUnion, lowerBounds_iUnion, lowerBounds_singleton, (hs _).lowerBounds_eq]

Premises used: lowerBounds_singleton, lowerBounds_iUnion, Set.range_eq_iUnion, IsGLB.lowerBounds_eq
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set α
⊢ Eq.{u_2 + 1} (α := Set β) (upperBounds ((⇑f : (a : α) → β) '' s)) ((⇑f : (a : α) → β) '' upperBounds s)

Tactic:
Subset.antisymm
    (fun x hx =>
      ⟨f.symm x, fun _ hy => f.le_symm_apply.2 (hx <| mem_image_of_mem _ hy), f.apply_symm_apply x⟩)
    f.monotone.image_upperBounds_subset_upperBounds_image

Premises used: Set.Subset.antisymm, Iff.mpr, Monotone.image_upperBounds_subset_upperBounds_image, OrderIso.monotone, OrderIso.apply_symm_apply, OrderIso.symm, Set.mem_image_of_mem, And.intro, Exists.intro, OrderIso.le_symm_apply, DFunLike.coe
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set α
⊢ Eq.{u_2 + 1} (α := Set β) (lowerBounds ((⇑f : (a : α) → β) '' s)) ((⇑f : (a : α) → β) '' lowerBounds s)

Tactic:
@upperBounds_image αᵒᵈ βᵒᵈ _ _ f.dual _

Premises used: lowerBounds, Set.Mem, setOf, OrderIso.dual, OrderIso.upperBounds_image, OrderDual
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB ((⇑f : (a : α) → β) '' s) x
⊢ ∀ {x y : α}, LE.le.{u_2} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) x : β) ↔ y ≤ x

Tactic:
simp
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB s ((f.symm : (a : β) → α) x)
⊢ ∀ {x y : β}, LE.le.{u_1} (α := α) ((f.symm : (a : β) → α) y : α) ((f.symm : (a : β) → α) x : α) ↔ y ≤ x

Tactic:
simp
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set α
x : α
rw : IsLUB s ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) ↔ IsLUB s x
rw₁ rw₂ : IsLUB s x ↔ IsLUB s x
⊢ IsLUB.{u_2} (α := β) ((⇑f : (a : α) → β) '' s : Set β) ((f : (a : α) → β) x : β) ↔ IsLUB s x

Tactic:
rw [isLUB_image, f.symm_apply_apply]

Premises used: OrderIso.isLUB_image, OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set α
x : β
⊢ IsGLB ((⇑f : (a : α) → β) '' s) x ↔ IsGLB s ((f.symm : (a : β) → α) x)

Tactic:
f.dual.isLUB_image

Premises used: OrderIso.isLUB_image, lowerBounds, Set.Mem, setOf, upperBounds, OrderIso.dual, IsGreatest, IsGLB, OrderDual
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsGLB.{u_2} (α := β) ((⇑f : (a : α) → β) '' s : Set β) ((f : (a : α) → β) x : β) ↔ IsGLB s x

Tactic:
f.dual.isLUB_image'

Premises used: OrderIso.isLUB_image', lowerBounds, Set.Mem, setOf, upperBounds, OrderIso.dual, IsGreatest, IsGLB, OrderDual
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set β
x : α
rw : IsLUB ((⇑f.symm.symm : (a : α) → β) ⁻¹' s) x ↔ IsLUB s ((f.symm.symm : (a : α) → β) x)
rw₁ : IsLUB ((⇑f.symm : (a : β) → α) '' s) x ↔ IsLUB s ((f.symm.symm : (a : α) → β) x)
rw₂ rw₃ : IsLUB s ((f.symm.symm : (a : α) → β) x) ↔ IsLUB s ((f.symm.symm : (a : α) → β) x)
⊢ IsLUB ((⇑f : (a : α) → β) ⁻¹' s) x ↔ IsLUB s ((f : (a : α) → β) x)

Tactic:
rw [← f.symm_symm, ← image_eq_preimage_symm, isLUB_image]

Premises used: OrderIso.isLUB_image, OrderIso.symm_symm, OrderIso.image_eq_preimage_symm
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set β
x : β
rw : IsLUB s ((f : (a : α) → β) ((f.symm : (a : β) → α) x : α)) ↔ IsLUB s x
rw₁ rw₂ : IsLUB s x ↔ IsLUB s x
⊢ IsLUB.{u_1} (α := α) ((⇑f : (a : α) → β) ⁻¹' s : Set α) ((f.symm : (a : β) → α) x : α) ↔ IsLUB s x

Tactic:
rw [isLUB_preimage, f.apply_symm_apply]

Premises used: OrderIso.apply_symm_apply, OrderIso.isLUB_preimage
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set β
x : α
⊢ IsGLB ((⇑f : (a : α) → β) ⁻¹' s) x ↔ IsGLB s ((f : (a : α) → β) x)

Tactic:
f.dual.isLUB_preimage

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, OrderIso.dual, IsGreatest, OrderIso.isLUB_preimage, IsGLB, OrderDual
-- Module: Mathlib.Order.Bounds.OrderIso
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsGLB.{u_1} (α := α) ((⇑f : (a : α) → β) ⁻¹' s : Set α) ((f.symm : (a : β) → α) x : α) ↔ IsGLB s x

Tactic:
f.dual.isLUB_preimage'

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, OrderIso.dual, IsGreatest, IsGLB, OrderDual, OrderIso.isLUB_preimage'
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ Ici x
⊢ f y ∈ Ici x

Tactic:
le_trans hy (le_map _)

Premises used: Set.Ici, Set.Mem, setOf, le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ Ici x
⊢ f y ∈ Ici x

Tactic:
exact le_trans hy (le_map _)

Premises used: le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ Ici x
have : ∀ (y : α) (hy : y ∈ c.carrier), cSup c ∈ Ici x
⊢ cSup c ∈ Ici x

Tactic:
have ⟨y, hy⟩ := c.Nonempty'
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ Ici x
y : α
hy : y ∈ c.carrier
⊢ cSup c ∈ Ici x

Tactic:
le_trans (hc hy) (le_cSup _ _ hy)

Premises used: Set.Ici, Set.Mem, setOf, ChainCompletePartialOrder.le_cSup, le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ Ici x
y : α
hy : y ∈ c.carrier
⊢ cSup c ∈ Ici x

Tactic:
exact le_trans (hc hy) (le_cSup _ _ hy)

Premises used: ChainCompletePartialOrder.le_cSup, le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
left : x ∈ bot x f
right : x ∈ lowerBounds (bot x f)
⊢ IsLeast (bot x f) x

Tactic:
constructor
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ bot x f

Tactic:
fun _ h ↦ h.base_isLeast.1

Premises used: Set.Mem, setOf, ChainCompletePartialOrder.IsAdmissible.base_isLeast, And.left, Set.sInter
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ bot x f

Tactic:
exact fun _ h ↦ h.base_isLeast.1
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
⊢ x ≤ y

Tactic:
hy (Ici x) (ici_isAdmissible le_map)

Premises used: Set.Ici, Set.Mem, setOf, ChainCompletePartialOrder.ici_isAdmissible
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
⊢ x ≤ y

Tactic:
exact hy (Ici x) (ici_isAdmissible le_map)

Premises used: Set.Ici, ChainCompletePartialOrder.ici_isAdmissible
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsAdmissible x f s} s
⊢ f y ∈ s

Tactic:
hs.image_self_subset_self ⟨y, ⟨mem_sInter.1 hy _ hs, rfl⟩⟩

Premises used: And.intro, Set.mem_sInter, Exists.intro, Iff.mp, ChainCompletePartialOrder.IsAdmissible.image_self_subset_self, rfl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsAdmissible x f s} s
⊢ f y ∈ s

Tactic:
exact hs.image_self_subset_self ⟨y, ⟨mem_sInter.1 hy _ hs, rfl⟩⟩

Premises used: And.intro, Set.mem_sInter, Exists.intro, Iff.mp, ChainCompletePartialOrder.IsAdmissible.image_self_subset_self, rfl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ bot x f
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsAdmissible x f s} s
⊢ cSup c ∈ s

Tactic:
hs.cSup_mem c (subset_trans hc (sInter_subset_of_mem hs))

Premises used: subset_trans, Set.sInter_subset_of_mem, ChainCompletePartialOrder.IsAdmissible.cSup_mem
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ bot x f
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsAdmissible x f s} s
⊢ cSup c ∈ s

Tactic:
exact hs.cSup_mem c (subset_trans hc (sInter_subset_of_mem hs))

Premises used: subset_trans, Set.sInter_subset_of_mem, ChainCompletePartialOrder.IsAdmissible.cSup_mem
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
h : y ∈ bot x f
⊢ f y ∈ bot x f

Tactic:
(bot_isAdmissible le_map).image_self_subset_self <| mem_image_of_mem f h

Premises used: ChainCompletePartialOrder.bot_isAdmissible, Set.mem_image_of_mem, ChainCompletePartialOrder.IsAdmissible.image_self_subset_self
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
rw : {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} ⊆ bot x f
rw₁ : IsAdmissible x f {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} = bot x f

Tactic:
rw [← subset_bot_iff]

Premises used: ChainCompletePartialOrder.subset_bot_iff
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} ⊆ bot x f

Tactic:
apply sep_subset

Premises used: Set.sep_subset
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
base_isLeast : IsLeast {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x
image_self_subset_self : f '' {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} ⊆ {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
cSup_mem :
  ∀ (c : NonemptyChain α),
    (↑c : Set α) ⊆ {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} →
      Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} (cSup c)
⊢ IsAdmissible x f {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

Tactic:
apply IsAdmissible.mk

Premises used: ChainCompletePartialOrder.IsAdmissible.mk
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
base_isLeast : Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x
base_isLeast₁ : Membership.mem (γ := Set α) (lowerBounds {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}) x
⊢ IsLeast {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x

Tactic:
constructor
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
base_isLeast : x ∈ bot x f
base_isLeast₁ : x ≤ y ∨ f y ≤ x
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x

Tactic:
constructor
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ∈ bot x f

Tactic:
(bot_isAdmissible le_map).base_isLeast.1

Premises used: ChainCompletePartialOrder.IsAdmissible.base_isLeast, ChainCompletePartialOrder.bot_isAdmissible, And.left
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ∈ bot x f

Tactic:
exact (bot_isAdmissible le_map).base_isLeast.1

Premises used: ChainCompletePartialOrder.IsAdmissible.base_isLeast, ChainCompletePartialOrder.bot_isAdmissible, And.left
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ≤ y ∨ f y ≤ x

Tactic:
Or.inl ((bot_isAdmissible le_map).base_isLeast.2 hy.mem_bot)

Premises used: ChainCompletePartialOrder.IsAdmissible.base_isLeast, ChainCompletePartialOrder.bot_isAdmissible, And.right, ChainCompletePartialOrder.IsExtremePt.mem_bot, Or.inl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ≤ y ∨ f y ≤ x

Tactic:
exact Or.inl ((bot_isAdmissible le_map).base_isLeast.2 hy.mem_bot)

Premises used: ChainCompletePartialOrder.IsAdmissible.base_isLeast, ChainCompletePartialOrder.bot_isAdmissible, And.right, ChainCompletePartialOrder.IsExtremePt.mem_bot, Or.inl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ Membership.mem (γ := Set α) (lowerBounds {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}) x

Tactic:
fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1

Premises used: lowerBounds, Set.Mem, setOf, ChainCompletePartialOrder.IsAdmissible.base_isLeast, ChainCompletePartialOrder.bot_isAdmissible, And.right, And.left
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ Membership.mem (γ := Set α) (lowerBounds {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}) x

Tactic:
exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1

Premises used: ChainCompletePartialOrder.IsAdmissible.base_isLeast, ChainCompletePartialOrder.bot_isAdmissible, And.right
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy : z ≤ y
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} (f z)

Tactic:
⟨map_mem_bot le_map hz, ?_⟩

Premises used: Set.Mem, setOf, ChainCompletePartialOrder.map_mem_bot, And.intro
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy : z ≤ y
image_self_subset_self : f z ≤ y ∨ f y ≤ f z
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} (f z)

Tactic:
refine ⟨map_mem_bot le_map hz, ?_⟩
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} (f z)

Tactic:
⟨map_mem_bot le_map hz, ?_⟩

Premises used: Set.Mem, setOf, ChainCompletePartialOrder.map_mem_bot, And.intro
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
image_self_subset_self : f z ≤ y ∨ f y ≤ f z
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} (f z)

Tactic:
refine ⟨map_mem_bot le_map hz, ?_⟩
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy : z ≤ y
image_self_subset_self : ∀ (hzy : z < y), f z ≤ y ∨ f y ≤ f z
image_self_subset_self₁ : ∀ (hy : IsExtremePt x f z) (hzy : z ≤ z), f z ≤ z ∨ f z ≤ f z
⊢ f z ≤ y ∨ f y ≤ f z

Tactic:
rcases le_iff_lt_or_eq.1 hzy with (hzy | rfl)

Premises used: le_iff_lt_or_eq, Iff.mp, rfl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy_1 : z ≤ y
hzy : z < y
image_self_subset_self : f z ≤ y
⊢ f z ≤ y ∨ f y ≤ f z

Tactic:
left
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy_1 : z ≤ y
hzy : z < y
⊢ f z ≤ y

Tactic:
hy.map_le_of_mem_of_lt hz hzy

Premises used: ChainCompletePartialOrder.IsExtremePt.map_le_of_mem_of_lt
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy_1 : z ≤ y
hzy : z < y
⊢ f z ≤ y

Tactic:
exact hy.map_le_of_mem_of_lt hz hzy

Premises used: ChainCompletePartialOrder.IsExtremePt.map_le_of_mem_of_lt
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
image_self_subset_self : f z ≤ f z
⊢ f z ≤ z ∨ f z ≤ f z

Tactic:
right
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ f z

Tactic:
le_refl _

Premises used: le_refl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ f z

Tactic:
exact le_refl _

Premises used: le_refl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
image_self_subset_self : f y ≤ f z
⊢ f z ≤ y ∨ f y ≤ f z

Tactic:
right
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f y ≤ f z

Tactic:
le_trans hyz (le_map z)

Premises used: le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f y ≤ f z

Tactic:
exact le_trans hyz (le_map z)

Premises used: le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} (cSup c)

Tactic:
⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (sep_subset _ _)), ?_⟩

Premises used: Set.Mem, subset_trans, setOf, ChainCompletePartialOrder.bot_isAdmissible, ChainCompletePartialOrder.IsAdmissible.cSup_mem, And.intro, Set.sep_subset
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
cSup_mem : cSup c ≤ y ∨ f y ≤ cSup c
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} (cSup c)

Tactic:
refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (sep_subset _ _)), ?_⟩