awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
⊢ cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)

Tactic:
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
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
I1 :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)
rw : Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)) ∈ cylinder (E := E) y (firstDiff (E := E) x y)
⊢ cylinder (E := E) y (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)

Tactic:
rw [eq_comm, ← mem_cylinder_iff_eq]

Premises used: eq_comm, PiNat.mem_cylinder_iff_eq
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
I1 :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)
⊢ Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)) ∈ cylinder (E := E) y (firstDiff (E := E) x y)

Tactic:
cylinder_anti y H.2 Ay.some_mem.2

Premises used: Set.Nonempty.some_mem, And.right, PiNat.cylinder_anti
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
I1 :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)
⊢ Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)) ∈ cylinder (E := E) y (firstDiff (E := E) x y)

Tactic:
exact cylinder_anti y H.2 Ay.some_mem.2

Premises used: Set.Nonempty.some_mem, And.right, PiNat.cylinder_anti
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
I1 :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)
⊢ cylinder (E := E) y (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)

Tactic:
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
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
I1 :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)
I3 :
  cylinder (E := E) y (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)
rw :
  cylinder (E := E) x (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)
rw₁ :
  cylinder (E := E) y (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)
rw₂ rw₃ :
  cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)
⊢ cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)

Tactic:
rw [I1, I2, I3]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
I1 :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)
I3 :
  cylinder (E := E) y (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)
⊢ cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)

Tactic:
have : cylinder Ax.some (firstDiff x y) = cylinder Ay.some (firstDiff x y) := by
            rw [I1, I2, I3]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
I1 :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)
I3 :
  cylinder (E := E) y (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)
this :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)

Tactic:
rw [← fx, ← fy, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at this

Premises used: PiNat.mem_cylinder_iff_le_firstDiff, PiNat.mem_cylinder_iff_eq
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
I1 :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)
I3 :
  cylinder (E := E) y (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)
this : firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)

Tactic:
this
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : (x : (n : ℕ) → E n) → (n : ℕ) → E n :=
  fun (x : (n : ℕ) → E n) ↦ if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s
I1 :
  cylinder (E := E) (Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) (firstDiff (E := E) x y) =
    cylinder (E := E) x (firstDiff (E := E) x y)
I3 :
  cylinder (E := E) y (firstDiff (E := E) x y) =
    cylinder (E := E) (Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y)
this : firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)

Tactic:
exact this
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
rcases :
  ∀ (f : ((n : ℕ) → E n) → (n : ℕ) → E n) (fs : ∀ x ∈ s, f x = x) (frange : range f = s) (hf : LipschitzWith 1 f),
    ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n),
      (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f
⊢ ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n),
    (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f

Tactic:
rcases exists_lipschitz_retraction_of_isClosed hs hne with ⟨f, fs, frange, hf⟩

Premises used: PiNat.exists_lipschitz_retraction_of_isClosed
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n
fs : ∀ x ∈ s, f x = x
frange : range f = s
hf : LipschitzWith 1 f
⊢ ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n),
    (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f

Tactic:
⟨f, fs, frange, hf.continuous⟩

Premises used: LipschitzWith.continuous, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n
fs : ∀ x ∈ s, f x = x
frange : range f = s
hf : LipschitzWith 1 f
⊢ ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n),
    (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f

Tactic:
exact ⟨f, fs, frange, hf.continuous⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
⊢ ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n),
    (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f

Tactic:
exists_retraction_of_isClosed hs hne

Premises used: PiNat.exists_retraction_of_isClosed
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
obtain :
  ∀ (f : ((n : ℕ) → E n) → (n : ℕ) → E n) (f_cont : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f)
    (hs : IsClosed[Pi.topologicalSpace] (range f)) (hne : (range f).Nonempty) (fs : ∀ x ∈ range f, f x = x),
    ∃ (f_1 : ((n : ℕ) → E n) → (↑(range f) : Type u_1)),
      (∀ (x : (↑(range f) : Type u_1)), f_1 (↑x : (n : ℕ) → E n) = x) ∧
        Surjective f_1 ∧ Continuous[Pi.topologicalSpace, instTopologicalSpaceSubtype] f_1
⊢ ∃ (f : ((n : ℕ) → E n) → (↑s : Type u_1)),
    (∀ (x : (↑s : Type u_1)), f (↑x : (n : ℕ) → E n) = x) ∧
      Surjective f ∧ Continuous[Pi.topologicalSpace, instTopologicalSpaceSubtype] f

Tactic:
obtain ⟨f, fs, rfl, f_cont⟩ :
    ∃ f : (∀ n, E n) → ∀ n, E n, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f :=
    exists_retraction_of_isClosed hs hne

Premises used: PiNat.exists_retraction_of_isClosed, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f
hs : IsClosed[Pi.topologicalSpace] (range f)
hne : (range f).Nonempty
fs : ∀ x ∈ range f, f x = x
⊢ ∀ (x : (↑(range f) : Type u_1)), rangeFactorization f (↑x : (n : ℕ) → E n) = x

Tactic:
have A : ∀ x : range f, rangeFactorization f x = x := fun x ↦ Subtype.ext <| fs x x.2
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f
hs : IsClosed[Pi.topologicalSpace] (range f)
hne : (range f).Nonempty
fs : ∀ x ∈ range f, f x = x
A : ∀ (x : (↑(range f) : Type u_1)), rangeFactorization f (↑x : (n : ℕ) → E n) = x
⊢ ∃ (f_1 : ((n : ℕ) → E n) → (↑(range f) : Type u_1)),
    (∀ (x : (↑(range f) : Type u_1)), f_1 (↑x : (n : ℕ) → E n) = x) ∧
      Surjective f_1 ∧ Continuous[Pi.topologicalSpace, instTopologicalSpaceSubtype] f_1

Tactic:
⟨rangeFactorization f, A, fun x => ⟨x, A x⟩, f_cont.subtype_mk _⟩

Premises used: Continuous.subtype_mk, And.intro, Exists.intro, Set.rangeFactorization, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f
hs : IsClosed[Pi.topologicalSpace] (range f)
hne : (range f).Nonempty
fs : ∀ x ∈ range f, f x = x
A : ∀ (x : (↑(range f) : Type u_1)), rangeFactorization f (↑x : (n : ℕ) → E n) = x
⊢ ∃ (f_1 : ((n : ℕ) → E n) → (↑(range f) : Type u_1)),
    (∀ (x : (↑(range f) : Type u_1)), f_1 (↑x : (n : ℕ) → E n) = x) ∧
      Surjective f_1 ∧ Continuous[Pi.topologicalSpace, instTopologicalSpaceSubtype] f_1

Tactic:
exact ⟨rangeFactorization f, A, fun x => ⟨x, A x⟩, f_cont.subtype_mk _⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
⊢ 0 < 1 / 2

Tactic:
have I0 : (0 : ℝ) < 1 / 2 := by simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
⊢ 1 / 2 < 1

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
⊢ 1 / 2 < 1

Tactic:
have I1 : (1 / 2 : ℝ) < 1 := by norm_num
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
rcases :
  ∀ (u : ℕ → α) (hu : DenseRange u),
    ∃ (f : (ℕ → ℕ) → α), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f
⊢ ∃ (f : (ℕ → ℕ) → α), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f

Tactic:
rcases exists_dense_seq α with ⟨u, hu⟩

Premises used: TopologicalSpace.exists_dense_seq
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
inst : MetricSpace α
inst_1 : CompleteSpace α
inst_2 : SecondCountableTopology α
inst_3 : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x : ℕ → ℕ | Set.Nonempty.{u_2} (α := α) (⋂ (n : ℕ), closedBall (u (x n)) ((1 / 2) ^ n))}
g : (↑s : Type) → α :=
  fun (x : (↑s : Type)) ↦ Set.Nonempty.some (s := ⋂ (n : ℕ), closedBall (u ((↑x : ℕ → ℕ) n)) ((1 / 2) ^ n)) ⋯
⊢ ∀ (x : (↑s : Type)) (n : ℕ), dist (g x) (u ((↑x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n

Tactic:
have A : ∀ (x : s) (n : ℕ), dist (g x) (u ((x : ℕ → ℕ) n)) ≤ (1 / 2) ^ n := fun x n =>
    (mem_iInter.1 x.2.some_mem n :)