-- Mathlib/.lake/packages/batteries/Batteries/WF.lean
theorem rec_eq_recC : @Acc.rec = @Acc.recC

Proof state:
case h.h.h.h.h.h.intro
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro ⋯ = Acc.recC intro ⋯
⊢ (intro x h fun y a => rec intro ⋯) = intro x h fun y hr => Acc.recC intro ⋯

Tactic:
congr

Result:
case h.h.h.h.h.h.intro.e_h_ih
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro ⋯ = Acc.recC intro ⋯
⊢ (fun y a => rec intro ⋯) = fun y hr => Acc.recC intro ⋯

Proof state:
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯
a : α
t : Acc r a
⊢ rec intro t = Acc.recC intro t

Tactic:
induction t with
| intro x h ih =>
  dsimp only [recC_intro intro h]
  congr; funext y hr; exact ih _ hr

Result:
no goals

Proof state:
case h.h.h.h.h.h.intro.e_h_ih.h.h
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro ⋯ = Acc.recC intro ⋯
y : α
hr : r y x
⊢ rec intro ⋯ = Acc.recC intro ⋯

Tactic:
exact ih _ hr

Result:
no goals

Proof state:
case h.h.h.h.h.h.intro
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro ⋯ = Acc.recC intro ⋯
⊢ rec intro ⋯ = Acc.recC intro ⋯

Tactic:
dsimp only [recC_intro intro h]

Result:
case h.h.h.h.h.h.intro
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro ⋯ = Acc.recC intro ⋯
⊢ (intro x h fun y a => rec intro ⋯) = intro x h fun y hr => Acc.recC intro ⋯

Proof state:
case h.h.h.h.h.h.intro.e_h_ih
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro ⋯ = Acc.recC intro ⋯
⊢ (fun y a => rec intro ⋯) = fun y hr => Acc.recC intro ⋯

Tactic:
funext y hr

Result:
case h.h.h.h.h.h.intro.e_h_ih.h.h
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯
a x : α
h : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α) (a : r y x), rec intro ⋯ = Acc.recC intro ⋯
y : α
hr : r y x
⊢ rec intro ⋯ = Acc.recC intro ⋯

Proof state:
⊢ @rec = @Acc.recC

Tactic:
funext α r motive intro a t

Result:
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : (a : α) → Acc r a → Sort u_2
intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯
a : α
t : Acc r a
⊢ rec intro t = Acc.recC intro t