Module: Mathlib.Data.PFun

Goal state before:
pp: α : 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'
⊢ (have h₂ := ⋯;
    (fun pf pf_1 h₂ ↦
        Acc.rec (motive := fun {a} pf_2 ↦
          b ∈
              WellFounded.fixF
                (fun a IH ↦
                  Part.assert (f a).Dom fun hf ↦
                    match e : (f a).get hf with
                    | Sum.inl b => Part.some b
                    | Sum.inr a' => IH a' ⋯)
                a pf_2 →
            C a)
          (fun a ha IH h₂ ↦
            have h := ⋯;
            H a h fun a' fa' ↦ IH a' fa' ⋯)
          pf_1 h₂)
      ⋯ ⋯ h₂) =
    H a h fun x h' ↦
      have h₂ := ⋯;
      (fun pf pf_1 h₂ ↦
          Acc.rec (motive := fun {a} pf_2 ↦
            b ∈
                WellFounded.fixF
                  (fun a IH ↦
                    Part.assert (f a).Dom fun hf ↦
                      match e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' ⋯)
                  a pf_2 →
              (fun x ↦ C x) a)
            (fun a ha IH h₂ ↦
              have h := ⋯;
              H a h fun a' fa' ↦ IH a' fa' ⋯)
            pf_1 h₂)
        ⋯ ⋯ h₂

Tactic:
generalize_proofs

Goal state after:
α : 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' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a
pf✝⁶ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
pf✝⁵ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a pf✝⁶
pf✝⁴ : ∀ (a : α), (∀ (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✝³ :
  ∀ (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α), (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),
    b ∈
        WellFounded.fixF
          (fun a IH ↦
            Part.assert (f a).Dom fun hf ↦
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          a ⋯ →
      b ∈ f.fix a
pf✝² :
  ∀ (pf : ∀ (a : α) (hf : (f a).Dom) (a' : α), (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),
    b ∈ f.fix a →
      ∀ (a' : α) (fa' : Sum.inr a' ∈ f a),
        b ∈
          WellFounded.fixF
            (fun a IH ↦
              Part.assert (f a).Dom fun hf ↦
                match e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯)
            a' ⋯
pf✝¹ : ∀ (x : α), Sum.inr x ∈ f a → Acc (fun x y ↦ Sum.inr x ∈ f y) x
pf✝ :
  ∀ (x : α) (h' : Sum.inr x ∈ f a),
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        x ⋯
⊢ (have h₂ := pf✝⁵;
    (fun pf pf_1 h₂ ↦
        Acc.rec (motive := fun {a} pf_2 ↦
          b ∈
              WellFounded.fixF
                (fun a IH ↦
                  Part.assert (f a).Dom fun hf ↦
                    match e : (f a).get hf with
                    | Sum.inl b => Part.some b
                    | Sum.inr a' => IH a' ⋯)
                a pf_2 →
            C a)
          (fun a ha IH h₂ ↦
            have h := ⋯;
            H a h fun a' fa' ↦ IH a' fa' ⋯)
          pf_1 h₂)
      pf✝⁷ pf✝⁶ h₂) =
    H a h fun x h' ↦
      have h₂ := ⋯;
      (fun pf pf_1 h₂ ↦
          Acc.rec (motive := fun {a} pf_2 ↦
            b ∈
                WellFounded.fixF
                  (fun a IH ↦
                    Part.assert (f a).Dom fun hf ↦
                      match e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' ⋯)
                  a pf_2 →
              (fun x ↦ C x) a)
            (fun a ha IH h₂ ↦
              have h := ⋯;
              H a h fun a' fa' ↦ IH a' fa' ⋯)
            pf_1 h₂)
        pf✝⁷ ⋯ h₂