-- Mathlib/Data/PFun.lean
theorem fixInduction'_fwd {C : α → Sort*} {f : α →. β ⊕ α} {b : β} {a a' : α} (h : b ∈ f.fix a)
    (h' : b ∈ f.fix a') (fa : Sum.inr a' ∈ f a)
    (hbase : ∀ a_final : α, Sum.inl b ∈ f a_final → C a_final)
    (hind : ∀ a₀ a₁ : α, b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀) :
    @fixInduction' _ _ C _ _ _ h hbase hind = hind a a' h' fa (fixInduction' h' hbase hind)

Proof state:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih =>
      Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯)
        (fun b' e =>
          let_fun e := ⋯;
          hbase a' ⋯)
        (fun a'' e =>
          let_fun e := ⋯;
          hind a' a'' ⋯ e (ih a'' e))
        ⋯) =
    hind a a' h' fa
      (fixInduction h' fun a' h ih =>
        Sum.casesOn (motive := fun x => (f a').get ⋯ = x → (fun x => C x) a') ((f a').get ⋯)
          (fun b' e =>
            let_fun e := ⋯;
            hbase a' ⋯)
          (fun a'' e =>
            let_fun e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)

Tactic:
rw [fixInduction_spec]

Result:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x => (f a).get ⋯ = x → C a) ((f a).get ⋯)
      (fun b' e =>
        let_fun e := ⋯;
        hbase a ⋯)
      (fun a'' e =>
        let_fun e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' =>
              fixInduction ⋯ fun a' h ih =>
                Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e =>
                    let_fun e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e =>
                    let_fun e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hind a a' h' fa
      (fixInduction h' fun a' h ih =>
        Sum.casesOn (motive := fun x => (f a').get ⋯ = x → (fun x => C x) a') ((f a').get ⋯)
          (fun b' e =>
            let_fun e := ⋯;
            hbase a' ⋯)
          (fun a'' e =>
            let_fun e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)

Proof state:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ fixInduction' h hbase hind = hind a a' h' fa (fixInduction' h' hbase hind)

Tactic:
unfold fixInduction'

Result:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih =>
      Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯)
        (fun b' e =>
          let_fun e := ⋯;
          hbase a' ⋯)
        (fun a'' e =>
          let_fun e := ⋯;
          hind a' a'' ⋯ e (ih a'' e))
        ⋯) =
    hind a a' h' fa
      (fixInduction h' fun a' h ih =>
        Sum.casesOn (motive := fun x => (f a').get ⋯ = x → (fun x => C x) a') ((f a').get ⋯)
          (fun b' e =>
            let_fun e := ⋯;
            hbase a' ⋯)
          (fun a'' e =>
            let_fun e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)

Proof state:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fun x e =>
      Sum.casesOn (motive := fun y => (f a).get ⋯ = y → C a) x
          (fun b' e =>
            let_fun e := ⋯;
            hbase a ⋯)
          (fun a'' e =>
            let_fun e := ⋯;
            hind a a'' ⋯ e
              ((fun x h' =>
                  fixInduction ⋯ fun a' h ih =>
                    Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯)
                      (fun b' e =>
                        let_fun e := ⋯;
                        hbase a' ⋯)
                      (fun a'' e =>
                        let_fun e := ⋯;
                        hind a' a'' ⋯ e (ih a'' e))
                      ⋯)
                a'' e))
          ⋯ =
        hind a a' h' fa
          (fixInduction h' fun a' h ih =>
            Sum.casesOn (motive := fun x => (f a').get ⋯ = x → (fun x => C x) a') ((f a').get ⋯)
              (fun b' e =>
                let_fun e := ⋯;
                hbase a' ⋯)
              (fun a'' e =>
                let_fun e := ⋯;
                hind a' a'' ⋯ e (ih a'' e))
              ⋯))
    (Sum.inr a') ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x => (f a).get ⋯ = x → C a) ((f a).get ⋯)
      (fun b' e =>
        let_fun e := ⋯;
        hbase a ⋯)
      (fun a'' e =>
        let_fun e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' =>
              fixInduction ⋯ fun a' h ih =>
                Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e =>
                    let_fun e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e =>
                    let_fun e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hind a a' h' fa
      (fixInduction h' fun a' h ih =>
        Sum.casesOn (motive := fun x => (f a').get ⋯ = x → (fun x => C x) a') ((f a').get ⋯)
          (fun b' e =>
            let_fun e := ⋯;
            hbase a' ⋯)
          (fun a'' e =>
            let_fun e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)

Tactic:
refine Eq.rec (motive := fun x e =>
    Sum.casesOn (motive := fun y => (f a).get (dom_of_mem_fix h) = y → C a) x ?_ ?_
    (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = _) ?_
  (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm

Result:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fun x e =>
      Sum.casesOn (motive := fun y => (f a).get ⋯ = y → C a) x
          (fun b' e =>
            let_fun e := ⋯;
            hbase a ⋯)
          (fun a'' e =>
            let_fun e := ⋯;
            hind a a'' ⋯ e
              ((fun x h' =>
                  fixInduction ⋯ fun a' h ih =>
                    Sum.casesOn (motive := fun x => (f a').get ⋯ = x → C a') ((f a').get ⋯)
                      (fun b' e =>
                        let_fun e := ⋯;
                        hbase a' ⋯)
                      (fun a'' e =>
                        let_fun e := ⋯;
                        hind a' a'' ⋯ e (ih a'' e))
                      ⋯)
                a'' e))
          ⋯ =
        hind a a' h' fa
          (fixInduction h' fun a' h ih =>
            Sum.casesOn (motive := fun x => (f a').get ⋯ = x → (fun x => C x) a') ((f a').get ⋯)
              (fun b' e =>
                let_fun e := ⋯;
                hbase a' ⋯)
              (fun a'' e =>
                let_fun e := ⋯;
                hind a' a'' ⋯ e (ih a'' e))
              ⋯))
    (Sum.inr a') ⋯