E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
l_eq : longestPrefix y s = longestPrefix x s
⊢ x ∈ cylinder y (longestPrefix x s)
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
l_eq : longestPrefix y s = longestPrefix x s
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
rw [l_eq, ← mem_cylinder_iff_eq]
no goals
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
l_eq : longestPrefix y s = longestPrefix x s
⊢ x ∈ cylinder y (longestPrefix x s)
exact cylinder_anti y H.le (mem_cylinder_firstDiff x y)
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
⊢ longestPrefix y s = longestPrefix x s

case inr.inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s = longestPrefix x s
⊢ longestPrefix y s = longestPrefix x s

case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
⊢ longestPrefix y s = longestPrefix x s
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
⊢ longestPrefix y s = longestPrefix x s
rcases lt_trichotomy (longestPrefix y s) (longestPrefix x s) with (L | L | L)
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
⊢ longestPrefix y s = longestPrefix x s
have Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
  inter_cylinder_longestPrefix_nonempty hs hne x
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
Z : Disjoint s (cylinder y (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
have Z := disjoint_cylinder_of_longestPrefix_lt hs ys L
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff y x
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
Z : Disjoint s (cylinder y (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
Z : Disjoint s (cylinder y (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
rw [firstDiff_comm] at H
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff y x
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
Z : Disjoint s (cylinder x (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff y x
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
Z : Disjoint s (cylinder y (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H.le] at Z
no goals
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff y x
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s < longestPrefix x s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
Z : Disjoint s (cylinder x (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
exact (Ax.not_disjoint Z).elim
no goals
case inr.inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix y s = longestPrefix x s
⊢ longestPrefix y s = longestPrefix x s
exact L
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
⊢ longestPrefix y s = longestPrefix x s
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
⊢ longestPrefix y s = longestPrefix x s
have Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty :=
  inter_cylinder_longestPrefix_nonempty hs hne y
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
A'y : Set.Nonempty (s ∩ cylinder y (Nat.succ (longestPrefix x s)))
⊢ longestPrefix y s = longestPrefix x s
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
⊢ longestPrefix y s = longestPrefix x s
have A'y : (s ∩ cylinder y (longestPrefix x s).succ).Nonempty :=
  Ay.mono (inter_subset_inter_right s (cylinder_anti _ L))
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
A'y : Set.Nonempty (s ∩ cylinder y (Nat.succ (longestPrefix x s)))
Z : Disjoint s (cylinder x (Nat.succ (longestPrefix x s)))
⊢ longestPrefix y s = longestPrefix x s
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
A'y : Set.Nonempty (s ∩ cylinder y (Nat.succ (longestPrefix x s)))
⊢ longestPrefix y s = longestPrefix x s
have Z := disjoint_cylinder_of_longestPrefix_lt hs xs (Nat.lt_succ_self _)
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
A'y : Set.Nonempty (s ∩ cylinder y (Nat.succ (longestPrefix x s)))
Z : Disjoint s (cylinder y (Nat.succ (longestPrefix x s)))
⊢ longestPrefix y s = longestPrefix x s
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
A'y : Set.Nonempty (s ∩ cylinder y (Nat.succ (longestPrefix x s)))
Z : Disjoint s (cylinder x (Nat.succ (longestPrefix x s)))
⊢ longestPrefix y s = longestPrefix x s
rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H] at Z
no goals
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
H : longestPrefix x s < firstDiff x y
xs : ¬x ∈ s
ys : ¬y ∈ s
L : longestPrefix x s < longestPrefix y s
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
A'y : Set.Nonempty (s ∩ cylinder y (Nat.succ (longestPrefix x s)))
Z : Disjoint s (cylinder y (Nat.succ (longestPrefix x s)))
⊢ longestPrefix y s = longestPrefix x s
exact (A'y.not_disjoint Z).elim