-- Module: Mathlib.Data.PFun
Goal:
α : 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₀
refine :
  Sum.casesOn (motive := fun (y : β ⊕ α) ↦ (f a).get ⋯ = y → C a) (Sum.inr a')
      (fun (b' : β) (e : (f a).get ⋯ = Sum.inl b') ↦
        have e := ⋯;
        hbase a ⋯)
      (fun (a'' : α) (e : (f a).get ⋯ = Sum.inr a'') ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun (x : α) (h' : Sum.inr x ∈ f a) ↦
              (fixInduction (C := fun (x : α) ↦ C x) ⋯
                  fun (a' : α) (h : b ∈ f.fix a') (ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a'') ↦
                  Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a').get ⋯ = x) → C a') ((f a').get ⋯)
                    (fun (b' : β) (e : (f a').get ⋯ = Sum.inl b') ↦
                      have e := ⋯;
                      hbase a' ⋯)
                    (fun (a'' : α) (e : (f a').get ⋯ = Sum.inr a'') ↦
                      have e := ⋯;
                      hind a' a'' ⋯ e (ih a'' e))
                    ⋯ :
                C x))
            a'' e))
      ⋯ =
    hind a a' h' fa
      (fixInduction (C := fun (x : α) ↦ (fun (x : α) ↦ C x) x) h'
        fun (a' : α) (h : b ∈ f.fix a') (ih : (a'' : α) → Sum.inr a'' ∈ f a' → (fun (x : α) ↦ C x) a'') ↦
        Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a').get ⋯ = x) → (fun (x : α) ↦ C x) a') ((f a').get ⋯)
          (fun (b' : β) (e : (f a').get ⋯ = Sum.inl b') ↦
            have e := ⋯;
            hbase a' ⋯)
          (fun (a'' : α) (e : (f a').get ⋯ = Sum.inr a'') ↦
            have e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)
⊢ Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a).get ⋯ = x) → C a) ((f a).get ⋯)
      (fun (b' : β) (e : (f a).get ⋯ = Sum.inl b') ↦
        have e := ⋯;
        hbase a ⋯)
      (fun (a'' : α) (e : (f a).get ⋯ = Sum.inr a'') ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun (x : α) (h' : Sum.inr x ∈ f a) ↦
              (fixInduction (C := fun (x : α) ↦ C x) ⋯
                  fun (a' : α) (h : b ∈ f.fix a') (ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a'') ↦
                  Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a').get ⋯ = x) → C a') ((f a').get ⋯)
                    (fun (b' : β) (e : (f a').get ⋯ = Sum.inl b') ↦
                      have e := ⋯;
                      hbase a' ⋯)
                    (fun (a'' : α) (e : (f a').get ⋯ = Sum.inr a'') ↦
                      have e := ⋯;
                      hind a' a'' ⋯ e (ih a'' e))
                    ⋯ :
                C x))
            a'' e))
      ⋯ =
    hind a a' h' fa
      (fixInduction (C := fun (x : α) ↦ (fun (x : α) ↦ C x) x) h'
        fun (a' : α) (h : b ∈ f.fix a') (ih : (a'' : α) → Sum.inr a'' ∈ f a' → (fun (x : α) ↦ C x) a'') ↦
        Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (e : (f a').get ⋯ = x) → (fun (x : α) ↦ C x) a') ((f a').get ⋯)
          (fun (b' : β) (e : (f a').get ⋯ = Sum.inl b') ↦
            have e := ⋯;
            hbase a' ⋯)
          (fun (a'' : α) (e : (f a').get ⋯ = Sum.inr a'') ↦
            have 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

Premises used: Part.get_eq_of_mem, Eq.rec, Eq.symm, PFun.dom_of_mem_fix