[GOAL]
⊢ {0} ∪ range succ = univ
[PROOFSTEP]
ext n
[GOAL]
case h
n : ℕ
⊢ n ∈ {0} ∪ range succ ↔ n ∈ univ
[PROOFSTEP]
cases n
[GOAL]
case h.zero
⊢ zero ∈ {0} ∪ range succ ↔ zero ∈ univ
[PROOFSTEP]
simp
[GOAL]
case h.succ
n✝ : ℕ
⊢ succ n✝ ∈ {0} ∪ range succ ↔ succ n✝ ∈ univ
[PROOFSTEP]
simp
[GOAL]
⊢ range succ = {i | 0 < i}
[PROOFSTEP]
ext (_ | i)
[GOAL]
case h.zero
⊢ zero ∈ range succ ↔ zero ∈ {i | 0 < i}
[PROOFSTEP]
simp [succ_pos, succ_ne_zero, Set.mem_setOf]
[GOAL]
case h.succ
i : ℕ
⊢ succ i ∈ range succ ↔ succ i ∈ {i | 0 < i}
[PROOFSTEP]
simp [succ_pos, succ_ne_zero, Set.mem_setOf]
[GOAL]
α : Type u_1
f : ℕ → α
⊢ {f 0} ∪ range (f ∘ succ) = range f
[PROOFSTEP]
rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]
[GOAL]
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
⊢ (range fun n => rec x f n) = {x} ∪ range fun n => rec (f 0 x) (f ∘ succ) n
[PROOFSTEP]
convert (range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm using 4
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = ((fun n => rec x f n) ∘ succ) x✝
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = f x✝ (rec x f x✝)
[PROOFSTEP]
rename_i n
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h.zero
α✝ : Type u_1
α : Type u_2
x : α
f : ℕ → α → α
⊢ rec (f 0 x) (f ∘ succ) zero = f zero (rec x f zero)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h.succ
α✝ : Type u_1
α : Type u_2
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))
[PROOFSTEP]
dsimp at ihn ⊢
[GOAL]
case h.e'_3.h.e'_4.h.e'_3.h.succ
α✝ : Type u_1
α : Type u_2
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))
[PROOFSTEP]
rw [ihn]
