-- 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:
case intro
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
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✝⁵ : ∀ (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' ⋯
x✝ : α
h✝ : ∀ (y : α), Sum.inr y ∈ f x✝ → Acc (fun x y => Sum.inr x ∈ f y) y
h_ih✝ :
  ∀ (y : α) (a : Sum.inr y ∈ f x✝) (h : b ∈ f.fix y)
    (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' ⋯)
          y ⋯)
    (pf_1 : ∀ (x : α), Sum.inr x ∈ f y → Acc (fun x y => Sum.inr x ∈ f y) x)
    (pf_2 :
      ∀ (x : α) (h' : Sum.inr x ∈ f 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' ⋯)
            x ⋯),
    (let_fun h₂ := pf;
      (fun pf pf_3 h₂ =>
          Acc.rec (motive := fun {a} pf_4 =>
            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_4 →
              C a)
            (fun a ha IH h₂ =>
              let_fun h := ⋯;
              H a h fun a' fa' => IH a' fa' ⋯)
            pf_3 h₂)
        pf✝⁶ ⋯ h₂) =
      H y h fun x h' =>
        let_fun h₂ := ⋯;
        (fun pf pf_3 h₂ =>
            Acc.rec (motive := fun {a} pf_4 =>
              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_4 →
                (fun x => C x) a)
              (fun a ha IH h₂ =>
                let_fun h := ⋯;
                H a h fun a' fa' => IH a' fa' ⋯)
              pf_3 h₂)
          pf✝⁶ ⋯ h₂
h : b ∈ f.fix x✝
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' ⋯)
      x✝ ⋯
pf✝¹ : ∀ (x : α), Sum.inr x ∈ f x✝ → Acc (fun x y => Sum.inr x ∈ f y) x
pf✝ :
  ∀ (x : α) (h' : Sum.inr x ∈ f x✝),
    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✝⁶ ⋯ h₂) =
    H x✝ 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₂

Tactic:
rfl

Result:
no goals

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'
⊢ fixInduction h H = H a h fun x h' => fixInduction ⋯ H

Tactic:
unfold fixInduction

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'
⊢ (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₂