awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
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' : α) (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' ⋯ :
            Part β))
        a pf_1 :
      Part β)
    b
intro :
  (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) →
          C a
⊢ C a

Tactic:
induction ‹Acc (Sum.inr · ∈ f ·) a› with | intro a ha IH => _

Premises used: Membership.mem, Acc, Sum.inr
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a_1 : α
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
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
⊢ b ∈ f.fix a

Tactic:
have h : b ∈ f.fix a := Part.mem_assert_iff.2 ⟨⟨a, ha⟩, h₂⟩
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a_1 : α
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
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
h : b ∈ f.fix a
⊢ C a

Tactic:
exact H a h fun a' fa' => IH a' fa' (Part.mem_assert_iff.1 (fix_fwd h fa')).snd

Premises used: PFun.fix_fwd, Exists.snd, Iff.mp, Part.mem_assert_iff
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix 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₀
refine : (a' : α) → (h : b ∈ f.fix a') → (ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ C a

Tactic:
refine fixInduction h fun a' h ih => ?_
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
inl : (b' : β) → (e : (f a').get ⋯ = Sum.inl b') → C a'
inr : (a'' : α) → (e : (f a').get ⋯ = Sum.inr a'') → C a'
⊢ C a'

Tactic:
rcases e : (f a').get (dom_of_mem_fix h) with b' | a''

Premises used: Part.get, PFun.dom_of_mem_fix
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : (f a').get ⋯ = Sum.inl b'
inl : (e : Sum.inl b' ∈ f a') → C a'
⊢ C a'

Tactic:
replace e : _ ∈ f a' := ⟨_, e⟩
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : (f a').get ⋯ = Sum.inr a''
inr : (e : Sum.inr a'' ∈ f a') → C a'
⊢ C a'

Tactic:
replace e : _ ∈ f a' := ⟨_, e⟩
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
inl : Sum.inl b ∈ f a'
⊢ C a'

Tactic:
apply hbase
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ Sum.inl b' ∈ f a'

Tactic:
e
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
h₁ : b = b'
⊢ Sum.inl b ∈ f a'

Tactic:
convert! e
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ b = b'

Tactic:
Part.mem_unique h (fix_stop e)

Premises used: PFun.fix_stop, Part.mem_unique
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : Sum.inl b' ∈ f a'
⊢ b = b'

Tactic:
exact Part.mem_unique h (fix_stop e)

Premises used: PFun.fix_stop, Part.mem_unique
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h_1 : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : Sum.inr a'' ∈ f a'
⊢ C a'

Tactic:
exact hind _ _ (fix_fwd h e) e (ih _ e)

Premises used: PFun.fix_fwd
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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₀
unfold :
  (fixInduction (C := fun (x : α) ↦ C x) h
      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))
        ⋯) =
    hbase a fa
⊢ fixInduction' (C := C) h hbase hind = hbase a fa

Tactic:
unfold fixInduction'
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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₀
rw :
  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))
      ⋯ =
    hbase a fa
⊢ (fixInduction (C := fun (x : α) ↦ C x) h
      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))
        ⋯) =
    hbase a fa

Tactic:
rw [fixInduction_spec]

Premises used: PFun.fixInduction_spec
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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))
      ⋯ =
    hbase a fa

Tactic:
Eq.rec (motive := fun x e ↦
      Sum.casesOn x ?_ ?_ (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = hbase a fa) ?_
    (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm

Premises used: Part.get_eq_of_mem, Eq.rec, Eq.symm, PFun.dom_of_mem_fix
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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₀
refine :
  Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (f a).get ⋯ = x → C a) (Sum.inl b)
      (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))
      ⋯ =
    hbase a fa
⊢ 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))
      ⋯ =
    hbase a fa

Tactic:
refine Eq.rec (motive := fun x e ↦
      Sum.casesOn x ?_ ?_ (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = hbase a fa) ?_
    (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm

Premises used: Part.get_eq_of_mem, Eq.rec, Eq.symm, PFun.dom_of_mem_fix
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ 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₀
⊢ (fun (x : β ⊕ α) (e : Sum.inl b = x) ↦
      Sum.casesOn (motive := fun (x : β ⊕ α) ↦ (f a).get ⋯ = x → C a) x
          (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))
          ⋯ =
        hbase a fa)
    (Sum.inl b) ⋯

Tactic:
simp
-- Module: Mathlib.Data.PFun
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₀
unfold :
  (fixInduction (C := fun (x : α) ↦ C x) h
      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))
        ⋯) =
    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))
          ⋯)
⊢ fixInduction' (C := C) h hbase hind = hind a a' h' fa (fixInduction' (C := fun (x : α) ↦ C x) h' hbase hind)

Tactic:
unfold fixInduction'
-- Module: Mathlib.Data.PFun
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₀
rw :
  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))
          ⋯)
⊢ (fixInduction (C := fun (x : α) ↦ C x) h
      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))
        ⋯) =
    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))
          ⋯)

Tactic:
rw [fixInduction_spec]

Premises used: PFun.fixInduction_spec