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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B :
  Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1 <
    Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
⊢ ∃ y ∈ s, x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)

Tactic:
simpa only [not_disjoint_iff, mem_cylinder_comm] using Nat.find_min A B

Premises used: Set.not_disjoint_iff, Nat.find_min, PiNat.mem_cylinder_comm
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B :
  Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1 <
    Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
neg :
  ∀ (y : (n : ℕ) → E n) (ys : y ∈ s)
    (hy : x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)),
    (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty

Tactic:
obtain ⟨y, ys, hy⟩ : ∃ y : ∀ n : ℕ, E n, y ∈ s ∧ x ∈ cylinder y (Nat.find A - 1) := by
    simpa only [not_disjoint_iff, mem_cylinder_comm] using Nat.find_min A B
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B :
  Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1 <
    Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
y : (n : ℕ) → E n
ys : y ∈ s
hy : x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty

Tactic:
⟨y, ys, ?_⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B :
  Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1 <
    Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
y : (n : ℕ) → E n
ys : y ∈ s
hy : x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
neg : y ∈ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty

Tactic:
refine ⟨y, 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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B :
  Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1 <
    Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
y : (n : ℕ) → E n
ys : y ∈ s
hy : x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
neg :
  ∀
    (hy :
      cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1) =
        cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)),
    cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1) =
      cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
⊢ y ∈ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)

Tactic:
rw [mem_cylinder_iff_eq] at hy ⊢

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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B :
  Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1 <
    Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
y : (n : ℕ) → E n
ys : y ∈ s
hy :
  cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1) =
    cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
neg neg₁ :
  cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1) =
    cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
⊢ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1) =
    cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)

Tactic:
rw [hy]
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B :
  Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1 <
    Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
obtain : ∃ y ∈ s, x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
neg :
  ∀ (y : (n : ℕ) → E n) (ys : y ∈ s)
    (hy : x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)),
    (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty
neg₁ :
  ∀ (y : (n : ℕ) → E n) (ys : y ∈ s)
    (hy : x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)),
    y ∈ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
neg₂ :
  ∀ (y : (n : ℕ) → E n) (ys : y ∈ s)
    (hy :
      cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1) =
        cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)),
    cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1) =
      cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty

Tactic:
classical
  obtain ⟨y, ys, hy⟩ : ∃ y : ∀ n : ℕ, E n, y ∈ s ∧ x ∈ cylinder y (Nat.find A - 1) := by
    simpa only [not_disjoint_iff, mem_cylinder_comm] using Nat.find_min A B
  refine ⟨y, ys, ?_⟩
  rw [mem_cylinder_iff_eq] at hy ⊢
  rw [hy]

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
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : longestPrefix (E := E) x s < n
contrapose! : ∀ (hn : ¬Disjoint s (cylinder (E := E) x n)), n ≤ longestPrefix (E := E) x s
⊢ Disjoint s (cylinder (E := E) x n)

Tactic:
contrapose! hn
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder (E := E) x n)
rcases : ∀ (y : (n : ℕ) → E n) (ys : y ∈ s) (hy : y ∈ cylinder (E := E) x n), n ≤ longestPrefix (E := E) x s
⊢ n ≤ longestPrefix (E := E) x s

Tactic:
rcases not_disjoint_iff_nonempty_inter.1 hn with ⟨y, ys, hy⟩

Premises used: Set.not_disjoint_iff_nonempty_inter, Iff.mp
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder (E := E) x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder (E := E) x n
apply : n ≤ firstDiff (E := E) x y
⊢ n ≤ longestPrefix (E := E) x s

Tactic:
apply le_trans _ (firstDiff_le_longestPrefix hs hx ys)

Premises used: PiNat.firstDiff_le_longestPrefix, le_trans
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder (E := E) x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder (E := E) x n
apply : x ∈ cylinder (E := E) y n
⊢ n ≤ firstDiff (E := E) x y

Tactic:
apply (mem_cylinder_iff_le_firstDiff (ne_of_mem_of_not_mem ys hx).symm _).1

Premises used: Ne.symm, ne_of_mem_of_not_mem, PiNat.mem_cylinder_iff_le_firstDiff, Iff.mp
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder (E := E) x n)
y : (n : ℕ) → E n
ys : y ∈ s
hy rwa rwa₁ rwa₂ rwa₃ : y ∈ cylinder (E := E) x n
⊢ x ∈ cylinder (E := E) y n

Tactic:
rwa [mem_cylinder_comm]

Premises used: PiNat.mem_cylinder_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
inl :
  ∀ (L : longestPrefix (E := E) y s < longestPrefix (E := E) x s),
    longestPrefix (E := E) y s = longestPrefix (E := E) x s
inr :
  ∀ (L : longestPrefix (E := E) y s = longestPrefix (E := E) x s),
    longestPrefix (E := E) y s = longestPrefix (E := E) x s
inr₁ :
  ∀ (L : longestPrefix (E := E) x s < longestPrefix (E := E) y s),
    longestPrefix (E := E) y s = longestPrefix (E := E) x s
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s

Tactic:
rcases lt_trichotomy (longestPrefix y s) (longestPrefix x s) with (L | L | L)

Premises used: PiNat.longestPrefix, lt_trichotomy
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) y s < longestPrefix (E := E) x 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)
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) y s < longestPrefix (E := E) x s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
⊢ Disjoint s (cylinder (E := E) y (longestPrefix (E := E) x s))

Tactic:
have Z := disjoint_cylinder_of_longestPrefix_lt hs ys L
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) 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) x s < firstDiff (E := E) y x

Tactic:
rw [firstDiff_comm] at H

Premises used: PiNat.firstDiff_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) 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))
H₁ : longestPrefix (E := E) x s < firstDiff (E := E) y x
⊢ x ∉ s

Tactic:
rw [firstDiff_comm] at H

Premises used: PiNat.firstDiff_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) 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))
H₁ : longestPrefix (E := E) x s < firstDiff (E := E) y x
xs₁ : x ∉ s
⊢ y ∉ s

Tactic:
rw [firstDiff_comm] at H

Premises used: PiNat.firstDiff_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) 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))
H₁ : longestPrefix (E := E) x s < firstDiff (E := E) y x
xs₁ : x ∉ s
ys₁ : y ∉ s
⊢ longestPrefix (E := E) y s < longestPrefix (E := E) x s

Tactic:
rw [firstDiff_comm] at H

Premises used: PiNat.firstDiff_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) 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))
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
⊢ (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty

Tactic:
rw [firstDiff_comm] at H

Premises used: PiNat.firstDiff_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) 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))
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
⊢ Disjoint s (cylinder (E := E) y (longestPrefix (E := E) x s))

Tactic:
rw [firstDiff_comm] at H

Premises used: PiNat.firstDiff_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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))
⊢ Disjoint s (cylinder (E := E) x (longestPrefix (E := E) x s))

Tactic:
rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H.le] at Z

Premises used: PiNat.cylinder_eq_cylinder_of_le_firstDiff, LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) x (longestPrefix (E := E) x s))
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s

Tactic:
(Ax.not_disjoint Z).elim

Premises used: False.elim, Set.Nonempty.not_disjoint
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) x (longestPrefix (E := E) x s))
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s

Tactic:
exact (Ax.not_disjoint Z).elim

Premises used: False.elim, Set.Nonempty.not_disjoint
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) y s = longestPrefix (E := E) x s
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s

Tactic:
L
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) y s = longestPrefix (E := E) x s
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s

Tactic:
exact L
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
⊢ (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)
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
⊢ (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))
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
⊢ 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 _)
-- Module: Mathlib.Topology.MetricSpace.PiNat
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)
⊢ Disjoint s (cylinder (E := E) y (longestPrefix (E := E) x s).succ)

Tactic:
rw [cylinder_eq_cylinder_of_le_firstDiff _ _ H] at Z

Premises used: PiNat.cylinder_eq_cylinder_of_le_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) y (longestPrefix (E := E) x s).succ)
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s

Tactic:
(A'y.not_disjoint Z).elim

Premises used: False.elim, Set.Nonempty.not_disjoint
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) y (longestPrefix (E := E) x s).succ)
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s

Tactic:
exact (A'y.not_disjoint Z).elim

Premises used: False.elim, Set.Nonempty.not_disjoint