-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem exists_disjoint_cylinder {s : Set (∀ n, E n)} (hs : IsClosed s) {x : ∀ n, E n}
    (hx : x ∉ s) : ∃ n, Disjoint s (cylinder x n)

Proof state:
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
hs : IsClosed ∅
hx : x ∉ ∅
⊢ ∃ n, Disjoint ∅ (cylinder x n)

Tactic:
exact ⟨0, by simp⟩

Result:
no goals

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
⊢ ∃ n, Disjoint s (cylinder x n)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Result:
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
hs : IsClosed ∅
hx : x ∉ ∅
⊢ ∃ n, Disjoint ∅ (cylinder x n)

case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
⊢ ∃ n, Disjoint s (cylinder x n)

Proof state:
case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
A : 0 < infDist x s
⊢ ∃ n, Disjoint s (cylinder x n)

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

Result:
case inr.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed 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 x n)

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed 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 x n
⊢ dist x y ≤ (1 / 2) ^ n

Tactic:
rw [mem_cylinder_comm] at hy

Result:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed 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 y n
⊢ dist x y ≤ (1 / 2) ^ n

Proof state:
case inr.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed 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 x n
⊢ False

Tactic:
apply lt_irrefl (infDist x s)

Result:
case inr.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed 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 x n
⊢ infDist x s < infDist x s

Proof state:
case inr.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed 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 x n)

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

Result:
case inr.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed 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 x n
⊢ False

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed 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 y n
⊢ dist x y ≤ (1 / 2) ^ n

Tactic:
exact mem_cylinder_iff_dist_le.1 hy

Result:
no goals

Proof state:
case inr.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed 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 x n
⊢ infDist x s < 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

Result:
no goals

Proof state:
case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
⊢ ∃ n, Disjoint s (cylinder x n)

Tactic:
have A : 0 < infDist x s := (hs.not_mem_iff_infDist_pos hne).1 hx

Result:
case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
A : 0 < infDist x s
⊢ ∃ n, Disjoint s (cylinder x n)

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
hs : IsClosed ∅
hx : x ∉ ∅
⊢ Disjoint ∅ (cylinder x 0)

Tactic:
simp

Result:
no goals