case intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : ¬x ∈ s
y : (n : ℕ) → E n
hy : y ∈ s
⊢ 0 < shortestPrefixDiff x s
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
x : (n : ℕ) → E n
hx : ¬x ∈ s
⊢ 0 < shortestPrefixDiff x s
rcases hne with ⟨y, hy⟩
no goals
case intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : ¬x ∈ s
y : (n : ℕ) → E n
hy : y ∈ s
⊢ 0 < shortestPrefixDiff x s
exact (zero_le _).trans_lt (firstDiff_lt_shortestPrefixDiff hs hx hy)