-- Mathlib/Data/PFun.lean
theorem fixInduction_spec {C : α → Sort*} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a)
    (H : ∀ a', b ∈ f.fix a' → (∀ a'', Sum.inr a'' ∈ f a' → C a'') → C a') :
    @fixInduction _ _ C _ _ _ h H = H a h fun _ h' => fixInduction (fix_fwd h h') H

Proof state:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ (let_fun h₂ := ⋯;
    (fun pf pf_1 h₂ =>
        Acc.rec (motive := fun {a} pf_2 =>
          b ∈
              WellFounded.fixF
                (fun a IH =>
                  Part.assert (f a).Dom fun hf =>
                    match e : (f a).get hf with
                    | Sum.inl b => Part.some b
                    | Sum.inr a' => IH a' ⋯)
                a pf_2 →
            C a)
          (fun a ha IH h₂ =>
            let_fun h := ⋯;
            H a h fun a' fa' => IH a' fa' ⋯)
          pf_1 h₂)
      ⋯ ⋯ h₂) =
    H a h fun x h' =>
      let_fun h₂ := ⋯;
      (fun pf pf_1 h₂ =>
          Acc.rec (motive := fun {a} pf_2 =>
            b ∈
                WellFounded.fixF
                  (fun a IH =>
                    Part.assert (f a).Dom fun hf =>
                      match e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' ⋯)
                  a pf_2 →
              (fun x => C x) a)
            (fun a ha IH h₂ =>
              let_fun h := ⋯;
              H a h fun a' fa' => IH a' fa' ⋯)
            pf_1 h₂)
        ⋯ ⋯ h₂

Tactic:
generalize_proofs

Result:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
pf✝⁷ : ∀ (a : α) (hf : (f a).Dom) (a' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a
pf✝⁶ : Acc (fun x y => Sum.inr x ∈ f y) a
pf✝⁵ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a pf✝⁶
pf✝⁴ : ∀ (a : α), (∀ (y : α), Sum.inr y ∈ f a → Acc (fun x y => Sum.inr x ∈ f y) y) → Acc (fun x y => Sum.inr x ∈ f y) a
pf✝³ :
  ∀ (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a) (a : α)
    (ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun x y => Sum.inr x ∈ f y) y),
    b ∈
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          a ⋯ →
      b ∈ f.fix a
pf✝² :
  ∀ (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a) (a : α)
    (ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun x y => Sum.inr x ∈ f y) y),
    b ∈ f.fix a →
      ∀ (a' : α) (fa' : Sum.inr a' ∈ f a),
        b ∈
          WellFounded.fixF
            (fun a IH =>
              Part.assert (f a).Dom fun hf =>
                match e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯)
            a' ⋯
pf✝¹ : ∀ (x : α), Sum.inr x ∈ f a → Acc (fun x y => Sum.inr x ∈ f y) x
pf✝ :
  ∀ (x : α) (h' : Sum.inr x ∈ f a),
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        x ⋯
⊢ (let_fun h₂ := pf✝⁵;
    (fun pf pf_1 h₂ =>
        Acc.rec (motive := fun {a} pf_2 =>
          b ∈
              WellFounded.fixF
                (fun a IH =>
                  Part.assert (f a).Dom fun hf =>
                    match e : (f a).get hf with
                    | Sum.inl b => Part.some b
                    | Sum.inr a' => IH a' ⋯)
                a pf_2 →
            C a)
          (fun a ha IH h₂ =>
            let_fun h := ⋯;
            H a h fun a' fa' => IH a' fa' ⋯)
          pf_1 h₂)
      pf✝⁷ pf✝⁶ h₂) =
    H a h fun x h' =>
      let_fun h₂ := ⋯;
      (fun pf pf_1 h₂ =>
          Acc.rec (motive := fun {a} pf_2 =>
            b ∈
                WellFounded.fixF
                  (fun a IH =>
                    Part.assert (f a).Dom fun hf =>
                      match e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' ⋯)
                  a pf_2 →
              (fun x => C x) a)
            (fun a ha IH h₂ =>
              let_fun h := ⋯;
              H a h fun a' fa' => IH a' fa' ⋯)
            pf_1 h₂)
        pf✝⁷ ⋯ h₂