English
If longestPrefix x s < firstDiff x y and x,y ∉ s, then cylinder x (longestPrefix x s) equals cylinder y (longestPrefix y s).
Русский
Если longestPrefix x s < firstDiff x y и x,y ∉ s, то цилиндр x( longestPrefix x s ) равен цилиндру y( longestPrefix y s ).
LaTeX
$$$$ \text{If } \text{longestPrefix}(x,s) < \text{firstDiff}(x,y) \text{ and } x,y \notin s, \; \mathrm{cylinder}(x,\text{longestPrefix}(x,s)) = \mathrm{cylinder}(y,\text{longestPrefix}(y,s)) $$$$
Lean4
/-- If two points `x, y` coincide up to length `n`, and the longest common prefix of `x` with `s`
is strictly shorter than `n`, then the longest common prefix of `y` with `s` is the same, and both
cylinders of this length based at `x` and `y` coincide. -/
theorem cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff {x y : ∀ n, E n} {s : Set (∀ n, E n)} (hs : IsClosed s)
(hne : s.Nonempty) (H : longestPrefix x s < firstDiff x y) (xs : x ∉ s) (ys : y ∉ s) :
cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s) :=
by
have l_eq : longestPrefix y s = longestPrefix x s :=
by
rcases lt_trichotomy (longestPrefix y s) (longestPrefix x s) with (L | L | L)
· have Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty := inter_cylinder_longestPrefix_nonempty hs hne x
have Z := disjoint_cylinder_of_longestPrefix_lt hs ys L
rw [firstDiff_comm] at H
rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H.le] at Z
exact (Ax.not_disjoint Z).elim
· exact L
· have Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty := inter_cylinder_longestPrefix_nonempty hs hne y
have A'y : (s ∩ cylinder y (longestPrefix x s).succ).Nonempty :=
Ay.mono (inter_subset_inter_right s (cylinder_anti _ L))
have Z := disjoint_cylinder_of_longestPrefix_lt hs xs (Nat.lt_succ_self _)
rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H] at Z
exact (A'y.not_disjoint Z).elim
rw [l_eq, ← mem_cylinder_iff_eq]
exact cylinder_anti y H.le (mem_cylinder_firstDiff x y)
