-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : 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 (C := C) h H = H a h fun (x : α) (h' : Sum.inr x ∈ f a) ↦ fixInduction (C := fun (x : α) ↦ C x) ⋯ H
have unfold : (have h₂ := sorry;
  (fun (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a)
        (pf_1 : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a)
        (h₂ :
          Membership.mem (γ := Part β)
            (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                  (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                      match (motive := β ⊕ α → Part β) e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' sorry :
                    Part β))
                a pf_1 :
              Part β)
            b) ↦
      (Acc.rec (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (motive :=
          fun {a : α} (pf_2 : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a) ↦
          (h₂ :
              Membership.mem (γ := Part β)
                (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                    (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                      (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                          match (motive := β ⊕ α → Part β) e : (f a).get hf with
                          | Sum.inl b => Part.some b
                          | Sum.inr a' => IH a' sorry :
                        Part β))
                    a pf_2 :
                  Part β)
                b) →
            C a)
          (fun (a : α) (ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y)
              (IH :
                (y : α) →
                  (a : Sum.inr y ∈ f a) →
                    (h₂ :
                        Membership.mem (γ := Part β)
                          (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                              (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                                (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                                    match (motive := β ⊕ α → Part β) e : (f a).get hf with
                                    | Sum.inl b => Part.some b
                                    | Sum.inr a' => IH a' sorry :
                                  Part β))
                              y sorry :
                            Part β)
                          b) →
                      C y)
              (h₂ :
                Membership.mem (γ := Part β)
                  (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                      (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                        (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                            match (motive := β ⊕ α → Part β) e : (f a).get hf with
                            | Sum.inl b => Part.some b
                            | Sum.inr a' => IH a' sorry :
                          Part β))
                      a sorry :
                    Part β)
                  b) ↦
            have h := sorry;
            H a h fun (a' : α) (fa' : Sum.inr a' ∈ f a) ↦ IH a' fa' sorry)
          pf_1 h₂ :
        C a))
    sorry sorry h₂) =
  H a h fun (x : α) (h' : Sum.inr x ∈ f a) ↦
    have h₂ := sorry;
    (fun (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a)
          (pf_1 : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) x)
          (h₂ :
            Membership.mem (γ := Part β)
              (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                  (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                    (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                        match (motive := β ⊕ α → Part β) e : (f a).get hf with
                        | Sum.inl b => Part.some b
                        | Sum.inr a' => IH a' sorry :
                      Part β))
                  x pf_1 :
                Part β)
              b) ↦
        (Acc.rec (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (motive :=
            fun {a : α} (pf_2 : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a) ↦
            (h₂ :
                Membership.mem (γ := Part β)
                  (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                      (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                        (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                            match (motive := β ⊕ α → Part β) e : (f a).get hf with
                            | Sum.inl b => Part.some b
                            | Sum.inr a' => IH a' sorry :
                          Part β))
                      a pf_2 :
                    Part β)
                  b) →
              (fun (x : α) ↦ C x) a)
            (fun (a : α) (ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y)
                (IH :
                  (y : α) →
                    (a : Sum.inr y ∈ f a) →
                      (h₂ :
                          Membership.mem (γ := Part β)
                            (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                                (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                                  (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                                      match (motive := β ⊕ α → Part β) e : (f a).get hf with
                                      | Sum.inl b => Part.some b
                                      | Sum.inr a' => IH a' sorry :
                                    Part β))
                                y sorry :
                              Part β)
                            b) →
                        (fun (x : α) ↦ C x) y)
                (h₂ :
                  Membership.mem (γ := Part β)
                    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                              match (motive := β ⊕ α → Part β) e : (f a).get hf with
                              | Sum.inl b => Part.some b
                              | Sum.inr a' => IH a' sorry :
                            Part β))
                        a sorry :
                      Part β)
                    b) ↦
              have h := sorry;
              H a h fun (a' : α) (fa' : Sum.inr a' ∈ f a) ↦ IH a' fa' sorry)
            pf_1 h₂ :
          (fun (x : α) ↦ C x) x))
      sorry sorry h₂
Tactic: unfold fixInduction