E : ℕ → Type ?u.22017
α : Type u_1
x y : ℕ → α
h : res x = res y
⊢ x = y
E : ℕ → Type ?u.22017
α : Type u_1
⊢ Injective res
intro x y h
case h
E : ℕ → Type ?u.22017
α : Type u_1
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ x n = y n
E : ℕ → Type ?u.22017
α : Type u_1
x y : ℕ → α
h : res x = res y
⊢ x = y
ext n
E : ℕ → Type ?u.22017
α : Type u_1
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ res x (Nat.succ n) = res (fun n => y n) (Nat.succ n)
case h
E : ℕ → Type ?u.22017
α : Type u_1
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ x n = y n
apply res_eq_res.mp _ (Nat.lt_succ_self _)
no goals
E : ℕ → Type ?u.22017
α : Type u_1
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ res x (Nat.succ n) = res (fun n => y n) (Nat.succ n)
rw [h]