α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
hSup : ∀ (s : Set α), (∀ (a : α), a ∈ s → p a) → p (sSup s)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
⊢ p (↑lfp f)
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
hSup : ∀ (s : Set α), (∀ (a : α), a ∈ s → p a) → p (sSup s)
⊢ p (↑lfp f)
set s := { a | a ≤ lfp f ∧ p a }
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
⊢ p (↑lfp f)
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
hSup : ∀ (s : Set α), (∀ (a : α), a ∈ s → p a) → p (sSup s)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
⊢ p (↑lfp f)
specialize hSup s fun a => And.right
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
this : sSup s = ↑lfp f
⊢ p (↑lfp f)

case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = ↑lfp f
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
⊢ p (↑lfp f)
suffices : sSup s = lfp f
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = ↑lfp f
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
this : sSup s = ↑lfp f
⊢ p (↑lfp f)

case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = ↑lfp f
exact this ▸ hSup
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ ↑lfp f
⊢ sSup s = ↑lfp f
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = ↑lfp f
have h : sSup s ≤ lfp f := sSup_le fun b => And.left
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ ↑lfp f
hmem : ↑f (sSup s) ∈ s
⊢ sSup s = ↑lfp f
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ ↑lfp f
⊢ sSup s = ↑lfp f
have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
no goals
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ ↑lfp f
hmem : ↑f (sSup s) ∈ s
⊢ sSup s = ↑lfp f
exact h.antisymm (f.lfp_le <| le_sSup hmem)