-- Mathlib/Data/PFun.lean
theorem fixInduction'_stop {C : α → Sort*} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a)
    (fa : Sum.inl b ∈ 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 = hbase a fa

Proof state:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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 = hbase a fa

Tactic:
unfold fixInduction'

Result:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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))
        ⋯) =
    hbase a fa

Proof state:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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))
        ⋯) =
    hbase a fa

Tactic:
rw [fixInduction_spec]

Result:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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))
      ⋯ =
    hbase a fa

Proof state:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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 x => (f a).get ⋯ = x → 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))
          ⋯ =
        hbase a fa)
    (Sum.inl b) ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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))
      ⋯ =
    hbase a fa

Tactic:
refine Eq.rec (motive := fun x e ↦
    Sum.casesOn x ?_ ?_ (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = hbase a fa) ?_
  (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 : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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 x => (f a).get ⋯ = x → 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))
          ⋯ =
        hbase a fa)
    (Sum.inl b) ⋯