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)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (n : ℕ) ↦ (1 / 2) ^ n) N
i : ℕ
h : ∀ (n : ℕ) (hn : n ∈ Ici i), u i i = u n i
⊢ EventuallyEq.{0, u_1} (β := E i) atTop (fun (x : ℕ) ↦ u i i) fun (i_1 : ℕ) ↦ u i_1 i

Tactic:
filter_upwards [Filter.Ici_mem_atTop i] with n hn

Premises used: Filter.Ici_mem_atTop
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (n : ℕ) ↦ (1 / 2) ^ n) N
i n : ℕ
hn : n ∈ Ici i
⊢ u i i = u n i

Tactic:
apply_eq_of_dist_lt (hu i i n le_rfl hn) le_rfl

Premises used: PiNat.apply_eq_of_dist_lt, le_rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (n : ℕ) ↦ (1 / 2) ^ n) N
i n : ℕ
hn : n ∈ Ici i
⊢ u i i = u n i

Tactic:
exact apply_eq_of_dist_lt (hu i i n le_rfl hn) le_rfl

Premises used: PiNat.apply_eq_of_dist_lt, le_rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
rw : ∃ (C : ℝ), ∀ (a b : (n : ℕ) → E n), dist a b ≤ C
⊢ BoundedSpace.{u_1} ((n : ℕ) → E n)

Tactic:
rw [Metric.boundedSpace_iff]

Premises used: Metric.boundedSpace_iff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
h : ∀ (a b : (n : ℕ) → E n), dist a b ≤ 1
⊢ ∃ (C : ℝ), ∀ (a b : (n : ℕ) → E n), dist a b ≤ C

Tactic:
use 1
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
⊢ ∀ (a b : (n : ℕ) → E n), dist a b ≤ 1

Tactic:
apply PiNat.dist_le_one

Premises used: PiNat.dist_le_one
-- 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
inl : ∀ (hs : IsClosed[Pi.topologicalSpace] ∅) (hx : x ∉ ∅), ∃ (n : ℕ), Disjoint ∅ (cylinder (E := E) x n)
inr : ∀ (hne : s.Nonempty), ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
x : (n : ℕ) → E n
hs : IsClosed[Pi.topologicalSpace] ∅
hx : x ∉ ∅
⊢ Disjoint ∅ (cylinder (E := E) x 0)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
x : (n : ℕ) → E n
hs : IsClosed[Pi.topologicalSpace] ∅
hx : x ∉ ∅
⊢ ∃ (n : ℕ), Disjoint ∅ (cylinder (E := E) x n)

Tactic:
exact ⟨0, by simp⟩
-- 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
hne : s.Nonempty
⊢ 0 < infDist x s

Tactic:
have A : 0 < infDist x s := (hs.notMem_iff_infDist_pos hne).1 hx
-- 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
hne : s.Nonempty
A : 0 < infDist x s
⊢ ∃ (n : ℕ), (1 / 2) ^ n < infDist x s

Tactic:
exists_pow_lt_of_lt_one A one_half_lt_one

Premises used: exists_pow_lt_of_lt_one, one_half_lt_one
-- 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
hne : s.Nonempty
A : 0 < infDist x s
inr : ∀ (n : ℕ) (hn : (1 / 2) ^ n < infDist x s), ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)

Tactic:
obtain ⟨n, hn⟩ : ∃ n, (1 / 2 : ℝ) ^ n < infDist x s := exists_pow_lt_of_lt_one A one_half_lt_one

Premises used: Metric.infDist, exists_pow_lt_of_lt_one, one_half_lt_one, HDiv.hDiv, OfNat.ofNat
-- 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
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)

Tactic:
⟨n, disjoint_left.2 fun y ys hy => ?_⟩

Premises used: Iff.mpr, Set.disjoint_left, 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
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
inr : ∀ (y : (n : ℕ) → E n) (ys : y ∈ s) (hy : y ∈ cylinder (E := E) x n), False
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)

Tactic:
refine ⟨n, disjoint_left.2 fun y ys 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
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder (E := E) x n
inr : infDist x s < infDist x s
⊢ False

Tactic:
apply lt_irrefl (infDist x s)

Premises used: lt_irrefl, Metric.infDist
-- 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
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder (E := E) x n
⊢ infDist x s ≤ dist x y

Tactic:
infDist_le_dist_of_mem ys

Premises used: Metric.infDist_le_dist_of_mem
-- 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
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder (E := E) x n
⊢ x ∈ cylinder (E := E) y n

Tactic:
rw [mem_cylinder_comm] at hy

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)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : x ∈ cylinder (E := E) y n
⊢ dist x y ≤ (1 / 2) ^ n

Tactic:
mem_cylinder_iff_dist_le.1 hy

Premises used: PiNat.mem_cylinder_iff_dist_le, 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
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : x ∈ cylinder (E := E) y n
⊢ dist x y ≤ (1 / 2) ^ n

Tactic:
exact mem_cylinder_iff_dist_le.1 hy

Premises used: PiNat.mem_cylinder_iff_dist_le, 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
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder (E := E) x n
⊢ (1 / 2) ^ n < infDist x s

Tactic:
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
hne : s.Nonempty
A : 0 < Metric.infDist x s
n : ℕ
hn : (1 / 2) ^ n < Metric.infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder (E := E) x n
infDist : dist x y ≤ (1 / 2) ^ n
⊢ Metric.infDist x s < Metric.infDist x s

Tactic:
calc
    infDist x s ≤ dist x y := infDist_le_dist_of_mem ys
    _ ≤ (1 / 2) ^ n := by
      rw [mem_cylinder_comm] at hy
      exact mem_cylinder_iff_dist_le.1 hy
    _ < infDist x s := hn

Premises used: Metric.infDist_le_dist_of_mem, Metric.infDist, HDiv.hDiv, Dist.dist, OfNat.ofNat
-- 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)

Tactic:
have A := exists_disjoint_cylinder hs hx
-- 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
rw : firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
⊢ firstDiff (E := E) x y < shortestPrefixDiff (E := E) x s

Tactic:
rw [shortestPrefixDiff, dif_pos A]

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

Tactic:
have B := Nat.find_spec A
-- 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B : Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))
contrapose! :
  ∀ (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))
⊢ firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A

Tactic:
contrapose! 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
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y
rw : (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)).Nonempty
⊢ ¬Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))

Tactic:
rw [not_disjoint_iff_nonempty_inter]

Premises used: Set.not_disjoint_iff_nonempty_inter
-- 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
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

Tactic:
⟨y, hy, ?_⟩

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

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

Tactic:
rw [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)
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)
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:
cylinder_anti y B (mem_cylinder_firstDiff x y)

Premises used: PiNat.mem_cylinder_firstDiff, 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
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
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:
exact cylinder_anti y B (mem_cylinder_firstDiff x y)

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

Premises used: Set.not_disjoint_iff_nonempty_inter, 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
rcases : ∀ (y : (n : ℕ) → E n) (hy : y ∈ s), 0 < shortestPrefixDiff (E := E) x s
⊢ 0 < shortestPrefixDiff (E := E) x s

Tactic:
rcases hne with ⟨y, 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
x : (n : ℕ) → E n
hx : x ∉ s
y : (n : ℕ) → E n
hy : y ∈ s
⊢ 0 < shortestPrefixDiff (E := E) x s

Tactic:
(firstDiff_lt_shortestPrefixDiff hs hx hy).pos

Premises used: LT.lt.pos, PiNat.firstDiff_lt_shortestPrefixDiff
-- 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
y : (n : ℕ) → E n
hy : y ∈ s
⊢ 0 < shortestPrefixDiff (E := E) x s

Tactic:
exact (firstDiff_lt_shortestPrefixDiff hs hx hy).pos

Premises used: LT.lt.pos, PiNat.firstDiff_lt_shortestPrefixDiff
-- 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
rw : firstDiff (E := E) x y + 1 ≤ shortestPrefixDiff (E := E) x s
rw₁ : 1 ≤ shortestPrefixDiff (E := E) x s
⊢ firstDiff (E := E) x y ≤ longestPrefix (E := E) x s

Tactic:
rw [longestPrefix, le_tsub_iff_right]

Premises used: PiNat.longestPrefix, le_tsub_iff_right
-- 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff (E := E) x y + 1 ≤ shortestPrefixDiff (E := E) x s

Tactic:
firstDiff_lt_shortestPrefixDiff hs hx hy

Premises used: PiNat.firstDiff_lt_shortestPrefixDiff, Nat.lt
-- 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff (E := E) x y + 1 ≤ shortestPrefixDiff (E := E) x s

Tactic:
exact firstDiff_lt_shortestPrefixDiff hs hx hy

Premises used: PiNat.firstDiff_lt_shortestPrefixDiff
-- 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff (E := E) x s

Tactic:
shortestPrefixDiff_pos hs ⟨y, hy⟩ hx

Premises used: Exists.intro, Nat.lt, PiNat.shortestPrefixDiff_pos
-- 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff (E := E) x s

Tactic:
exact shortestPrefixDiff_pos hs ⟨y, hy⟩ hx

Premises used: Exists.intro, PiNat.shortestPrefixDiff_pos
-- 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
pos : ∀ (hx : x ∈ s), (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty
neg : ∀ (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

Tactic:
by_cases hx : x ∈ 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
x : (n : ℕ) → E n
hx : x ∈ s
⊢ (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty

Tactic:
⟨x, hx, self_mem_cylinder _ _⟩

Premises used: Set.Nonempty, PiNat.self_mem_cylinder, 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
⊢ (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty

Tactic:
exact ⟨x, hx, self_mem_cylinder _ _⟩
-- 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
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)

Tactic:
have A := exists_disjoint_cylinder hs hx
-- 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)
⊢ 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'
-- 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 : longestPrefix (E := E) x s < shortestPrefixDiff (E := E) x s
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
⊢ (s ∩ cylinder (E := E) x (longestPrefix (E := E) x s)).Nonempty

Tactic:
rw [longestPrefix, shortestPrefixDiff, dif_pos A] at B ⊢

Premises used: dif_pos, PiNat.shortestPrefixDiff, PiNat.longestPrefix