cases x using by_cases with
| pure r =>
  simp only [pure_bind, flip, Function.comp]
  apply @eqF.monotone F inst T eq
  . intro x y h
    apply Or.inr
    apply pgfp.monotone ⟨eqF, eqF.monotone⟩ ⊥
    . intro x y h
      cases h
    . exact h
  . have := eq.refl (k₁ r >>= k₂)
    rw [eq, eqP, ←pgfp.unfold, CompleteLattice.bot_sup] at this
    exact this
| free f =>
  simp only [←QPF.map_comp, free_bind]
  let P : Free F T → Free F T → Prop :=(λ y z:Free F T => ∃ x, (x >>= k₁ >>= k₂) = y ∧ x >>= (flip bind k₂ ∘ k₁) = z)
  apply @eqF.monotone F inst T P
  . intro x y h
    apply Or.inl
    exact h
  . apply eqF.Free
    exists inst.map (λ x => ⟨⟨x >>= k₁ >>= k₂, x >>= (flip bind k₂ ∘ k₁)⟩, by exists x⟩) f
    simp only [←QPF.map_comp]
    constructor
    . constructor
    . constructor
case refl.refl
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y z : Free F T
x : Free F R
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (x >>= k₁ >>= k₂) (x >>= flip bind k₂ ∘ k₁)
no goals