case h
E : ℕ → Type ?u.22143
α : Type u_1
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ y ∈ cylinder x n ↔ y ∈ {y | res y n = res x n}
E : ℕ → Type ?u.22143
α : Type u_1
x : ℕ → α
n : ℕ
⊢ cylinder x n = {y | res y n = res x n}
ext y
case h
E : ℕ → Type ?u.22143
α : Type u_1
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ (∀ (i : ℕ), i < n → y i = x i) ↔ res y n = res x n
case h
E : ℕ → Type ?u.22143
α : Type u_1
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ y ∈ cylinder x n ↔ y ∈ {y | res y n = res x n}
dsimp [cylinder]
no goals
case h
E : ℕ → Type ?u.22143
α : Type u_1
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ (∀ (i : ℕ), i < n → y i = x i) ↔ res y n = res x n
rw [res_eq_res]