-- Module: Mathlib.Data.PFun
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'
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
pf_2 :
  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' ⋯ :
            Part β))
        a pf_1 :
      Part β)
    b
pf_3 :
  ∀ (a : α) (ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y),
    Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a
pf_4 :
  ∀ (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a) (a : α)
    (ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) 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' ⋯ :
                Part β))
            a ⋯ :
          Part β)
        b),
    b ∈ f.fix a
pf_5 :
  ∀ (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a) (a : α)
    (ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y) (h : b ∈ f.fix a) (a' : α)
    (fa' : Sum.inr a' ∈ f a),
    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' ⋯ :
              Part β))
          a' ⋯ :
        Part β)
      b
pf_6 : ∀ (x : α) (h' : Sum.inr x ∈ f a), Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) x
pf_7 :
  ∀ (x : α) (h' : Sum.inr x ∈ f a),
    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' ⋯ :
              Part β))
          x ⋯ :
        Part β)
      b
intro :
  ∀ (x : α) (h : ∀ (y : α), Sum.inr y ∈ f x → Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y),
    (∀ (y : α) (a : Sum.inr y ∈ f x) (h_1 : b ∈ f.fix y)
        (pf_8 :
          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' ⋯ :
                    Part β))
                y ⋯ :
              Part β)
            b)
        (pf_9 : ∀ (x : α) (h' : Sum.inr x ∈ f y), Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) x)
        (pf_10 :
          ∀ (x : α) (h' : Sum.inr x ∈ f y),
            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' ⋯ :
                      Part β))
                  x ⋯ :
                Part β)
              b),
        (have h₂ := pf_8;
          (fun (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a)
                (pf_11 : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) 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' ⋯ :
                            Part β))
                        y pf_11 :
                      Part β)
                    b) ↦
              (Acc.rec (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (motive :=
                  fun {a : α} (pf_12 : 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' ⋯ :
                                Part β))
                            a pf_12 :
                          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' ⋯ :
                                          Part β))
                                      y ⋯ :
                                    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' ⋯ :
                                  Part β))
                              a ⋯ :
                            Part β)
                          b) ↦
                    have h := ⋯;
                    H a h fun (a' : α) (fa' : Sum.inr a' ∈ f a) ↦ IH a' fa' ⋯)
                  pf_11 h₂ :
                C y))
            pf ⋯ h₂) =
          H y h_1 fun (x : α) (h' : Sum.inr x ∈ f y) ↦
            have h₂ := ⋯;
            (fun (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a)
                  (pf_11 : 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' ⋯ :
                              Part β))
                          x pf_11 :
                        Part β)
                      b) ↦
                (Acc.rec (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (motive :=
                    fun {a : α} (pf_12 : 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' ⋯ :
                                  Part β))
                              a pf_12 :
                            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' ⋯ :
                                            Part β))
                                        y ⋯ :
                                      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' ⋯ :
                                    Part β))
                                a ⋯ :
                              Part β)
                            b) ↦
                      have h := ⋯;
                      H a h fun (a' : α) (fa' : Sum.inr a' ∈ f a) ↦ IH a' fa' ⋯)
                    pf_11 h₂ :
                  (fun (x : α) ↦ C x) x))
              pf ⋯ h₂) →
      ∀ (h_1 : b ∈ f.fix x)
        (pf_8 :
          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' ⋯ :
                    Part β))
                x ⋯ :
              Part β)
            b)
        (pf_9 : ∀ (x_1 : α) (h' : Sum.inr x_1 ∈ f x), Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) x_1)
        (pf_10 :
          ∀ (x_1 : α) (h' : Sum.inr x_1 ∈ f x),
            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' ⋯ :
                      Part β))
                  x_1 ⋯ :
                Part β)
              b),
        (have h₂ := pf_8;
          (fun (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a)
                (pf_11 : 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' ⋯ :
                            Part β))
                        x pf_11 :
                      Part β)
                    b) ↦
              (Acc.rec (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (motive :=
                  fun {a : α} (pf_12 : 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' ⋯ :
                                Part β))
                            a pf_12 :
                          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' ⋯ :
                                          Part β))
                                      y ⋯ :
                                    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' ⋯ :
                                  Part β))
                              a ⋯ :
                            Part β)
                          b) ↦
                    have h := ⋯;
                    H a h fun (a' : α) (fa' : Sum.inr a' ∈ f a) ↦ IH a' fa' ⋯)
                  pf_11 h₂ :
                C x))
            pf ⋯ h₂) =
          H x h_1 fun (x_1 : α) (h' : Sum.inr x_1 ∈ f x) ↦
            have h₂ := ⋯;
            (fun (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a)
                  (pf_11 : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) x_1)
                  (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' ⋯ :
                              Part β))
                          x_1 pf_11 :
                        Part β)
                      b) ↦
                (Acc.rec (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (motive :=
                    fun {a : α} (pf_12 : 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' ⋯ :
                                  Part β))
                              a pf_12 :
                            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' ⋯ :
                                            Part β))
                                        y ⋯ :
                                      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' ⋯ :
                                    Part β))
                                a ⋯ :
                              Part β)
                            b) ↦
                      have h := ⋯;
                      H a h fun (a' : α) (fa' : Sum.inr a' ∈ f a) ↦ IH a' fa' ⋯)
                    pf_11 h₂ :
                  (fun (x : α) ↦ C x) x_1))
              pf ⋯ h₂
⊢ (have h₂ := pf_2;
    (fun (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a)
          (pf_8 : 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' ⋯ :
                      Part β))
                  a pf_8 :
                Part β)
              b) ↦
        (Acc.rec (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (motive :=
            fun {a : α} (pf_9 : 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' ⋯ :
                          Part β))
                      a pf_9 :
                    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' ⋯ :
                                    Part β))
                                y ⋯ :
                              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' ⋯ :
                            Part β))
                        a ⋯ :
                      Part β)
                    b) ↦
              have h := ⋯;
              H a h fun (a' : α) (fa' : Sum.inr a' ∈ f a) ↦ IH a' fa' ⋯)
            pf_8 h₂ :
          C a))
      pf pf_1 h₂) =
    H a h fun (x : α) (h' : Sum.inr x ∈ f a) ↦
      have h₂ := ⋯;
      (fun (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a)
            (pf_8 : 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' ⋯ :
                        Part β))
                    x pf_8 :
                  Part β)
                b) ↦
          (Acc.rec (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (motive :=
              fun {a : α} (pf_9 : 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' ⋯ :
                            Part β))
                        a pf_9 :
                      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' ⋯ :
                                      Part β))
                                  y ⋯ :
                                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' ⋯ :
                              Part β))
                          a ⋯ :
                        Part β)
                      b) ↦
                have h := ⋯;
                H a h fun (a' : α) (fa' : Sum.inr a' ∈ f a) ↦ IH a' fa' ⋯)
              pf_8 h₂ :
            (fun (x : α) ↦ C x) x))
        pf ⋯ h₂

Tactic:
induction ‹Acc _ _›

Premises used: Acc