no goals
m n✝ : ℕ
α✝ : Fin (n✝ + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ (succ i)
i : Fin n✝
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ Set.range (cons x b) = insert x (Set.range b)
rw [range_fin_succ, cons_zero, tail_cons]