awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)}
pos : ∀ (h : ∀ z ∈ c, z ≤ y), cSup c ≤ y ∨ f y ≤ cSup c
neg : ∀ (h : ∃ z ∈ c, ¬z ≤ y), cSup c ≤ y ∨ f y ≤ cSup c
⊢ cSup c ≤ y ∨ f y ≤ cSup c

Tactic:
by_cases! h : ∀ z ∈ c, z ≤ y
-- 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)}
h : ∀ z ∈ c, z ≤ y
pos : cSup c ≤ y
⊢ cSup c ≤ y ∨ f y ≤ cSup c

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
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
h : ∀ z ∈ c, z ≤ y
⊢ cSup c ≤ y

Tactic:
apply cSup_le c y h

Premises used: ChainCompletePartialOrder.cSup_le
-- 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)}
h : ∃ z ∈ c, ¬z ≤ y
neg : ∀ (z : α) (hz : z ∈ c) (hzy : ¬z ≤ y), cSup c ≤ y ∨ f y ≤ cSup c
⊢ cSup c ≤ y ∨ f y ≤ cSup c

Tactic:
rcases h with ⟨z, hz, hzy⟩
-- 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)}
z : α
hz : z ∈ c
hzy : ¬z ≤ y
⊢ f y ≤ z

Tactic:
have h' := Or.resolve_left (hc hz).2 hzy
-- 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)}
z : α
hz : z ∈ c
hzy : ¬z ≤ y
h' : f y ≤ z
neg : f y ≤ cSup c
⊢ cSup c ≤ y ∨ f y ≤ cSup c

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
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
z : α
hz : z ∈ c
hzy : ¬z ≤ y
h' : f y ≤ z
⊢ f y ≤ cSup c

Tactic:
apply le_trans h' (le_cSup _ _ hz)

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
base_isLeast : IsLeast {y : α | IsExtremePt x f y} x
image_self_subset_self : f '' {y : α | IsExtremePt x f y} ⊆ {y : α | IsExtremePt x f y}
cSup_mem :
  ∀ (c : NonemptyChain α),
    (↑c : Set α) ⊆ {y : α | IsExtremePt x f y} → Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} (cSup c)
⊢ IsAdmissible x f {y : α | IsExtremePt x f y}

Tactic:
apply IsAdmissible.mk

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

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

Tactic:
⟨(bot_isAdmissible le_map).base_isLeast.1, ?_⟩

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

Tactic:
refine ⟨(bot_isAdmissible le_map).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
hyx : y < x
base_isLeast : False
⊢ f y ≤ x

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

Tactic:
lt_irrefl x (lt_of_le_of_lt ((bot_isAdmissible le_map).base_isLeast.2 hy) hyx)

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

Tactic:
exact lt_irrefl x (lt_of_le_of_lt ((bot_isAdmissible le_map).base_isLeast.2 hy) hyx)

Premises used: lt_of_le_of_lt, lt_irrefl, ChainCompletePartialOrder.IsAdmissible.base_isLeast, ChainCompletePartialOrder.bot_isAdmissible, And.right
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ Membership.mem (γ := Set α) (lowerBounds {y : α | IsExtremePt x f y}) 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, ChainCompletePartialOrder.IsExtremePt.mem_bot
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ Membership.mem (γ := Set α) (lowerBounds {y : α | IsExtremePt x f y}) 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 : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y
⊢ Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} (f y)

Tactic:
⟨map_mem_bot le_map hy.mem_bot, ?_⟩

Premises used: Set.Mem, setOf, ChainCompletePartialOrder.map_mem_bot, ChainCompletePartialOrder.IsExtremePt.mk, ChainCompletePartialOrder.IsExtremePt.mem_bot
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y
image_self_subset_self : ∀ {z : α} (h : z ∈ bot x f) (h' : z < f y), f z ≤ f y
⊢ Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} (f y)

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

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

Tactic:
rw [← bot_eq_of_le_or_map_le le_map hy] at hz'

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

Tactic:
rcases hz' with ⟨_, (hz' | hz')⟩
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y
z : α
hz : z ∈ bot x f
hzy : z < f y
left : z ∈ bot x f
hz' : z ≤ y
image_self_subset_self : ∀ (hz' : z < y), f z ≤ f y
image_self_subset_self₁ :
  ∀ (hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} z) (hzy : z < f z) (hz' : z ≤ z), f z ≤ f z
⊢ f z ≤ f y

Tactic:
rcases le_iff_lt_or_eq.1 hz' with (hz' | rfl)

Premises used: le_iff_lt_or_eq, Iff.mp, rfl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y
z : α
hz : z ∈ bot x f
hzy : z < f y
left : z ∈ bot x f
hz'_1 : z ≤ y
hz' : z < y
⊢ f z ≤ f y

Tactic:
le_trans (hy.map_le_of_mem_of_lt hz hz') (le_map y)

Premises used: ChainCompletePartialOrder.IsExtremePt.map_le_of_mem_of_lt, le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y
z : α
hz : z ∈ bot x f
hzy : z < f y
left : z ∈ bot x f
hz'_1 : z ≤ y
hz' : z < y
⊢ f z ≤ f y

Tactic:
exact le_trans (hy.map_le_of_mem_of_lt hz hz') (le_map y)

Premises used: ChainCompletePartialOrder.IsExtremePt.map_le_of_mem_of_lt, le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz left : z ∈ bot x f
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} z
hzy : z < f z
hz' : z ≤ z
⊢ f z ≤ f z

Tactic:
le_refl (f z)

Premises used: le_refl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz left : z ∈ bot x f
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} z
hzy : z < f z
hz' : z ≤ z
⊢ f z ≤ f z

Tactic:
exact le_refl (f z)

Premises used: le_refl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y
z : α
hz : z ∈ bot x f
hzy : z < f y
left : z ∈ bot x f
hz' : f y ≤ z
image_self_subset_self : False
⊢ f z ≤ f y

Tactic:
exfalso
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y
z : α
hz : z ∈ bot x f
hzy : z < f y
left : z ∈ bot x f
hz' : f y ≤ z
⊢ False

Tactic:
lt_irrefl z (lt_of_lt_of_le hzy hz')

Premises used: lt_irrefl, lt_of_lt_of_le
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y
z : α
hz : z ∈ bot x f
hzy : z < f y
left : z ∈ bot x f
hz' : f y ≤ z
⊢ False

Tactic:
exact lt_irrefl z (lt_of_lt_of_le hzy hz')

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

Tactic:
⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (fun _ h ↦ h.mem_bot)), ?_⟩

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

Tactic:
refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (fun _ h ↦ h.mem_bot)), ?_⟩
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
by_contra! : ∀ (h : ∀ (z : α) (_ : z ∈ c), f z ≤ y), False
⊢ ∃ z ∈ c, ¬f z ≤ y

Tactic:
by_contra! h
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
h : ∀ (z : α) (_ : z ∈ c), f z ≤ y
apply : cSup c ≤ y
⊢ False

Tactic:
apply lt_irrefl y (lt_of_lt_of_le hy' ?_)

Premises used: lt_irrefl, lt_of_lt_of_le
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
h : ∀ (z : α) (_ : z ∈ c), f z ≤ y
a : ∀ y_1 ∈ c.carrier, y_1 ≤ y
⊢ cSup c ≤ y

Tactic:
apply cSup_le

Premises used: ChainCompletePartialOrder.cSup_le
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
h : ∀ (z : α) (_ : z ∈ c), f z ≤ y
z : α
hz : z ∈ c.carrier
⊢ z ≤ y

Tactic:
le_trans (le_map z) (h z hz)

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 α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
h : ∀ (z : α) (_ : z ∈ c), f z ≤ y
z : α
hz : z ∈ c.carrier
⊢ z ≤ y

Tactic:
exact le_trans (le_map z) (h z hz)

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 α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
cSup_mem : ∀ (z : α) (hz : z ∈ c) (hzy : ¬f z ≤ y), f y ≤ cSup c
⊢ f y ≤ cSup c

Tactic:
obtain ⟨z, hz, hzy⟩ : ∃ z ∈ c, ¬ (f z ≤ y) := by
      by_contra! h
      apply lt_irrefl y (lt_of_lt_of_le hy' ?_)
      apply cSup_le
      intro z hz
      exact le_trans (le_map z) (h z hz)
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
⊢ Membership.mem (γ := Set α) {z_1 : α | z_1 ∈ bot x f ∧ (z_1 ≤ z ∨ f z ≤ z_1)} y

Tactic:
rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hy

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

Tactic:
rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hy

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

Tactic:
rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hy

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

Tactic:
Or.resolve_right hy.2 hzy

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

Tactic:
exact Or.resolve_right hy.2 hzy

Premises used: And.right, Or.resolve_right
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
⊢ y ≤ z

Tactic:
have h : y ≤ z := by
      rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hy
      exact Or.resolve_right hy.2 hzy
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
h : y ≤ z
cSup_mem : ∀ (hyz : y < z), f y ≤ cSup c
cSup_mem₁ : ∀ (hz : y ∈ c) (hzy : ¬f y ≤ y) (h : y ≤ y), f y ≤ cSup c
⊢ f y ≤ cSup c

Tactic:
obtain hyz | rfl := le_iff_lt_or_eq.1 h

Premises used: le_iff_lt_or_eq, Iff.mp, rfl
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
h : y ≤ z
hyz : y < z
⊢ f y ≤ cSup c

Tactic:
le_trans ((hc hz).map_le_of_mem_of_lt hy hyz) (le_cSup _ _ hz)

Premises used: ChainCompletePartialOrder.le_cSup, ChainCompletePartialOrder.IsExtremePt.map_le_of_mem_of_lt, 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 α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
h : y ≤ z
hyz : y < z
⊢ f y ≤ cSup c

Tactic:
exact le_trans ((hc hz).map_le_of_mem_of_lt hy hyz) (le_cSup _ _ hz)

Premises used: ChainCompletePartialOrder.le_cSup, ChainCompletePartialOrder.IsExtremePt.map_le_of_mem_of_lt, 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 α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
⊢ cSup c ∈ bot x f

Tactic:
have hc' := (bot_isAdmissible le_map).cSup_mem _ (subset_trans hc fun _ h ↦ h.mem_bot)
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc' : cSup c ∈ bot x f
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} (cSup c)

Tactic:
rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hc'

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

Tactic:
apply hc'.2.resolve_left

Premises used: Or.resolve_left, And.right
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ {y : α | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc'_1 : Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} (cSup c)
hc' : cSup c ≤ y
⊢ False

Tactic:
lt_irrefl y (lt_of_lt_of_le hy' hc')

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

Tactic:
exact lt_irrefl y (lt_of_lt_of_le hy' hc')

Premises used: lt_irrefl, lt_of_lt_of_le
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
rw : {y : α | IsExtremePt x f y} ⊆ bot x f
rw₁ : IsAdmissible x f {y : α | IsExtremePt x f y}
⊢ {y : α | IsExtremePt x f y} = 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 : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ {y : α | IsExtremePt x f y} ⊆ bot x f

Tactic:
fun _ h ↦ h.mem_bot

Premises used: Set.Subset, ChainCompletePartialOrder.IsExtremePt.mem_bot
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ {y : α | IsExtremePt x f y} ⊆ bot x f

Tactic:
exact fun _ h ↦ h.mem_bot
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsAdmissible x f {y : α | IsExtremePt x f y}

Tactic:
setOf_isExtremePt_isAdmissible le_map

Premises used: ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_isAdmissible
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsAdmissible x f {y : α | IsExtremePt x f y}

Tactic:
exact setOf_isExtremePt_isAdmissible le_map

Premises used: ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_isAdmissible
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
rw : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y ↔ IsExtremePt x f y
rw₁ rw₂ : IsExtremePt x f y ↔ IsExtremePt x f y
⊢ y ∈ bot x f ↔ IsExtremePt x f y

Tactic:
rw [← setOf_isExtremePt_eq_bot le_map, mem_setOf]

Premises used: Set.mem_setOf, ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_eq_bot
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
z : α
hz : z ∈ bot x f
_ : y ≠ z → (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
⊢ y ≠ z → (fun (x y : α) ↦ (fun (x1 x2 : α) ↦ x1 ≤ x2) x y ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) y x) y z

Tactic:
_