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 : 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) y x ≤ longestPrefix (E := E) y s

Tactic:
firstDiff_le_longestPrefix hs ys xs

Premises used: PiNat.firstDiff_le_longestPrefix
-- 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 : 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) y x ≤ longestPrefix (E := E) y s

Tactic:
exact firstDiff_le_longestPrefix hs ys xs

Premises used: PiNat.firstDiff_le_longestPrefix
-- 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 : 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)

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
-- 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 : 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)
neg₄ neg₅ neg₆ neg₇ :
  ∀ (I : firstDiff (E := E) x y ≤ firstDiff (E := E) x (f y)), 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

Premises used: Ne.symm, PiNat.firstDiff_comm, 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
pos : ∀ (ys : y ∈ s), firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)
neg : ∀ (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)

Tactic:
by_cases ys : y ∈ s
-- 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
⊢ (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
-- 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
A : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
simp_rw :
  (if x ∈ s then x else ⋯.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))
⊢ f x = A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))

Tactic:
simp_rw [f, if_neg xs]

Premises used: if_neg
-- 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
A : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
⊢ 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]
-- 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
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))
rw : A.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)) ∈ cylinder (E := E) x (firstDiff (E := E) x y)
⊢ 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:
rw [← mem_cylinder_iff_eq]

Premises used: 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
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))
apply : firstDiff (E := E) x y ≤ 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)

Tactic:
apply cylinder_anti x _ A.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
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 ≤ longestPrefix (E := E) x s

Tactic:
apply firstDiff_le_longestPrefix hs xs ys

Premises used: PiNat.firstDiff_le_longestPrefix
-- 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
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)

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
-- 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
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 :
  ∀ (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
⊢ firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) (f y)

Tactic:
rw [fs y ys] at hfxfy ⊢
-- 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 ≠ 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
pos₃ pos₄ pos₅ pos₆ :
  ∀ (I : firstDiff (E := E) x y ≤ firstDiff (E := E) (f x) y), 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

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
⊢ (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
-- 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
simp_rw :
  (if x ∈ s then x else ⋯.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))) =
    Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))
⊢ f x = Ax.some (s := s ∩ cylinder (E := E) x (longestPrefix (E := E) x s))

Tactic:
simp_rw [f, if_neg xs]

Premises used: if_neg
-- 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
⊢ 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]
-- 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))
⊢ (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
-- 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
simp_rw :
  (if y ∈ s then y else ⋯.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))) =
    Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))
⊢ f y = Ay.some (s := s ∩ cylinder (E := E) y (longestPrefix (E := E) y s))

Tactic:
simp_rw [f, if_neg ys]

Premises used: if_neg
-- 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
⊢ 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]
-- 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))
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)
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)
⊢ 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

Premises used: PiNat.firstDiff, PiNat.longestPrefix
-- 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 : 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)
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)
⊢ cylinder (E := E) x (longestPrefix (E := E) x s) = cylinder (E := E) y (longestPrefix (E := E) y s)

Tactic:
rcases H with H | H