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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
⊢ ∃ f, (∀ (x : (n : ℕ) → E n), x ∈ s → f x = x) ∧ range f = s ∧ LipschitzWith 1 f
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
⊢ ∃ f, (∀ (x : (n : ℕ) → E n), x ∈ s → f x = x) ∧ range f = s ∧ LipschitzWith 1 f
set f := fun x => if x ∈ s then x else (inter_cylinder_longestPrefix_nonempty hs hne x).some
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ ∃ f, (∀ (x : (n : ℕ) → E n), x ∈ s → f x = x) ∧ range f = s ∧ LipschitzWith 1 f
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
⊢ ∃ f, (∀ (x : (n : ℕ) → E n), x ∈ s → f x = x) ∧ range f = s ∧ LipschitzWith 1 f
have fs : ∀ x ∈ s, f x = x := fun x xs => by simp [xs]
case refine'_1
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ range f = s

case refine'_2
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ LipschitzWith 1 f
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ ∃ f, (∀ (x : (n : ℕ) → E n), x ∈ s → f x = x) ∧ range f = s ∧ LipschitzWith 1 f
refine' ⟨f, fs, _, _⟩
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
x : (n : ℕ) → E n
xs : x ∈ s
⊢ f x = x
simp [xs]
case refine'_1.h₁
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ range f ⊆ s

case refine'_1.h₂
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ s ⊆ range f
case refine'_1
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ range f = s
apply Subset.antisymm
case refine'_1.h₁.intro
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
y : (n : ℕ) → E n
⊢ f y ∈ s
case refine'_1.h₁
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ range f ⊆ s
rintro x ⟨y, rfl⟩
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
y : (n : ℕ) → E n
hy : y ∈ s
⊢ f y ∈ s

case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
y : (n : ℕ) → E n
hy : ¬y ∈ s
⊢ f y ∈ s
case refine'_1.h₁.intro
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
y : (n : ℕ) → E n
⊢ f y ∈ s
by_cases hy : y ∈ s
no goals
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
y : (n : ℕ) → E n
hy : ¬y ∈ s
⊢ f y ∈ s
simpa [if_neg hy] using (inter_cylinder_longestPrefix_nonempty hs hne y).choose_spec.1
no goals
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
y : (n : ℕ) → E n
hy : y ∈ s
⊢ f y ∈ s
rwa [fs y hy]
case refine'_1.h₂
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x : (n : ℕ) → E n
hx : x ∈ s
⊢ x ∈ range f
case refine'_1.h₂
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ s ⊆ range f
intro x hx
case refine'_1.h₂
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x : (n : ℕ) → E n
hx : x ∈ s
⊢ f x ∈ range f
case refine'_1.h₂
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x : (n : ℕ) → E n
hx : x ∈ s
⊢ x ∈ range f
rw [← fs x hx]
no goals
case refine'_1.h₂
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x : (n : ℕ) → E n
hx : x ∈ s
⊢ f x ∈ range f
exact mem_range_self _
case refine'_2
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
⊢ dist (f x) (f y) ≤ dist x y
case refine'_2
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
⊢ LipschitzWith 1 f
refine LipschitzWith.mk_one fun x y => ?_
case refine'_2.inl
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x : (n : ℕ) → E n
⊢ dist (f x) (f x) ≤ dist x x

case refine'_2.inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
⊢ dist (f x) (f y) ≤ dist x y
case refine'_2
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
⊢ dist (f x) (f y) ≤ dist x y
rcases eq_or_ne x y with (rfl | hxy)
case refine'_2.inr.inl
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
h' : f x = f y
⊢ dist (f x) (f y) ≤ dist x y

case refine'_2.inr.inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
⊢ dist (f x) (f y) ≤ dist x y
case refine'_2.inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
⊢ dist (f x) (f y) ≤ dist x y
rcases eq_or_ne (f x) (f y) with (h' | hfxfy)
case refine'_2.inr.inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
⊢ dist (f x) (f y) ≤ dist x y
case refine'_2.inr.inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
⊢ dist (f x) (f y) ≤ dist x y
have I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y) := by
  rw [← mem_cylinder_iff_eq]
  apply mem_cylinder_firstDiff
case refine'_2.inr.inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case refine'_2.inr.inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
⊢ dist (f x) (f y) ≤ dist x y
suffices firstDiff x y ≤ firstDiff (f x) (f y) by
  simpa [dist_eq_of_ne hxy, dist_eq_of_ne hfxfy]
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case refine'_2.inr.inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
by_cases xs : x ∈ s
no goals
case refine'_2.inl
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x : (n : ℕ) → E n
⊢ dist (f x) (f x) ≤ dist x x
simp
no goals
case refine'_2.inr.inl
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
h' : f x = f y
⊢ dist (f x) (f y) ≤ dist x y
simp [h', dist_nonneg]
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
⊢ x ∈ cylinder y (firstDiff x y)
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
⊢ cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
rw [← mem_cylinder_iff_eq]
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
⊢ x ∈ cylinder y (firstDiff x y)
apply mem_cylinder_firstDiff
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
this : firstDiff x y ≤ firstDiff (f x) (f y)
⊢ dist (f x) (f y) ≤ dist x y
simpa [dist_eq_of_ne hxy, dist_eq_of_ne hfxfy]
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
⊢ firstDiff x y ≤ firstDiff x (f y)
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
rw [fs x xs] at hfxfy ⊢
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : y ∈ s
⊢ firstDiff x y ≤ firstDiff x (f y)

case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
⊢ firstDiff x y ≤ firstDiff x (f y)
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
⊢ firstDiff x y ≤ firstDiff x (f y)
by_cases ys : y ∈ s
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
⊢ firstDiff x y ≤ firstDiff x (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
⊢ firstDiff x y ≤ firstDiff x (f y)
have A : (s ∩ cylinder y (longestPrefix y s)).Nonempty :=
  inter_cylinder_longestPrefix_nonempty hs hne y
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some A
⊢ firstDiff x y ≤ firstDiff x (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
⊢ firstDiff x y ≤ firstDiff x (f y)
have fy : f y = A.some := by simp_rw [if_neg ys]
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some A
I : cylinder (Set.Nonempty.some A) (firstDiff x y) = cylinder y (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff x (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some A
⊢ firstDiff x y ≤ firstDiff x (f y)
have I : cylinder A.some (firstDiff x y) = cylinder y (firstDiff x y) := by
  rw [← mem_cylinder_iff_eq, firstDiff_comm]
  apply cylinder_anti y _ A.some_mem.2
  exact firstDiff_le_longestPrefix hs ys xs
no goals
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some A
I : cylinder (Set.Nonempty.some A) (firstDiff x y) = cylinder y (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff x (f y)
rwa [← fy, ← I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy.symm,
  firstDiff_comm _ x] at I
no goals
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : y ∈ s
⊢ firstDiff x y ≤ firstDiff x (f y)
rw [fs y ys]
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
⊢ f y = Set.Nonempty.some A
simp_rw [if_neg ys]
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some A
⊢ Set.Nonempty.some A ∈ cylinder y (firstDiff y x)
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some A
⊢ cylinder (Set.Nonempty.some A) (firstDiff x y) = cylinder y (firstDiff x y)
rw [← mem_cylinder_iff_eq, firstDiff_comm]
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some A
⊢ firstDiff y x ≤ longestPrefix y 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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some A
⊢ Set.Nonempty.some A ∈ cylinder y (firstDiff y x)
apply cylinder_anti y _ A.some_mem.2
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : ¬y ∈ s
A : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some A
⊢ firstDiff y x ≤ longestPrefix y s
exact firstDiff_le_longestPrefix hs ys xs
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
by_cases ys : y ∈ s
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have A : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
  inter_cylinder_longestPrefix_nonempty hs hne x
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have fx : f x = A.some := by simp_rw [if_neg xs]
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
I : cylinder (Set.Nonempty.some A) (firstDiff x y) = cylinder x (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have I : cylinder A.some (firstDiff x y) = cylinder x (firstDiff x y) := by
  rw [← mem_cylinder_iff_eq]
  apply cylinder_anti x _ A.some_mem.2
  apply firstDiff_le_longestPrefix hs xs ys
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
I : cylinder (Set.Nonempty.some A) (firstDiff x y) = cylinder x (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) y
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
I : cylinder (Set.Nonempty.some A) (firstDiff x y) = cylinder x (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
rw [fs y ys] at hfxfy⊢
no goals
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
I : cylinder (Set.Nonempty.some A) (firstDiff x y) = cylinder x (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) y
rwa [← fx, I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at I
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
⊢ f x = Set.Nonempty.some A
simp_rw [if_neg xs]
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
⊢ Set.Nonempty.some A ∈ cylinder x (firstDiff x y)
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
⊢ cylinder (Set.Nonempty.some A) (firstDiff x y) = cylinder x (firstDiff x y)
rw [← mem_cylinder_iff_eq]
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
⊢ firstDiff x y ≤ longestPrefix 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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
⊢ Set.Nonempty.some A ∈ cylinder x (firstDiff x y)
apply cylinder_anti x _ A.some_mem.2
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : y ∈ s
A : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some A
⊢ firstDiff x y ≤ longestPrefix x s
apply firstDiff_le_longestPrefix hs xs ys
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
  inter_cylinder_longestPrefix_nonempty hs hne x
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have fx : f x = Ax.some := by simp_rw [if_neg xs]
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty :=
  inter_cylinder_longestPrefix_nonempty hs hne y
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have fy : f y = Ay.some := by simp_rw [if_neg ys]
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : ¬(longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
by_cases H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
⊢ f x = Set.Nonempty.some Ax
simp_rw [if_neg xs]
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
⊢ f y = Set.Nonempty.some Ay
simp_rw [if_neg ys]
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
hfxfy : Set.Nonempty.some Ax ≠ Set.Nonempty.some Ay
fy : f y = Set.Nonempty.some Ay
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
this : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
this : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
rw [fx, fy] at hfxfy
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
hfxfy : Set.Nonempty.some Ax ≠ Set.Nonempty.some Ay
fy : f y = Set.Nonempty.some Ay
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
this : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
⊢ Set.Nonempty.some Ax = Set.Nonempty.some Ay
case pos
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
hfxfy : Set.Nonempty.some Ax ≠ Set.Nonempty.some Ay
fy : f y = Set.Nonempty.some Ay
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
this : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
apply (hfxfy _).elim
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
hfxfy : Set.Nonempty.some Ax ≠ Set.Nonempty.some Ay
fy : f y = Set.Nonempty.some Ay
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
this : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
⊢ Set.Nonempty.some Ax = Set.Nonempty.some Ay
congr
case inl
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix x s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)

case inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix y s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y 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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
cases' H with H H
no goals
case inl
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix x s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
exact cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff hs hne H xs ys
case inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix y s < firstDiff x y
⊢ cylinder y (longestPrefix y s) = cylinder x (longestPrefix x s)
case inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix y s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
symm
case inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix y s < firstDiff y x
⊢ cylinder y (longestPrefix y s) = cylinder x (longestPrefix x s)
case inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix y s < firstDiff x y
⊢ cylinder y (longestPrefix y s) = cylinder x (longestPrefix x s)
rw [firstDiff_comm] at H
no goals
case inr
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : longestPrefix y s < firstDiff y x
⊢ cylinder y (longestPrefix y s) = cylinder x (longestPrefix x s)
exact cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff hs hne H ys xs
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : ¬(longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
push_neg  at H
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y) := by
  rw [← mem_cylinder_iff_eq]
  exact cylinder_anti x H.1 Ax.some_mem.2
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
I3 : cylinder y (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have I3 : cylinder y (firstDiff x y) = cylinder Ay.some (firstDiff x y) := by
  rw [eq_comm, ← mem_cylinder_iff_eq]
  exact cylinder_anti y H.2 Ay.some_mem.2
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
I3 : cylinder y (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
this : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
I3 : cylinder y (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
have : cylinder Ax.some (firstDiff x y) = cylinder Ay.some (firstDiff x y) := by
  rw [I1, I2, I3]
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
I3 : cylinder y (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
this : firstDiff x y ≤ firstDiff (f x) (f y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
I3 : cylinder y (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
this : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
rw [← fx, ← fy, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at this
no goals
case neg
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
I3 : cylinder y (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
this : firstDiff x y ≤ firstDiff (f x) (f y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
exact this
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ Set.Nonempty.some Ax ∈ cylinder x (firstDiff x y)
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
rw [← mem_cylinder_iff_eq]
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ Set.Nonempty.some Ax ∈ cylinder x (firstDiff x y)
exact cylinder_anti x H.1 Ax.some_mem.2
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
⊢ Set.Nonempty.some Ay ∈ cylinder y (firstDiff x y)
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
⊢ cylinder y (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
rw [eq_comm, ← mem_cylinder_iff_eq]
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
⊢ Set.Nonempty.some Ay ∈ cylinder y (firstDiff x y)
exact cylinder_anti y H.2 Ay.some_mem.2
no goals
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
f : ((n : ℕ) → E n) → (n : ℕ) → E n :=
  fun x => if x ∈ s then x else Set.Nonempty.some (_ : Set.Nonempty (s ∩ cylinder x (longestPrefix x s)))
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : ¬x ∈ s
ys : ¬y ∈ s
Ax : Set.Nonempty (s ∩ cylinder x (longestPrefix x s))
fx : f x = Set.Nonempty.some Ax
Ay : Set.Nonempty (s ∩ cylinder y (longestPrefix y s))
fy : f y = Set.Nonempty.some Ay
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder x (firstDiff x y)
I3 : cylinder y (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
⊢ cylinder (Set.Nonempty.some Ax) (firstDiff x y) = cylinder (Set.Nonempty.some Ay) (firstDiff x y)
rw [I1, I2, I3]