awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
have have₁ have₂ :
  ∀ (B : Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))),
    firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have₃ :
  ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
    ¬Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))
have₄ :
  ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
    (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)).Nonempty
⊢ firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have have₅ : ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
  y ∈ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)
Tactic: classical
  have B := Nat.find_spec A
  contrapose! B
  rw [not_disjoint_iff_nonempty_inter]
  refine ⟨y, hy, ?_⟩
  rw [mem_cylinder_comm]
  exact cylinder_anti y B (mem_cylinder_firstDiff x y)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
have have₁ have₂ :
  ∀ (B : Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))),
    firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have₃ :
  ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
    ¬Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))
have₄ :
  ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
    (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)).Nonempty
have₅ :
  ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
    y ∈ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)
⊢ firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have have₆ : ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
  x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)
Tactic: classical
  have B := Nat.find_spec A
  contrapose! B
  rw [not_disjoint_iff_nonempty_inter]
  refine ⟨y, hy, ?_⟩
  rw [mem_cylinder_comm]
  exact cylinder_anti y B (mem_cylinder_firstDiff x y)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
x : (n : ℕ) → E n
hx : x ∉ s
⊢ 0 < shortestPrefixDiff (E := E) x s
have rcases : ∀ (y : (n : ℕ) → E n) (hy : y ∈ s), 0 < shortestPrefixDiff (E := E) x s
Tactic: rcases hne with ⟨y, hy⟩
Cleared hypotheses: hne
-- 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
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff (E := E) x y ≤ longestPrefix (E := E) x s
have rw : firstDiff (E := E) x y + 1 ≤ shortestPrefixDiff (E := E) x s
Tactic: rw [longestPrefix, le_tsub_iff_right]
-- 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
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
rw : firstDiff (E := E) x y + 1 ≤ shortestPrefixDiff (E := E) x s
⊢ firstDiff (E := E) x y ≤ longestPrefix (E := E) x s
have rw₁ : 1 ≤ shortestPrefixDiff (E := E) x s
Tactic: rw [longestPrefix, le_tsub_iff_right]
-- 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
x : (n : ℕ) → E n
⊢ (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
have pos : ∀ (hx : x ∈ s), (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
Tactic: by_cases hx : 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
x : (n : ℕ) → E n
pos : ∀ (hx : x ∈ s), (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
⊢ (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
have neg : ∀ (hx : x ∉ s), (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
Tactic: by_cases hx : x ∈ 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
x : (n : ℕ) → E n
hx : x ∉ s
⊢ (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
have A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
Tactic: have A := exists_disjoint_cylinder hs hx
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
⊢ (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
have B : longestPrefix (E := E) x s < shortestPrefixDiff (E := E) x s
Tactic: have B : longestPrefix x s < shortestPrefixDiff x s :=
    Nat.pred_lt (shortestPrefixDiff_pos hs hne hx).ne'
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B : longestPrefix (E := E) x s < shortestPrefixDiff (E := E) x s
⊢ (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
have neg : ∀
  (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),
  (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty
Tactic: rw [longestPrefix, shortestPrefixDiff, dif_pos A] at B ⊢
Cleared hypotheses: B
-- 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
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
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty
have 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
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
-- 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
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
have neg : y ∈ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
Tactic: refine ⟨y, 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
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)
⊢ y ∈ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
have 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)
Tactic: rw [mem_cylinder_iff_eq] at hy ⊢
Cleared hypotheses: hy
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [hy]
-- 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
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
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty
have obtain : ∃ y ∈ s, x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)
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]
-- 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
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)
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty
have 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
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]
-- 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
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
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty
have 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)
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]
-- 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
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)
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A - 1)).Nonempty
have 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)
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]
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : longestPrefix (E := E) x s < n
⊢ Disjoint s (cylinder (E := E) x n)
have contrapose! : ∀ (hn : ¬Disjoint s (cylinder (E := E) x n)), n ≤ longestPrefix (E := E) x s
Tactic: contrapose! hn
Cleared hypotheses: hn
-- 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
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder (E := E) x n)
⊢ n ≤ longestPrefix (E := E) x s
have rcases : ∀ (y : (n : ℕ) → E n) (ys : y ∈ s) (hy : y ∈ cylinder (E := E) x n), n ≤ longestPrefix (E := E) x s
Tactic: rcases not_disjoint_iff_nonempty_inter.1 hn with ⟨y, ys, hy⟩
-- 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
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
⊢ n ≤ longestPrefix (E := E) x s
have apply : n ≤ firstDiff (E := E) x y
Tactic: apply le_trans _ (firstDiff_le_longestPrefix hs hx 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
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
⊢ n ≤ firstDiff (E := E) x y
have apply : x ∈ cylinder (E := E) y n
Tactic: apply (mem_cylinder_iff_le_firstDiff (ne_of_mem_of_not_mem ys hx).symm _).1
-- 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
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
have inl : ∀ (L : 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)
-- 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
inl :
  ∀ (L : longestPrefix (E := E) y s < longestPrefix (E := E) x s),
    longestPrefix (E := E) y s = longestPrefix (E := E) x s
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
have inr : ∀ (L : 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)
-- 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
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
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
have inr₁ : ∀ (L : longestPrefix (E := E) x s < longestPrefix (E := E) y 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)
-- 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) y s < longestPrefix (E := E) x s
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
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
-- 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) y s < longestPrefix (E := E) x s
Ax : (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
⊢ longestPrefix (E := E) y s = longestPrefix (E := E) x s
have Z : Disjoint s (cylinder (E := E) y (longestPrefix (E := E) x s))
Tactic: have Z := disjoint_cylinder_of_longestPrefix_lt hs ys 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) 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 H₁ : longestPrefix (E := E) x s < firstDiff (E := E) y x
Tactic: rw [firstDiff_comm] at H
Cleared hypotheses: H, xs, ys, L, Ax, Z