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 : 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))
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have I : 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)
Tactic: 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
-- 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))
I :
  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)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have neg : ∀ (I : cylinder (E := E) (f y) (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)),
  firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
Tactic: rwa [← fy, ← I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy.symm,
        firstDiff_comm _ x] at I
Cleared hypotheses: I
-- 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))
I :
  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)
neg :
  ∀ (I : cylinder (E := E) (f y) (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have neg₁ : ∀ (I : cylinder (E := E) (f y) (firstDiff (E := E) x y) = cylinder (E := E) x (firstDiff (E := E) x y)),
  firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
Tactic: rwa [← fy, ← I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy.symm,
        firstDiff_comm _ x] at I
Cleared hypotheses: I
-- 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))
I :
  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)
neg :
  ∀ (I : cylinder (E := E) (f y) (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
neg₁ :
  ∀ (I : cylinder (E := E) (f y) (firstDiff (E := E) x y) = cylinder (E := E) x (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have neg₂ : ∀ (I : f y ∈ cylinder (E := E) x (firstDiff (E := E) x y)), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
Tactic: rwa [← fy, ← I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy.symm,
        firstDiff_comm _ x] at I
Cleared hypotheses: I
-- 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))
I :
  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)
neg :
  ∀ (I : cylinder (E := E) (f y) (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
neg₁ :
  ∀ (I : cylinder (E := E) (f y) (firstDiff (E := E) x y) = cylinder (E := E) x (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
neg₂ : ∀ (I : f y ∈ cylinder (E := E) x (firstDiff (E := E) x y)), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have neg₃ : ∀ (I : firstDiff (E := E) x y ≤ firstDiff (E := E) (f y) x), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
Tactic: rwa [← fy, ← I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy.symm,
        firstDiff_comm _ x] at I
Cleared hypotheses: I
-- 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))
I :
  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)
neg :
  ∀ (I : cylinder (E := E) (f y) (firstDiff (E := E) x y) = cylinder (E := E) y (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
neg₁ :
  ∀ (I : cylinder (E := E) (f y) (firstDiff (E := E) x y) = cylinder (E := E) x (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
neg₂ : ∀ (I : f y ∈ cylinder (E := E) x (firstDiff (E := E) x y)), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
neg₃ : ∀ (I : firstDiff (E := E) x y ≤ firstDiff (E := E) (f y) x), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
have neg₄ : ∀ (I : firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)), firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)
Tactic: rwa [← fy, ← I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy.symm,
        firstDiff_comm _ x] at I
Cleared hypotheses: I
-- 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 : ∀ (ys : y ∈ s), firstDiff (E := E) x y ≤ firstDiff (E := E) (f 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 : 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
pos : ∀ (ys : y ∈ 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 : ∀ (ys : y ∉ s), firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
Tactic: by_cases ys : y ∈ s
-- 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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have A : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
Tactic: have A : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
          inter_cylinder_longestPrefix_nonempty hs hne x
-- 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
A : (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 = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
Tactic: have fx : f x = A.some := by simp_rw [f, if_neg 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 : 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
A : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
⊢ cylinder (E := E) (A.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 : A.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 (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
A : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
⊢ A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)) ∈ cylinder (E := E) x (firstDiff (E := E) x y)
have apply : firstDiff (E := E) x y ≤ longestPrefix (E := E) x s
Tactic: apply cylinder_anti x _ A.some_mem.2
-- 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
A : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = A.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 I : cylinder (E := E) (A.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 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
-- 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
A : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
I :
  cylinder (E := E) (A.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 pos : ∀ (hfxfy : f 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) (A : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty)
  (fx : f x = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)))
  (I :
    cylinder (E := E) (A.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) y
Tactic: rw [fs y ys] at hfxfy ⊢
Cleared hypotheses: hfxfy, I2, xs, ys, A, fx, I
-- 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 ≠ 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) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
I :
  cylinder (E := E) (A.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) y
have pos : ∀ (I : cylinder (E := E) (f x) (firstDiff (E := E) x y) = cylinder (E := E) x (firstDiff (E := E) x y)),
  firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
Tactic: rwa [← fx, I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at I
Cleared hypotheses: I
-- 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 ≠ 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) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
I :
  cylinder (E := E) (A.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)
pos :
  ∀ (I : cylinder (E := E) (f x) (firstDiff (E := E) x y) = cylinder (E := E) x (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
have pos₁ : ∀ (I : cylinder (E := E) (f 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) y
Tactic: rwa [← fx, I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at I
Cleared hypotheses: I
-- 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 ≠ 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) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
I :
  cylinder (E := E) (A.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)
pos :
  ∀ (I : cylinder (E := E) (f x) (firstDiff (E := E) x y) = cylinder (E := E) x (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
pos₁ :
  ∀ (I : cylinder (E := E) (f 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) y
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
have pos₂ : ∀ (I : f x ∈ cylinder (E := E) y (firstDiff (E := E) x y)), firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
Tactic: rwa [← fx, I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at I
Cleared hypotheses: I
-- 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 ≠ 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) x (longestPrefix (E := E) x s)).Nonempty
fx : f x = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
I :
  cylinder (E := E) (A.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)
pos :
  ∀ (I : cylinder (E := E) (f x) (firstDiff (E := E) x y) = cylinder (E := E) x (firstDiff (E := E) x y)),
    firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
pos₁ :
  ∀ (I : cylinder (E := E) (f 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) y
pos₂ : ∀ (I : f x ∈ cylinder (E := E) y (firstDiff (E := E) x y)), firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
have pos₃ : ∀ (I : firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y), firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y
Tactic: rwa [← fx, I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at I
Cleared hypotheses: I
-- 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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
have Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
Tactic: have Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
          inter_cylinder_longestPrefix_nonempty hs hne x