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)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
mpr :
  ∀ (x : (n : ℕ) → E n) (hx : x ∈ s),
    ∃ (t : Set ((n : ℕ) → E n)),
      Membership.mem (γ := Set (Set ((n : ℕ) → E n)))
          {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n} t ∧
        x ∈ t ∧ t ⊆ s
⊢ IsOpen[Pi.topologicalSpace] s

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

Premises used: Iff.mpr, TopologicalSpace.IsTopologicalBasis.isOpen_iff, PiNat.isTopologicalBasis_cylinders
-- 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)
h : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
mpr :
  ∀ (ε : ℝ) (εpos : ε > 0) (hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s),
    ∃ (t : Set ((n : ℕ) → E n)),
      Membership.mem (γ := Set (Set ((n : ℕ) → E n)))
          {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n} t ∧
        x ∈ t ∧ t ⊆ s
⊢ ∃ (t : Set ((n : ℕ) → E n)),
    Membership.mem (γ := Set (Set ((n : ℕ) → E n)))
        {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n} t ∧
      x ∈ t ∧ t ⊆ s

Tactic:
rcases h x hx with ⟨ε, εpos, hε⟩
-- 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)
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 : ℕ), (1 / 2) ^ n < ε

Tactic:
exists_pow_lt_of_lt_one εpos 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)
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
mpr :
  ∀ (n : ℕ) (hn : (1 / 2) ^ n < ε),
    ∃ (t : Set ((n : ℕ) → E n)),
      Membership.mem (γ := Set (Set ((n : ℕ) → E n)))
          {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n} t ∧
        x ∈ t ∧ t ⊆ s
⊢ ∃ (t : Set ((n : ℕ) → E n)),
    Membership.mem (γ := Set (Set ((n : ℕ) → E n)))
        {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n} t ∧
      x ∈ t ∧ t ⊆ s

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

Premises used: 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)
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 : Set ((n : ℕ) → E n)),
    Membership.mem (γ := Set (Set ((n : ℕ) → E n)))
        {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n} t ∧
      x ∈ t ∧ t ⊆ s

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

Premises used: PiNat.cylinder, PiNat.self_mem_cylinder, And.intro, Exists.intro, rfl
-- 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)
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 < ε
mpr : ∀ (y : (n : ℕ) → E n) (hy : y ∈ cylinder (E := E) x n), dist x y < ε
⊢ ∃ (t : Set ((n : ℕ) → E n)),
    Membership.mem (γ := Set (Set ((n : ℕ) → E n)))
        {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n} t ∧
      x ∈ t ∧ t ⊆ s

Tactic:
refine ⟨cylinder x n, ⟨x, n, rfl⟩, self_mem_cylinder x n, fun y hy => hε y ?_⟩
-- 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)
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 (E := E) x n
mpr : dist y x < ε
⊢ dist x y < ε

Tactic:
rw [PiNat.dist_comm]

Premises used: PiNat.dist_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)
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 (E := E) x n
⊢ dist y x < ε

Tactic:
(mem_cylinder_iff_dist_le.1 hy).trans_lt hn

Premises used: PiNat.mem_cylinder_iff_dist_le, Iff.mp, LE.le.trans_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)
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 (E := E) x n
⊢ dist y x < ε

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

Premises used: PiNat.mem_cylinder_iff_dist_le, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
simp :
  Eq.{u_2 + 1} (α := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})
⊢ Eq.{u_2 + 1} (α := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n))) (uniformity ((n : ℕ) → E n))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})

Tactic:
simp only [Pi.uniformity, h, SetRel.id, comap_principal, preimage_setOf_eq]

Premises used: SetRel.id, Set.preimage_setOf_eq, Filter.comap_principal, Pi.uniformity
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
a :
  LE.le.{u_2} (α := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})
a₁ :
  LE.le.{u_2} (α := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})
    (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})
⊢ Eq.{u_2 + 1} (α := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
a :
  ∀ (i : ℝ) (i_1 : i > 0),
    Membership.mem (γ := Filter (((i : ℕ) → E i) × ((i : ℕ) → E i)))
      (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})
      {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < i}
⊢ LE.le.{u_2} (α := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})

Tactic:
simp only [le_iInf_iff, le_principal_iff]

Premises used: Filter.le_principal_iff, le_iInf_iff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
ε : ℝ
εpos : ε > 0
⊢ 1 / 2 < 1

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
ε : ℝ
εpos : ε > 0
a :
  ∀ (n : ℕ) (hn : (1 / 2) ^ n < ε),
    Membership.mem (γ := Filter (((i : ℕ) → E i) × ((i : ℕ) → E i)))
      (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})
      {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε}
⊢ Membership.mem (γ := Filter (((i : ℕ) → E i) × ((i : ℕ) → E i)))
    (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})
    {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε}

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

Premises used: exists_pow_lt_of_lt_one, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
a :
  ∀ (i : (↑(↑(Finset.range n) : Set ℕ) : Type)),
    Membership.mem (γ := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
      (𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 (↑i : ℕ) = a.2 (↑i : ℕ)})
      {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | p.1 (↑i : ℕ) = p.2 (↑i : ℕ)}
a₁ :
  Subset.{u_2} (α := Set (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⋂ (i : (↑(↑(Finset.range n) : Set ℕ) : Type)),
      {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | p.1 (↑i : ℕ) = p.2 (↑i : ℕ)})
    {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε}
⊢ Membership.mem (γ := Filter (((i : ℕ) → E i) × ((i : ℕ) → E i)))
    (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})
    {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε}

Tactic:
apply
          @mem_iInf_of_iInter _ _ _ _ _ (Finset.range n).finite_toSet fun i =>
            { p : (∀ n : ℕ, E n) × ∀ n : ℕ, E n | p.fst i = p.snd i }

Premises used: Filter.mem_iInf_of_iInter, Finset.range, Finset.finite_toSet
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
⊢ ∀ (i : (↑(↑(Finset.range n) : Set ℕ) : Type)),
    Membership.mem (γ := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
      (𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 (↑i : ℕ) = a.2 (↑i : ℕ)})
      {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | p.1 (↑i : ℕ) = p.2 (↑i : ℕ)}

Tactic:
simp only [mem_principal, setOf_subset_setOf, imp_self, imp_true_iff]

Premises used: imp_true_iff, Filter.mem_principal, imp_self, Set.setOf_subset_setOf
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy :
  Membership.mem (γ := Set (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⋂ (i : (↑(↑(Finset.range n) : Set ℕ) : Type)),
      {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | p.1 (↑i : ℕ) = p.2 (↑i : ℕ)})
    (x, y)
⊢ ∀ (i : ℕ) (i_1 : i < n), x i = y i

Tactic:
simp only [Finset.mem_coe, Finset.mem_range, iInter_coe_set, mem_iInter, mem_setOf_eq]
            at hxy

Premises used: Set.mem_setOf_eq, Finset.mem_range, Set.mem_iInter, Set.iInter_coe_set, Finset.mem_coe
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ (i : ℕ) (i_1 : i < n), x i = y i
apply : dist (x, y).1 (x, y).2 ≤ (1 / 2) ^ n
⊢ Membership.mem (γ := Set (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε} (x, y)

Tactic:
apply lt_of_le_of_lt _ hn

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ (i : ℕ) (i_1 : i < n), x i = y i
rw : ∀ i < n, (x, y).1 i = (x, y).2 i
⊢ dist (x, y).1 (x, y).2 ≤ (1 / 2) ^ n

Tactic:
rw [← mem_cylinder_iff_dist_le, mem_cylinder_iff]

Premises used: PiNat.mem_cylinder_iff_dist_le, PiNat.mem_cylinder_iff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ (i : ℕ) (i_1 : i < n), x i = y i
⊢ ∀ i < n, (x, y).1 i = (x, y).2 i

Tactic:
hxy
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ (i : ℕ) (i_1 : i < n), x i = y i
⊢ ∀ i < n, (x, y).1 i = (x, y).2 i

Tactic:
exact hxy
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
a :
  ∀ (i : ℕ),
    Membership.mem (γ := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
      (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})
      {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i}
⊢ LE.le.{u_2} (α := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})
    (⨅ (i : ℕ), 𝓟 {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 i = a.2 i})

Tactic:
simp only [le_iInf_iff, le_principal_iff]

Premises used: Filter.le_principal_iff, le_iInf_iff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
n : ℕ
⊢ Membership.mem (γ := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})
    {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 n = a.2 n}

Tactic:
mem_iInf_of_mem ((1 / 2) ^ n : ℝ) ?_

Premises used: HDiv.hDiv, Filter.mem_iInf_of_mem, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
n : ℕ
a :
  Membership.mem (γ := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (_ : (1 / 2) ^ n > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < (1 / 2) ^ n})
    {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 n = a.2 n}
⊢ Membership.mem (γ := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε})
    {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 n = a.2 n}

Tactic:
refine mem_iInf_of_mem ((1 / 2) ^ n : ℝ) ?_

Premises used: HDiv.hDiv, Filter.mem_iInf_of_mem, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
n : ℕ
⊢ (1 / 2) ^ n > 0

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
n : ℕ
a :
  Membership.mem (γ := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < (1 / 2) ^ n})
    {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 n = a.2 n}
⊢ Membership.mem (γ := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (⨅ (_ : (1 / 2) ^ n > 0), 𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < (1 / 2) ^ n})
    {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 n = a.2 n}

Tactic:
refine mem_iInf_of_mem (by positivity) ?_

Premises used: Filter.mem_iInf_of_mem
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
n : ℕ
a : ∀ (a b : (n : ℕ) → E n), dist a b < (1 / 2) ^ n → a n = b n
⊢ Membership.mem (γ := Filter (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    (𝓟 {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < (1 / 2) ^ n})
    {a : ((i : ℕ) → E i) × ((i : ℕ) → E i) | a.1 n = a.2 n}

Tactic:
simp only [mem_principal, setOf_subset_setOf, Prod.forall]

Premises used: Filter.mem_principal, Set.setOf_subset_setOf, Prod.forall
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
n : ℕ
x y : (n : ℕ) → E n
hxy : dist x y < (1 / 2) ^ n
⊢ x n = y n

Tactic:
apply_eq_of_dist_lt hxy le_rfl

Premises used: PiNat.apply_eq_of_dist_lt, le_rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E_1 : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E_1 n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E_1 n)
E : ℕ → Type u_2
inst_2 : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := Filter (E n × E n)) (uniformity (E n)) (𝓟 SetRel.id)
this : ∀ (n : ℕ), DiscreteTopology.{u_2} (E n)
n : ℕ
x y : (n : ℕ) → E n
hxy : dist x y < (1 / 2) ^ n
⊢ x n = y n

Tactic:
exact apply_eq_of_dist_lt hxy 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)
⊢ ∀ (n : ℕ), LT.lt (α := ℝ) 0 ((fun (n : ℕ) ↦ (1 / 2) ^ n) n)

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)
refine :
  ∀ (u : ℕ → (n : ℕ) → E n),
    (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (n : ℕ) ↦ (1 / 2) ^ n) N) →
      ∃ (x : (n : ℕ) → E n), Tendsto u atTop (𝓝 x)
⊢ CompleteSpace.{u_1} ((n : ℕ) → E n)

Tactic:
refine Metric.complete_of_convergent_controlled_sequences (fun n => (1 / 2) ^ n) (by simp) ?_

Premises used: Metric.complete_of_convergent_controlled_sequences, HDiv.hDiv, HPow.hPow, 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)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (n : ℕ) ↦ (1 / 2) ^ n) N
⊢ ∃ (x : (n : ℕ) → E n), Tendsto u atTop (𝓝 x)

Tactic:
⟨fun n => u n n, tendsto_pi_nhds.2 fun i => ?_⟩

Premises used: Iff.mpr, tendsto_pi_nhds, 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)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (n : ℕ) ↦ (1 / 2) ^ n) N
refine : ∀ (i : ℕ), Tendsto (fun (i_1 : ℕ) ↦ u i_1 i) atTop (𝓝 (u i i))
⊢ ∃ (x : (n : ℕ) → E n), Tendsto u atTop (𝓝 x)

Tactic:
refine ⟨fun n => u n n, tendsto_pi_nhds.2 fun i => ?_⟩
-- 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 : ℕ
⊢ Tendsto (fun (i_1 : ℕ) ↦ u i_1 i) atTop (𝓝 (u i i))

Tactic:
tendsto_const_nhds.congr' ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- 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 : ℕ
refine : EventuallyEq.{0, u_1} (β := E i) atTop (fun (x : ℕ) ↦ u i i) fun (i_1 : ℕ) ↦ u i_1 i
⊢ Tendsto (fun (i_1 : ℕ) ↦ u i_1 i) atTop (𝓝 (u i i))

Tactic:
refine tendsto_const_nhds.congr' ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'