mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f ≤ ⨆ n, (⇑f)^[n] ⊥

pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ lfp f

Tactic:
·

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f ≤ ⨆ n, (⇑f)^[n] ⊥
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ x

pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), c i ≤ x
⊢ ωSup c ≤ x

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ x
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ lfp f

Tactic:
·

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ lfp f
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ ωSup c

pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x

Tactic:
·

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ ωSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x

Tactic:
·

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ upperBounds (Set.range ⇑c)

pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))

Tactic:
·

Goal state after:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ upperBounds (Set.range ⇑c)
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ cSup c ≤ y ∨ f y ≤ cSup c

Tactic:
·

Goal state after:
case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ cSup c ≤ y ∨ f y ≤ cSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))

Tactic:
·

Goal state after:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
h : ∀ z ∈ c, z ≤ y
⊢ cSup c ≤ y ∨ f y ≤ cSup c

pp: case neg
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
h : ∃ z ∈ c, ¬z ≤ y
⊢ cSup c ≤ y ∨ f y ≤ cSup c

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
h : ∀ z ∈ c, z ≤ y
⊢ cSup c ≤ y ∨ f y ≤ cSup c
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ.inl
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

pp: case succ.inr
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
·

Goal state after:
case succ.inl
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ.inr
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
·

Goal state after:
case succ.inr
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ.inl
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
hc₁ : ChainClosure r s✝
h : s✝ ⊆ SuccChain r s✝
h₁ : s✝ ⊆ s✝
⊢ SuccChain r s✝ ⊆ SuccChain r s✝

pp: case succ.inr
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s✝
h₁ : c₁ ⊆ s✝
h₂ : SuccChain r c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝

Tactic:
·

Goal state after:
case succ.inl
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
hc₁ : ChainClosure r s✝
h : s✝ ⊆ SuccChain r s✝
h₁ : s✝ ⊆ s✝
⊢ SuccChain r s✝ ⊆ SuccChain r s✝
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ.inr
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s✝
h₁ : c₁ ⊆ s✝
h₂ : SuccChain r c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝

Tactic:
·

Goal state after:
case succ.inr
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s✝
h₁ : c₁ ⊆ s✝
h₂ : SuccChain r c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
h : ∃ z ∈ c, ¬z ≤ y
⊢ cSup c ≤ y ∨ f y ≤ cSup c

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
h : ∃ z ∈ c, ¬z ≤ y
⊢ cSup c ≤ y ∨ f y ≤ cSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c

pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ωSup c ≤ a

Tactic:
·

Goal state after:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ωSup c ≤ a

Tactic:
·

Goal state after:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ωSup c ≤ a
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast {y | IsExtremePt x f y} x

pp: case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' {y | IsExtremePt x f y} ⊆ {y | IsExtremePt x f y}

pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {y | IsExtremePt x f y} → cSup c ∈ {y | IsExtremePt x f y}

Tactic:
·

Goal state after:
case base_isLeast
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast {y | IsExtremePt x f y} x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ {y | IsExtremePt x f y}

pp: case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds {y | IsExtremePt x f y}

Tactic:
·

Goal state after:
case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ {y | IsExtremePt x f y}
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds {y | IsExtremePt x f y}

Tactic:
·

Goal state after:
case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds {y | IsExtremePt x f y}
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' {y | IsExtremePt x f y} ⊆ {y | IsExtremePt x f y}

pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {y | IsExtremePt x f y} → cSup c ∈ {y | IsExtremePt x f y}

Tactic:
·

Goal state after:
case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' {y | IsExtremePt x f y} ⊆ {y | IsExtremePt x f y}
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : SuccChain r c₃ ⊆ c₁
⊢ False

pp: case union.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
⊢ False

Tactic:
·

Goal state after:
case union.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : SuccChain r c₃ ⊆ c₁
⊢ False
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz' : z ≤ y
⊢ f z ≤ f y

pp: case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz' : f y ≤ z
⊢ f z ≤ f y

Tactic:
·

Goal state after:
case image_self_subset_self.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz' : z ≤ y
⊢ f z ≤ f y
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz'✝ : z ≤ y
hz' : z < y
⊢ f z ≤ f y

pp: case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz left✝ : z ∈ bot x f
hy : z ∈ {y | IsExtremePt x f y}
hzy : z < f z
hz' : z ≤ z
⊢ f z ≤ f z

Tactic:
·

Goal state after:
case image_self_subset_self.inl.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz'✝ : z ≤ y
hz' : z < y
⊢ f z ≤ f y
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz left✝ : z ∈ bot x f
hy : z ∈ {y | IsExtremePt x f y}
hzy : z < f z
hz' : z ≤ z
⊢ f z ≤ f z

Tactic:
·

Goal state after:
case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz left✝ : z ∈ bot x f
hy : z ∈ {y | IsExtremePt x f y}
hzy : z < f z
hz' : z ≤ z
⊢ f z ≤ f z
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz' : f y ≤ z
⊢ f z ≤ f y

Tactic:
·

Goal state after:
case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz' : f y ≤ z
⊢ f z ≤ f y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case e'_3
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f '' d✝ = Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })

pp: case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
·

Goal state after:
case e'_3
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f '' d✝ = Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {y | IsExtremePt x f y} → cSup c ∈ {y | IsExtremePt x f y}

Tactic:
·

Goal state after:
case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {y | IsExtremePt x f y} → cSup c ∈ {y | IsExtremePt x f y}
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union.inr.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : c₃ = c₁
⊢ False

pp: case union.inr.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False

Tactic:
·

Goal state after:
case union.inr.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : c₃ = c₁
⊢ False
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
H : ∃ m, Maximal (fun x_1 ↦ x_1 ∈ {y | y ∈ s ∧ x ≤ y}) m
⊢ ∃ m, x ≤ m ∧ Maximal (fun x ↦ x ∈ s) m

pp: case refine_1
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
H : ∃ m, Maximal (fun x_1 ↦ x_1 ∈ {y | y ∈ s ∧ x ≤ y}) m
⊢ ∃ m, x ≤ m ∧ Maximal (fun x ↦ x ∈ s) m
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
hcs : ∅ ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ ∅, z ≤ ub

pp: case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
·

Goal state after:
case refine_1.inl
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
hcs : ∅ ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ ∅, z ≤ ub
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
·

Goal state after:
case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
m : α
hxm : x ≤ m
ham : (fun x ↦ x ∈ Ici a) m
hm : ∀ ⦃y : α⦄, (fun x ↦ x ∈ Ici a) y → m ≤ y → y ≤ m
⊢ ∃ m, x ≤ m ∧ IsMax m

pp: case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
m : α
hxm : x ≤ m
ham : (fun x ↦ x ∈ Ici a) m
hm : ∀ ⦃y : α⦄, (fun x ↦ x ∈ Ici a) y → m ≤ y → y ≤ m
⊢ ∃ m, x ≤ m ∧ IsMax m
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
·

Goal state after:
case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union.inr.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False

Tactic:
·

Goal state after:
case union.inr.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False