unexpected eliminator when using gfp_induction

Stream: mathlib4

[Ira Fesefeldt]

I am trying to figure out how to use the induction principle offered for fixed points in a complete lattice. But whenever I am using it, lean complains about an unexpected eliminator resulting type.

See for example this artificial (since their is a very easy proof for this) example:

import Mathlib

open OrderHom ENNReal

noncomputable def f : ENNReal → ENNReal := fun x => x + 1

theorem f_mono : Monotone f := by
    intro a b h
    unfold f
    exact add_le_add h le_rfl

noncomputable def fixed : ENNReal := gfp ⟨f, f_mono⟩

example : fixed ≤ ∞ := by
    unfold fixed
    induction (⟨f, f_mono⟩ : ENNReal →o ENNReal) using gfp_induction with -- unexpected eliminator resulting type p (gfp f)
    | step a ih h_le => sorry
    | hInf s ih => sorry

I tried various versions of this, but with no luck. Does someone maybe have a clue whats going on here?

[Ira Fesefeldt]

I guess it works like this:

import Mathlib

open OrderHom ENNReal

noncomputable def f : ENNReal → ENNReal := fun x => x + 1

theorem f_mono : Monotone f := by
    intro a b h
    unfold f
    exact add_le_add h le_rfl

noncomputable def fixed : ENNReal := gfp ⟨f, f_mono⟩

example : ∞ = fixed := by
  apply gfp_induction
  · intro r hr _
    simp [f]
    rw [← top_add 1]
    apply congr_arg₂
    · exact hr
    · rfl
  · intro s hs
    apply le_antisymm
    · apply le_sInf
      intro b hb
      rw [← hs b hb]
    · exact OrderTop.le_top (sInf s)

Maybe the name is confusing if you cannot use the induction tactic with it?