-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem exists_lipschitz_retraction_of_isClosed {s : Set (∀ n, E n)} (hs : IsClosed s)
    (hne : s.Nonempty) :
    ∃ f : (∀ n, E n) → ∀ n, E n, (∀ x ∈ s, f x = x) ∧ range f = s ∧ LipschitzWith 1 f

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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 : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
hfxfy : Ax.some ≠ Ay.some
fy : f y = Ay.some
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
this : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
⊢ Ax.some = Ay.some

Tactic:
congr

Result:
no goals

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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 : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)

Tactic:
rw [← mem_cylinder_iff_eq]

Result:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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 : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ Ax.some ∈ cylinder x (firstDiff x y)

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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 : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)
⊢ cylinder y (firstDiff x y) = cylinder Ay.some (firstDiff x y)

Tactic:
rw [eq_comm, ← mem_cylinder_iff_eq]

Result:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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 : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)
⊢ Ay.some ∈ cylinder y (firstDiff x y)

Proof state:
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 : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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

Tactic:
suffices firstDiff x y ≤ firstDiff (f x) (f y) by
  simpa [dist_eq_of_ne hxy, dist_eq_of_ne hfxfy]

Result:
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 : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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)

Proof state:
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 : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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)

Tactic:
by_cases ys : y ∈ s

Result:
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 : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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 : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x => if x ∈ s then x else ⋯.some
fs : ∀ 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)