E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
⊢ x ∈ cylinder y n
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
⊢ cylinder x n = cylinder y n
rw [← mem_cylinder_iff_eq]
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
i : ℕ
hi : i < n
⊢ x i = y i
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
⊢ x ∈ cylinder y n
intro i hi
no goals
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
i : ℕ
hi : i < n
⊢ x i = y i
exact apply_eq_of_lt_firstDiff (hi.trans_le hn)