[GOAL]
α : 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)
[PROOFSTEP]
set s := {a | a ≤ lfp f ∧ p a}
[GOAL]
α : 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)
[PROOFSTEP]
specialize hSup s fun a => And.right
[GOAL]
α : 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)
[PROOFSTEP]
suffices : sSup s = lfp f
[GOAL]
α : 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
[PROOFSTEP]
exact this ▸ hSup
[GOAL]
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
[PROOFSTEP]
have h : sSup s ≤ lfp f := sSup_le fun b => And.left
[GOAL]
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
[PROOFSTEP]
have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
[GOAL]
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
[PROOFSTEP]
exact h.antisymm (f.lfp_le <| le_sSup hmem)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
⊢ ↑lfp (comp lfp h) = ↑lfp (onDiag h)
[PROOFSTEP]
let a := lfp (lfp.comp h)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
a : α := ↑lfp (comp lfp h)
⊢ ↑lfp (comp lfp h) = ↑lfp (onDiag h)
[PROOFSTEP]
refine' (lfp_le _ _).antisymm (lfp_le _ (Eq.le _))
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
a : α := ↑lfp (comp lfp h)
⊢ ↑(comp lfp h) (↑lfp (onDiag h)) ≤ ↑lfp (onDiag h)
[PROOFSTEP]
exact lfp_le _ h.onDiag.map_lfp.le
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
a : α := ↑lfp (comp lfp h)
⊢ ↑(onDiag h) (↑lfp (comp lfp h)) = ↑lfp (comp lfp h)
[PROOFSTEP]
have ha : (lfp ∘ h) a = a := (lfp.comp h).map_lfp
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
a : α := ↑lfp (comp lfp h)
ha : (↑lfp ∘ ↑h) a = a
⊢ ↑(onDiag h) (↑lfp (comp lfp h)) = ↑lfp (comp lfp h)
[PROOFSTEP]
calc
  h a a = h a (lfp (h a)) := congr_arg (h a) ha.symm
  _ = lfp (h a) := (h a).map_lfp
  _ = a := ha
