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