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'
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₂

Tactic:
induction ‹Acc _ _›

Goal state after:
case intro
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
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✝⁵ : ∀ (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' ⋯
x✝ : α
h✝ : ∀ (y : α), Sum.inr y ∈ f x✝ → Acc (fun x y ↦ Sum.inr x ∈ f y) y
h_ih✝ :
  ∀ (y : α) (a : Sum.inr y ∈ f x✝) (h : b ∈ f.fix y)
    (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' ⋯)
          y ⋯)
    (pf_1 : ∀ (x : α), Sum.inr x ∈ f y → Acc (fun x y ↦ Sum.inr x ∈ f y) x)
    (pf_2 :
      ∀ (x : α) (h' : Sum.inr x ∈ f 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' ⋯)
            x ⋯),
    (have h₂ := pf;
      (fun pf pf_3 h₂ ↦
          Acc.rec (motive := fun {a} pf_4 ↦
            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_4 →
              C a)
            (fun a ha IH h₂ ↦
              have h := ⋯;
              H a h fun a' fa' ↦ IH a' fa' ⋯)
            pf_3 h₂)
        pf✝⁶ ⋯ h₂) =
      H y h fun x h' ↦
        have h₂ := ⋯;
        (fun pf pf_3 h₂ ↦
            Acc.rec (motive := fun {a} pf_4 ↦
              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_4 →
                (fun x ↦ C x) a)
              (fun a ha IH h₂ ↦
                have h := ⋯;
                H a h fun a' fa' ↦ IH a' fa' ⋯)
              pf_3 h₂)
          pf✝⁶ ⋯ h₂
h : b ∈ f.fix x✝
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' ⋯)
      x✝ ⋯
pf✝¹ : ∀ (x : α), Sum.inr x ∈ f x✝ → Acc (fun x y ↦ Sum.inr x ∈ f y) x
pf✝ :
  ∀ (x : α) (h' : Sum.inr x ∈ f x✝),
    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✝⁶ ⋯ h₂) =
    H x✝ 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₂