case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = ((fun n => rec x f n) ∘ succ) x✝
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
⊢ (range fun n => rec x f n) = {x} ∪ range fun n => rec (f 0 x) (f ∘ succ) n
convert (range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm using 4
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = f x✝ (rec x f x✝)
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = ((fun n => rec x f n) ∘ succ) x✝
dsimp
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = f x✝ (rec x f x✝)
rename_i n
case h.e'_3.h.e'_4.h.e'_3.h.zero
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
⊢ rec (f 0 x) (f ∘ succ) zero = f zero (rec x f zero)

case h.e'_3.h.e'_4.h.e'_3.h.succ
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ rec (f 0 x) (f ∘ succ) (succ n) = f (succ n) (rec x f (succ n))
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
induction' n with n ihn
no goals
case h.e'_3.h.e'_4.h.e'_3.h.zero
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
⊢ rec (f 0 x) (f ∘ succ) zero = f zero (rec x f zero)
rfl
case h.e'_3.h.e'_4.h.e'_3.h.succ
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (succ n) (rec (f 0 x) (f ∘ succ) n) = f (succ n) (f n (rec x f n))
case h.e'_3.h.e'_4.h.e'_3.h.succ
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ rec (f 0 x) (f ∘ succ) (succ n) = f (succ n) (rec x f (succ n))
dsimp at ihn⊢
no goals
case h.e'_3.h.e'_4.h.e'_3.h.succ
α✝ : Type ?u.3713
α : Type u_1
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (succ n) (rec (f 0 x) (f ∘ succ) n) = f (succ n) (f n (rec x f n))
rw [ihn]