α : 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)
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
⊢ ↑lfp (comp lfp h) = ↑lfp (onDiag h)
let a := lfp (lfp.comp h)
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)

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)
α : 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)
refine' (lfp_le _ _).antisymm (lfp_le _ (Eq.le _))
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)
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)
have ha : (lfp ∘ h) a = a := (lfp.comp h).map_lfp
no goals
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)
calc
  h a a = h a (lfp (h a)) := congr_arg (h a) ha.symm
  _ = lfp (h a) := (h a).map_lfp
  _ = a := ha
no goals
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)
exact lfp_le _ h.onDiag.map_lfp.le