-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem isOpen_iff_dist (s : Set (∀ n, E n)) :
    IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder x n ⊆ s
⊢ (1 / 2) ^ n > 0

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder x n ⊆ s
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Tactic:
exact
  ⟨(1 / 2 : ℝ) ^ n, by simp, fun y hy => h's fun i hi => (apply_eq_of_dist_lt hy hi.le).symm⟩

Result:
no goals

Proof state:
case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ IsOpen s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Tactic:
intro hs x hx

Result:
case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Proof state:
case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Tactic:
obtain ⟨v, ⟨y, n, rfl⟩, h'x, h's⟩ :
    ∃ v ∈ { s | ∃ (x : ∀ n : ℕ, E n) (n : ℕ), s = cylinder x n }, x ∈ v ∧ v ⊆ s :=
  (isTopologicalBasis_cylinders E).exists_subset_of_mem_open hx hs

Result:
case mp.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder y n ⊆ s
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Proof state:
case mpr.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
⊢ ∃ t ∈ {s | ∃ x n, s = cylinder x n}, x ∈ t ∧ t ⊆ s

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2 : ℝ) ^ n < ε := exists_pow_lt_of_lt_one εpos one_half_lt_one

Result:
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
⊢ ∃ t ∈ {s | ∃ x n, s = cylinder x n}, x ∈ t ∧ t ⊆ s

Proof state:
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
y : (n : ℕ) → E n
hy : y ∈ cylinder x n
⊢ dist y x < ε

Tactic:
exact (mem_cylinder_iff_dist_le.1 hy).trans_lt hn

Result:
no goals

Proof state:
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
y : (n : ℕ) → E n
hy : y ∈ cylinder x n
⊢ dist x y < ε

Tactic:
rw [PiNat.dist_comm]

Result:
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
y : (n : ℕ) → E n
hy : y ∈ cylinder x n
⊢ dist y x < ε

Proof state:
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ (∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s) → IsOpen s

Tactic:
intro h

Result:
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
⊢ IsOpen s

Proof state:
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
⊢ IsOpen s

Tactic:
refine (isTopologicalBasis_cylinders E).isOpen_iff.2 fun x hx => ?_

Result:
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
⊢ ∃ t ∈ {s | ∃ x n, s = cylinder x n}, x ∈ t ∧ t ⊆ s

Proof state:
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
⊢ ∃ t ∈ {s | ∃ x n, s = cylinder x n}, x ∈ t ∧ t ⊆ s

Tactic:
refine ⟨cylinder x n, ⟨x, n, rfl⟩, self_mem_cylinder x n, fun y hy => hε y ?_⟩

Result:
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
y : (n : ℕ) → E n
hy : y ∈ cylinder x n
⊢ dist x y < ε

Proof state:
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
⊢ ∃ t ∈ {s | ∃ x n, s = cylinder x n}, x ∈ t ∧ t ⊆ s

Tactic:
rcases h x hx with ⟨ε, εpos, hε⟩

Result:
case mpr.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
⊢ ∃ t ∈ {s | ∃ x n, s = cylinder x n}, x ∈ t ∧ t ⊆ s

Proof state:
case mp.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder y n ⊆ s
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Tactic:
rw [← mem_cylinder_iff_eq.1 h'x] at h's

Result:
case mp.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder x n ⊆ s
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s