awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
left : x ∈ bot x f
⊢ IsLeast (bot x f) x
have right : x ∈ lowerBounds (bot x f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
have rw : {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} ⊆ bot x f
Tactic: rw [← subset_bot_iff]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} = bot x f
have rw₁ : IsAdmissible x f {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
Tactic: rw [← subset_bot_iff]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ IsAdmissible x f {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
have base_isLeast : IsLeast {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x
Tactic: apply IsAdmissible.mk
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ IsAdmissible x f {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
have 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)}
Tactic: apply IsAdmissible.mk
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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)}
⊢ IsAdmissible x f {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
have 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)
Tactic: apply IsAdmissible.mk
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ IsLeast {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x
have base_isLeast : Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ IsLeast {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x
have base_isLeast₁ : Membership.mem (γ := Set α) (lowerBounds {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x
have base_isLeast : x ∈ bot x f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} x
have base_isLeast₁ : x ≤ y ∨ f y ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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)
have image_self_subset_self : f z ≤ y ∨ f y ≤ f z
Tactic: refine ⟨map_mem_bot le_map hz, ?_⟩
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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)
have image_self_subset_self : f z ≤ y ∨ f y ≤ f z
Tactic: refine ⟨map_mem_bot le_map hz, ?_⟩
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f z ≤ y ∨ f y ≤ f z
have image_self_subset_self : ∀ (hzy : z < y), f z ≤ y ∨ f y ≤ f z
Tactic: rcases le_iff_lt_or_eq.1 hzy with (hzy | rfl)
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f z ≤ y ∨ f y ≤ f z
have image_self_subset_self₁ : ∀ (hy : IsExtremePt x f z) (hzy : z ≤ z), f z ≤ z ∨ f z ≤ f z
Tactic: rcases le_iff_lt_or_eq.1 hzy with (hzy | rfl)
Cleared hypotheses: y, hy, hzy
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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 ∨ f y ≤ f z
have image_self_subset_self : f z ≤ y
Tactic: left
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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 ≤ z ∨ f z ≤ f z
have image_self_subset_self : f z ≤ f z
Tactic: right
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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 z ≤ y ∨ f y ≤ f z
have image_self_subset_self : f y ≤ f z
Tactic: right
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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)
have cSup_mem : cSup c ≤ y ∨ f y ≤ cSup c
Tactic: refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (sep_subset _ _)), ?_⟩
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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 c ≤ y ∨ f y ≤ cSup c
have pos : ∀ (h : ∀ z ∈ c, z ≤ y), cSup c ≤ y ∨ f y ≤ cSup c
Tactic: by_cases! h : ∀ z ∈ c, z ≤ y
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ cSup c ≤ y ∨ f y ≤ cSup c
have neg : ∀ (h : ∃ z ∈ c, ¬z ≤ y), cSup c ≤ y ∨ f y ≤ cSup c
Tactic: by_cases! h : ∀ z ∈ c, z ≤ y
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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 ∨ f y ≤ cSup c
have pos : cSup c ≤ y
Tactic: left
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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 ∨ f y ≤ cSup c
have neg : ∀ (z : α) (hz : z ∈ c) (hzy : ¬z ≤ y), cSup c ≤ y ∨ f y ≤ cSup c
Tactic: rcases h with ⟨z, hz, hzy⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (hypothesis)
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
⊢ cSup c ≤ y ∨ f y ≤ cSup c
have h' : f y ≤ z
Tactic: have h' := Or.resolve_left (hc hz).2 hzy
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ cSup c ≤ y ∨ f y ≤ cSup c
have neg : f y ≤ cSup c
Tactic: right
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsAdmissible x f {y : α | IsExtremePt x f y}
have base_isLeast : IsLeast {y : α | IsExtremePt x f y} x
Tactic: apply IsAdmissible.mk
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
base_isLeast : IsLeast {y : α | IsExtremePt x f y} x
⊢ IsAdmissible x f {y : α | IsExtremePt x f y}
have image_self_subset_self : f '' {y : α | IsExtremePt x f y} ⊆ {y : α | IsExtremePt x f y}
Tactic: apply IsAdmissible.mk
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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}
⊢ IsAdmissible x f {y : α | IsExtremePt x f y}
have cSup_mem : ∀ (c : NonemptyChain α),
  (↑c : Set α) ⊆ {y : α | IsExtremePt x f y} → Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} (cSup c)
Tactic: apply IsAdmissible.mk
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast {y : α | IsExtremePt x f y} x
have base_isLeast : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ IsLeast {y : α | IsExtremePt x f y} x
have base_isLeast₁ : Membership.mem (γ := Set α) (lowerBounds {y : α | IsExtremePt x f y}) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} x
have base_isLeast : ∀ {z : α} (h : z ∈ bot x f) (h' : z < x), f z ≤ x
Tactic: refine ⟨(bot_isAdmissible le_map).base_isLeast.1, ?_⟩
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
hyx : y < x
⊢ f y ≤ x
have base_isLeast : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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)
have image_self_subset_self : ∀ {z : α} (h : z ∈ bot x f) (h' : z < f y), f z ≤ f y
Tactic: refine ⟨map_mem_bot le_map hy.mem_bot, ?_⟩
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (hypothesis)
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
⊢ f z ≤ f y
have hz'₁ : 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'
Cleared hypotheses: hz'
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f z ≤ f y
have image_self_subset_self : z ∈ bot x f → ∀ (hz' : z ≤ y), f z ≤ f y
Tactic: rcases hz' with ⟨_, (hz' | hz')⟩
Cleared hypotheses: hz'
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f z ≤ f y
have image_self_subset_self₁ : z ∈ bot x f → ∀ (hz' : f y ≤ z), f z ≤ f y
Tactic: rcases hz' with ⟨_, (hz' | hz')⟩
Cleared hypotheses: hz'
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f z ≤ f y
have image_self_subset_self : ∀ (hz' : z < y), f z ≤ f y
Tactic: rcases le_iff_lt_or_eq.1 hz' with (hz' | rfl)
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f z ≤ f y
have 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
Tactic: rcases le_iff_lt_or_eq.1 hz' with (hz' | rfl)
Cleared hypotheses: y, hy, hzy, hz'
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f z ≤ f y
have image_self_subset_self : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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)
have cSup_mem : ∀ {z : α} (h : z ∈ bot x f) (h' : z < cSup c), f z ≤ cSup c
Tactic: refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (fun _ h ↦ h.mem_bot)), ?_⟩
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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 ∈ c, ¬f z ≤ y
have by_contra! : ∀ (h : ∀ (z : α) (_ : z ∈ c), f z ≤ y), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ False
have apply : cSup c ≤ y
Tactic: apply lt_irrefl y (lt_of_lt_of_le hy' ?_)
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ cSup c ≤ y
have a : ∀ y_1 ∈ c.carrier, y_1 ≤ y
Tactic: apply cSup_le
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f y ≤ cSup c
have cSup_mem : ∀ (z : α) (hz : z ∈ c) (hzy : ¬f z ≤ y), 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)
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (hypothesis)
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
have hy₁ : 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
Cleared hypotheses: hy, hz, hzy
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (hypothesis)
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
⊢ f y ≤ cSup c
have h : 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
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f y ≤ cSup c
have cSup_mem : ∀ (hyz : y < z), f y ≤ cSup c
Tactic: obtain hyz | rfl := le_iff_lt_or_eq.1 h
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ f y ≤ cSup c
have cSup_mem₁ : ∀ (hz : y ∈ c) (hzy : ¬f y ≤ y) (h : y ≤ y), f y ≤ cSup c
Tactic: obtain hyz | rfl := le_iff_lt_or_eq.1 h
Cleared hypotheses: z, hz, hzy, h
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (hypothesis)
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
⊢ f y ≤ cSup c
have hc' : cSup c ∈ bot x f
Tactic: have hc' := (bot_isAdmissible le_map).cSup_mem _ (subset_trans hc fun _ h ↦ h.mem_bot)
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (hypothesis)
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
⊢ f y ≤ cSup c
have hc'₁ : 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'
Cleared hypotheses: hc'
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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)
⊢ f y ≤ cSup c
have cSup_mem : ¬cSup c ≤ y
Tactic: apply hc'.2.resolve_left
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ {y : α | IsExtremePt x f y} = bot x f
have rw : {y : α | IsExtremePt x f y} ⊆ bot x f
Tactic: rw [← subset_bot_iff]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
rw : {y : α | IsExtremePt x f y} ⊆ bot x f
⊢ {y : α | IsExtremePt x f y} = bot x f
have rw₁ : IsAdmissible x f {y : α | IsExtremePt x f y}
Tactic: rw [← subset_bot_iff]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
⊢ y ∈ bot x f ↔ IsExtremePt x f y
have rw : Membership.mem (γ := Set α) {y : α | IsExtremePt x f y} y ↔ IsExtremePt x f y
Tactic: rw [← setOf_isExtremePt_eq_bot le_map, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
⊢ y ∈ bot x f ↔ IsExtremePt x f y
have rw₁ : IsExtremePt x f y ↔ IsExtremePt x f y
Tactic: rw [← setOf_isExtremePt_eq_bot le_map, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
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
h : y ≠ z
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
have rw : ∀ (hy : IsExtremePt x f y) ⦃z : α⦄ (hz : z ∈ bot x f),
  y ≠ z → (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
Tactic: rw [mem_bot_iff_isExtremePt le_map] at hy
Cleared hypotheses: hy, z, hz, h
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (hypothesis)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
h : y ≠ z
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
have hz₁ : 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
Cleared hypotheses: hz, h
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} z
h : y ≠ z
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
have inl : z ∈ bot x f → ∀ (hz : z ≤ y), (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
Tactic: obtain ⟨_, (hz | hz)⟩ := hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} z
h : y ≠ z
inl : z ∈ bot x f → ∀ (hz : z ≤ y), (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
have inr : z ∈ bot x f → ∀ (hz : f y ≤ z), (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
Tactic: obtain ⟨_, (hz | hz)⟩ := hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
h : y ≠ z
left : z ∈ bot x f
hz : f y ≤ z
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
have inr : (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
Tactic: left