awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have fx : f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Tactic: have fx : f x = Ax.some := by simp_rw [f, if_neg xs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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))
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
Tactic: have Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty :=
          inter_cylinder_longestPrefix_nonempty hs hne y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
Tactic: have fy : f y = Ay.some := by simp_rw [f, if_neg ys]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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))
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have pos : ∀ (H : longestPrefix (E := E) x s < firstDiff (E := E) x y ∨ longestPrefix (E := E) y s < firstDiff (E := E) x y),
  firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
Tactic: by_cases! H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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))
pos :
  ∀ (H : longestPrefix (E := E) x s < firstDiff (E := E) x y ∨ longestPrefix (E := E) y s < firstDiff (E := E) x y),
    firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have neg : ∀ (H : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s ∧ firstDiff (E := E) x y ≤ longestPrefix (E := E) y s),
  firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
Tactic: by_cases! H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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 : longestPrefix (E := E) x s < firstDiff (E := E) x y ∨ longestPrefix (E := E) y s < firstDiff (E := E) x y
⊢ cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
have inl : ∀ (H : longestPrefix (E := E) x s < firstDiff (E := E) x y),
  cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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 : longestPrefix (E := E) x s < firstDiff (E := E) x y ∨ longestPrefix (E := E) y s < firstDiff (E := E) x y
inl :
  ∀ (H : longestPrefix (E := E) x s < firstDiff (E := E) x y),
    cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
⊢ cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
have inr : ∀ (H : longestPrefix (E := E) y s < firstDiff (E := E) x y),
  cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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 : longestPrefix (E := E) y s < firstDiff (E := E) x y
⊢ cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
have inr : cylinder (E := E) y (longestPrefix (E := E) y s) = cylinder (E := E) x (longestPrefix (E := E) x s)
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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 : longestPrefix (E := E) y s < firstDiff (E := E) x y
⊢ cylinder (E := E) y (longestPrefix (E := E) y s) = cylinder (E := E) x (longestPrefix (E := E) x s)
have H₁ : longestPrefix (E := E) y s < firstDiff (E := E) y x
Tactic: rw [firstDiff_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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 : longestPrefix (E := E) x s < firstDiff (E := E) x y ∨ longestPrefix (E := E) y s < firstDiff (E := E) x y
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have this : cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
Tactic: have : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s) := by
            rcases H with H | H
            · exact cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff hs hne H xs ys
            · symm
              rw [firstDiff_comm] at H
              exact cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff hs hne H ys xs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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 : longestPrefix (E := E) x s < firstDiff (E := E) x y ∨ longestPrefix (E := E) y s < firstDiff (E := E) x y
this : cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have hfxfy₁ : Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)) ≠
  Ay₁.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
Tactic: rw [fx, fy] at hfxfy
Cleared hypotheses: hfxfy, fx, Ay, fy, H, this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
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
hfxfy :
  Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)) ≠
    Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
fy : f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
H : longestPrefix (E := E) x s < firstDiff (E := E) x y ∨ longestPrefix (E := E) y s < firstDiff (E := E) x y
this : cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have apply : Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)) =
  Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
Tactic: apply (hfxfy _).elim
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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)
have rw : Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)) ∈ cylinder (E := E) x (firstDiff (E := E) x y)
Tactic: rw [← mem_cylinder_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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)
have rw : Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)) ∈ cylinder (E := E) y (firstDiff (E := E) x y)
Tactic: rw [eq_comm, ← mem_cylinder_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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)
have 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)
Tactic: rw [I1, I2, I3]