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)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix (E := E) x s < firstDiff (E := E) y x
xs : x ∉ s
ys : y ∉ s
L : longestPrefix (E := E) y s < longestPrefix (E := E) x s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
Z : Disjoint s (cylinder (E := E) y (longestPrefix (E := E) x s))
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
have Z₁ : Disjoint s (cylinder (E := E) x (longestPrefix (E := E) x s))
Tactic: rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H.le] at Z
Cleared hypotheses: Z
-- 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)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix (E := E) x s < firstDiff (E := E) x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix (E := E) x s < longestPrefix (E := E) y s
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
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)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix (E := E) x s < firstDiff (E := E) x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix (E := E) x s < longestPrefix (E := E) y s
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
have A'y : (s ∩ cylinder (E := E) y (longestPrefix (E := E) x s).succ).Nonempty
Tactic: have A'y : (s ∩ cylinder y (longestPrefix x s).succ).Nonempty :=
        Ay.mono (inter_subset_inter_right s (cylinder_anti _ L))
-- 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)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix (E := E) x s < firstDiff (E := E) x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix (E := E) x s < longestPrefix (E := E) y s
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
A'y : (s ∩ cylinder (E := E) y (longestPrefix (E := E) x s).succ).Nonempty
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
have Z : Disjoint s (cylinder (E := E) x (longestPrefix (E := E) x s).succ)
Tactic: have Z := disjoint_cylinder_of_longestPrefix_lt hs xs (Nat.lt_succ_self _)
-- 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)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix (E := E) x s < firstDiff (E := E) x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix (E := E) x s < longestPrefix (E := E) y s
Ay : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
A'y : (s ∩ cylinder (E := E) y (longestPrefix (E := E) x s).succ).Nonempty
Z : Disjoint s (cylinder (E := E) x (longestPrefix (E := E) x s).succ)
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
have Z₁ : Disjoint s (cylinder (E := E) y (longestPrefix (E := E) x s).succ)
Tactic: rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H] at Z
Cleared hypotheses: Z
-- 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)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix (E := E) x s < firstDiff (E := E) x y
xs : x ∉ s
ys : y ∉ s
⊢ cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
have l_eq : longestPrefix (E := E) y s = longestPrefix (E := E) x s
Tactic: have l_eq : longestPrefix y s = longestPrefix x s := by
    rcases lt_trichotomy (longestPrefix y s) (longestPrefix x s) with (L | L | L)
    · have Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
        inter_cylinder_longestPrefix_nonempty hs hne x
      have Z := disjoint_cylinder_of_longestPrefix_lt hs ys L
      rw [firstDiff_comm] at H
      rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H.le] at Z
      exact (Ax.not_disjoint Z).elim
    · exact L
    · have Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty :=
        inter_cylinder_longestPrefix_nonempty hs hne y
      have A'y : (s ∩ cylinder y (longestPrefix x s).succ).Nonempty :=
        Ay.mono (inter_subset_inter_right s (cylinder_anti _ L))
      have Z := disjoint_cylinder_of_longestPrefix_lt hs xs (Nat.lt_succ_self _)
      rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H] at Z
      exact (A'y.not_disjoint Z).elim
-- 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)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix (E := E) x s < firstDiff (E := E) x y
xs : x ∉ s
ys : y ∉ s
l_eq : longestPrefix (E := E) y s = longestPrefix (E := E) x s
⊢ cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)
have rw : x ∈ cylinder (E := E) y (longestPrefix (E := E) x s)
Tactic: rw [l_eq, ← 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))
⊢ ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n), (∀ x ∈ s, f x = x) ∧ range f = s ∧ LipschitzWith 1 f
have fs : ∀ x ∈ s, f x = x
Tactic: have fs : ∀ x ∈ s, f x = x := fun x xs => by simp [f, xs]
-- 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
⊢ ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n), (∀ x ∈ s, f x = x) ∧ range f = s ∧ LipschitzWith 1 f
have refine_1 : range f = s
Tactic: refine ⟨f, fs, ?_, ?_⟩
-- 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
refine_1 : range f = s
⊢ ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n), (∀ x ∈ s, f x = x) ∧ range f = s ∧ LipschitzWith 1 f
have refine_2 : LipschitzWith 1 f
Tactic: refine ⟨f, fs, ?_, ?_⟩
-- 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
⊢ range f = s
have refine_1 : range f ⊆ s
Tactic: apply Subset.antisymm
-- 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
refine_1 : range f ⊆ s
⊢ range f = s
have refine_1₁ : s ⊆ range f
Tactic: apply Subset.antisymm
-- 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
y : (n : ℕ) → E n
⊢ f y ∈ s
have pos : ∀ (hy : y ∈ s), f y ∈ s
Tactic: by_cases hy : y ∈ s
-- 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
y : (n : ℕ) → E n
pos : ∀ (hy : y ∈ s), f y ∈ s
⊢ f y ∈ s
have neg : ∀ (hy : y ∉ s), f y ∈ s
Tactic: by_cases hy : y ∈ s
-- 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 : (n : ℕ) → E n
hx : x ∈ s
⊢ x ∈ range f
have refine_1 : f x ∈ range f
Tactic: rw [← fs x hx]
-- 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
⊢ LipschitzWith 1 f
have refine_2 : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
Tactic: refine LipschitzWith.mk_one fun 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
⊢ dist (f x) (f y) ≤ dist x y
have refine_2 : dist (f x) (f x) ≤ dist x x
Tactic: rcases eq_or_ne x y with (rfl | hxy)
Cleared hypotheses: 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
refine_2 : dist (f x) (f x) ≤ dist x x
⊢ dist (f x) (f y) ≤ dist x y
have refine_2₁ : ∀ (hxy : x ≠ y), dist (f x) (f y) ≤ dist x y
Tactic: rcases eq_or_ne x y with (rfl | hxy)
-- 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
⊢ dist (f x) (f y) ≤ dist x y
have refine_2 : ∀ (h' : f x = f y), dist (f x) (f y) ≤ dist x y
Tactic: rcases eq_or_ne (f x) (f y) with (h' | hfxfy)
-- 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
refine_2 : ∀ (h' : f x = f y), dist (f x) (f y) ≤ dist x y
⊢ dist (f x) (f y) ≤ dist x y
have refine_2₁ : ∀ (hfxfy : f x ≠ f y), dist (f x) (f y) ≤ dist x y
Tactic: rcases eq_or_ne (f x) (f y) with (h' | hfxfy)
-- 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
⊢ cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
have rw : x ∈ cylinder (E := E) y (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
⊢ dist (f x) (f y) ≤ dist x y
have I2 : cylinder (E := E) x (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)
Tactic: have I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y) := by
      rw [← mem_cylinder_iff_eq]
      apply mem_cylinder_firstDiff
-- 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)
⊢ dist (f x) (f y) ≤ dist x y
have refine_2 : firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
Tactic: suffices firstDiff x y ≤ firstDiff (f x) (f y) by
      simpa [dist_eq_of_ne hxy, dist_eq_of_ne hfxfy]
-- 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)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have pos : ∀ (xs : x ∈ s), firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
Tactic: by_cases xs : x ∈ s
-- 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)
pos : ∀ (xs : x ∈ s), 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 : ∀ (xs : x ∉ s), firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
Tactic: by_cases xs : x ∈ s
-- 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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have pos : ∀ (hfxfy : 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), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
Tactic: rw [fs x xs] at hfxfy ⊢
Cleared hypotheses: hfxfy, I2, xs
-- 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 : 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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have pos : ∀ (ys : y ∈ s), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
Tactic: by_cases ys : y ∈ s
-- 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 : 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
pos : ∀ (ys : y ∈ s), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have neg : ∀ (ys : y ∉ s), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
Tactic: by_cases ys : y ∈ s
-- 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 : 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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have pos : firstDiff (E := E) x y ≤ firstDiff (E := E) x y
Tactic: rw [fs y ys]
-- 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 : 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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have A : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
Tactic: have A : (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 : 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
A : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have fy : f y = A.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
Tactic: have fy : f y = A.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 : 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
A : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = A.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
⊢ cylinder (E := E) (A.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) (firstDiff (E := E) x y) =
    cylinder (E := E) y (firstDiff (E := E) x y)
have rw : A.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)) ∈ cylinder (E := E) y (firstDiff (E := E) y x)
Tactic: rw [← mem_cylinder_iff_eq, firstDiff_comm]
-- 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 : 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
A : (s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)).Nonempty
fy : f y = A.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
⊢ A.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s)) ∈ cylinder (E := E) y (firstDiff (E := E) y x)
have apply : firstDiff (E := E) y x ≤ longestPrefix (E := E) y s
Tactic: apply cylinder_anti y _ A.some_mem.2