case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ y ∈ cylinder x n ↔ y ∈ Set.pi ↑(Finset.range n) fun i => {x i}
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
⊢ cylinder x n = Set.pi ↑(Finset.range n) fun i => {x i}
ext y
no goals
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ y ∈ cylinder x n ↔ y ∈ Set.pi ↑(Finset.range n) fun i => {x i}
simp [cylinder]