awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
h : x ≠ y
⊢ x = y

Tactic:
simp [dist_eq_of_ne h] at hxy

Premises used: PiNat.dist_eq_of_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
inl : y ∈ cylinder (E := E) y n ↔ dist y y ≤ (1 / 2) ^ n
inr : ∀ (hne : y ≠ x), y ∈ cylinder (E := E) x n ↔ dist y x ≤ (1 / 2) ^ n
⊢ y ∈ cylinder (E := E) x n ↔ dist y x ≤ (1 / 2) ^ n

Tactic:
rcases eq_or_ne y x with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder (E := E) y n ↔ dist y y ≤ (1 / 2) ^ n

Tactic:
simp [PiNat.dist_self]

Premises used: PiNat.dist_self
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
this : (∀ i < n, y i = x i) ↔ n ≤ firstDiff (E := E) y x
⊢ y ∈ cylinder (E := E) x n ↔ dist y x ≤ (1 / 2) ^ n

Tactic:
simpa [dist_eq_of_ne hne]

Premises used: PiNat.dist_eq_of_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
inr : (∀ i < n, y i = x i) ↔ n ≤ firstDiff (E := E) y x
⊢ y ∈ cylinder (E := E) x n ↔ dist y x ≤ (1 / 2) ^ n

Tactic:
suffices (∀ i : ℕ, i < n → y i = x i) ↔ n ≤ firstDiff y x by simpa [dist_eq_of_ne hne]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
inr : (∀ i < n, y i = x i) → n ≤ firstDiff (E := E) y x
inr₁ : n ≤ firstDiff (E := E) y x → ∀ i < n, y i = x i
⊢ (∀ i < n, y i = x i) ↔ n ≤ firstDiff (E := E) y x

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
inr : ∀ (H : firstDiff (E := E) y x < n), False
⊢ n ≤ firstDiff (E := E) y x

Tactic:
by_contra! H
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
H : firstDiff (E := E) y x < n
⊢ False

Tactic:
apply_firstDiff_ne hne (hy _ H)

Premises used: PiNat.apply_firstDiff_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
H : firstDiff (E := E) y x < n
⊢ False

Tactic:
exact apply_firstDiff_ne hne (hy _ H)

Premises used: PiNat.apply_firstDiff_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
h : n ≤ firstDiff (E := E) y x
i : ℕ
hi : i < n
⊢ y i = x i

Tactic:
apply_eq_of_lt_firstDiff (hi.trans_le h)

Premises used: LT.lt.trans_le, PiNat.apply_eq_of_lt_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
h : n ≤ firstDiff (E := E) y x
i : ℕ
hi : i < n
⊢ y i = x i

Tactic:
exact apply_eq_of_lt_firstDiff (hi.trans_le h)

Premises used: LT.lt.trans_le, PiNat.apply_eq_of_lt_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
inl : ∀ (h : dist x x < (1 / 2) ^ n), x i = x i
inr : ∀ (hne : x ≠ y), x i = y i
⊢ x i = y i

Tactic:
rcases eq_or_ne x y with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n i : ℕ
hi : i ≤ n
h : dist x x < (1 / 2) ^ n
⊢ x i = x i

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
⊢ n < firstDiff (E := E) x y

Tactic:
simpa [dist_eq_of_ne hne, inv_lt_inv₀, pow_lt_pow_iff_right₀, one_lt_two] using h

Premises used: pow_lt_pow_iff_right₀, PiNat.dist_eq_of_ne, one_lt_two, inv_lt_inv₀
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
⊢ n < firstDiff (E := E) x y

Tactic:
have : n < firstDiff x y := by
    simpa [dist_eq_of_ne hne, inv_lt_inv₀, pow_lt_pow_iff_right₀, one_lt_two] using h
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
this : n < firstDiff (E := E) x y
⊢ x i = y i

Tactic:
apply_eq_of_lt_firstDiff (hi.trans_lt this)

Premises used: PiNat.apply_eq_of_lt_firstDiff, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
this : n < firstDiff (E := E) x y
⊢ x i = y i

Tactic:
exact apply_eq_of_lt_firstDiff (hi.trans_lt this)

Premises used: PiNat.apply_eq_of_lt_firstDiff, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
mp :
  (∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) →
    ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n
mpr :
  (∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n) →
    ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
⊢ (∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) ↔
    ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder (E := E) x n
mp : dist x y ≤ (1 / 2) ^ n
⊢ dist (f x) (f y) ≤ (1 / 2) ^ n

Tactic:
apply (H x y).trans

Premises used: LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder (E := E) x n
mp : dist y x ≤ (1 / 2) ^ n
⊢ dist x y ≤ (1 / 2) ^ n

Tactic:
rw [PiNat.dist_comm]

Premises used: PiNat.dist_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder (E := E) x n
⊢ dist y x ≤ (1 / 2) ^ n

Tactic:
mem_cylinder_iff_dist_le.1 hxy

Premises used: PiNat.mem_cylinder_iff_dist_le, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y
x y : (n : ℕ) → E n
n : ℕ
hxy : y ∈ cylinder (E := E) x n
⊢ dist y x ≤ (1 / 2) ^ n

Tactic:
exact mem_cylinder_iff_dist_le.1 hxy

Premises used: PiNat.mem_cylinder_iff_dist_le, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
mpr : dist (f x) (f x) ≤ dist x x
mpr₁ : ∀ (hne : x ≠ y), dist (f x) (f y) ≤ dist x y
⊢ dist (f x) (f y) ≤ dist x y

Tactic:
rcases eq_or_ne x y with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x : (n : ℕ) → E n
⊢ dist (f x) (f x) ≤ dist x x

Tactic:
simp [PiNat.dist_nonneg]

Premises used: PiNat.dist_nonneg
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
mpr : dist (f x) (f y) ≤ (1 / 2) ^ firstDiff (E := E) x y
⊢ dist (f x) (f y) ≤ dist x y

Tactic:
rw [dist_eq_of_ne hne]

Premises used: PiNat.dist_eq_of_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
mpr : y ∈ cylinder (E := E) x (firstDiff (E := E) x y)
⊢ dist (f x) (f y) ≤ (1 / 2) ^ firstDiff (E := E) x y

Tactic:
apply H x y (firstDiff x y)

Premises used: PiNat.firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
mpr : y ∈ cylinder (E := E) x (firstDiff (E := E) y x)
⊢ y ∈ cylinder (E := E) x (firstDiff (E := E) x y)

Tactic:
rw [firstDiff_comm]

Premises used: PiNat.firstDiff_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder (E := E) x (firstDiff (E := E) y x)

Tactic:
mem_cylinder_firstDiff _ _

Premises used: PiNat.mem_cylinder_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder (E := E) x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder (E := E) x (firstDiff (E := E) y x)

Tactic:
exact mem_cylinder_firstDiff _ _

Premises used: PiNat.mem_cylinder_firstDiff
-- 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
n : ℕ
rw : IsOpen[Pi.topologicalSpace] ((↑(Finset.range n) : Set ℕ).pi (α := E) fun (i : ℕ) ↦ {x i})
⊢ IsOpen[Pi.topologicalSpace] (cylinder (E := E) x n)

Tactic:
rw [PiNat.cylinder_eq_pi]

Premises used: PiNat.cylinder_eq_pi
-- 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
n : ℕ
⊢ IsOpen[Pi.topologicalSpace] ((↑(Finset.range n) : Set ℕ).pi (α := E) fun (i : ℕ) ↦ {x i})

Tactic:
isOpen_set_pi (Finset.range n).finite_toSet fun a _ => isOpen_discrete _

Premises used: Finset.range, isOpen_set_pi, isOpen_discrete, Finset.finite_toSet, Singleton.singleton
-- 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
n : ℕ
⊢ IsOpen[Pi.topologicalSpace] ((↑(Finset.range n) : Set ℕ).pi (α := E) fun (i : ℕ) ↦ {x i})

Tactic:
exact isOpen_set_pi (Finset.range n).finite_toSet fun a _ => isOpen_discrete _

Premises used: Finset.range, isOpen_set_pi, isOpen_discrete, Finset.finite_toSet
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
h_open :
  ∀ (u : 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} u →
      IsOpen[Pi.topologicalSpace] u
h_nhds :
  ∀ (a : (n : ℕ) → E n) (u : Set ((n : ℕ) → E n)),
    a ∈ u →
      IsOpen[Pi.topologicalSpace] u →
        ∃ (v : 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} v ∧
            a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u_1} (α := (n : ℕ) → E n)
    {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n}

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- 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
n : ℕ
⊢ IsOpen[Pi.topologicalSpace] (cylinder (E := E) x n)

Tactic:
apply isOpen_cylinder

Premises used: PiNat.isOpen_cylinder
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
⊢ ∃ (v : Set ((i : ℕ) → E i)),
    Membership.mem (γ := Set (Set ((i : ℕ) → E i)))
        {S : Set ((i : ℕ) → E i) |
          ∃ (U : (i : ℕ) → Set (E i)) (F : Finset ℕ),
            (∀ i ∈ F, Membership.mem (γ := Set (Set (E i))) {s : Set (E i) | IsOpen[inst i] s} (U i)) ∧
              S = (↑F : Set ℕ).pi (α := E) U}
        v ∧
      x ∈ v ∧ v ⊆ u

Tactic:
(isTopologicalBasis_pi fun n : ℕ => isTopologicalBasis_opens).exists_subset_of_mem_open hx
        u_open

Premises used: Set.Mem, setOf, TopologicalSpace.isTopologicalBasis_opens, isTopologicalBasis_pi, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
h_nhds :
  ∀ (U : (i : ℕ) → Set (E i)) (F : Finset ℕ) (xU : x ∈ (↑F : Set ℕ).pi (α := E) U)
    (Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u),
    ∃ (v : 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} v ∧
        x ∈ v ∧ v ⊆ u
⊢ ∃ (v : 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} v ∧
      x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, ⟨U, F, -, rfl⟩, xU, Uu⟩ :
        ∃ v ∈ { S : Set (∀ i : ℕ, E i) | ∃ (U : ∀ i : ℕ, Set (E i)) (F : Finset ℕ),
          (∀ i : ℕ, i ∈ F → U i ∈ { s : Set (E i) | IsOpen s }) ∧ S = (F : Set ℕ).pi U },
        x ∈ v ∧ v ⊆ u :=
      (isTopologicalBasis_pi fun n : ℕ => isTopologicalBasis_opens).exists_subset_of_mem_open hx
        u_open

Premises used: Finset, TopologicalSpace.isTopologicalBasis_opens, Nat, isTopologicalBasis_pi, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open, Set
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F : Set ℕ).pi (α := E) U
Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u
h_nhds :
  ∀ (n : ℕ) (hn : n ∈ upperBounds (↑F : Set ℕ)),
    ∃ (v : 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} v ∧
        x ∈ v ∧ v ⊆ u
⊢ ∃ (v : 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} v ∧
      x ∈ v ∧ v ⊆ u

Tactic:
rcases Finset.bddAbove F with ⟨n, hn⟩

Premises used: Finset.bddAbove
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F : Set ℕ).pi (α := E) U
Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u
n : ℕ
hn : n ∈ upperBounds (↑F : Set ℕ)
⊢ ∃ (v : 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} v ∧
      x ∈ v ∧ v ⊆ u

Tactic:
⟨cylinder x (n + 1), ⟨x, n + 1, rfl⟩, self_mem_cylinder _ _, Subset.trans ?_ Uu⟩

Premises used: Set.Subset.trans, PiNat.cylinder, HAdd.hAdd, PiNat.self_mem_cylinder, And.intro, Exists.intro, OfNat.ofNat, 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F : Set ℕ).pi (α := E) U
Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u
n : ℕ
hn : n ∈ upperBounds (↑F : Set ℕ)
h_nhds : cylinder (E := E) x (n + 1) ⊆ (↑F : Set ℕ).pi (α := E) U
⊢ ∃ (v : 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} v ∧
      x ∈ v ∧ v ⊆ u

Tactic:
refine ⟨cylinder x (n + 1), ⟨x, n + 1, rfl⟩, self_mem_cylinder _ _, Subset.trans ?_ Uu⟩
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F : Set ℕ).pi (α := E) U
Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u
n : ℕ
hn : n ∈ upperBounds (↑F : Set ℕ)
y : (n : ℕ) → E n
hy : y ∈ cylinder (E := E) x (n + 1)
this : ∀ i ∈ F, y i ∈ U i
⊢ y ∈ (↑F : Set ℕ).pi (α := E) U

Tactic:
simpa
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F : Set ℕ).pi (α := E) U
Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u
n : ℕ
hn : n ∈ upperBounds (↑F : Set ℕ)
y : (n : ℕ) → E n
hy : y ∈ cylinder (E := E) x (n + 1)
i : ℕ
hi : i ∈ F
⊢ y i = x i

Tactic:
have : y i = x i := mem_cylinder_iff.1 hy i ((hn hi).trans_lt (lt_add_one n))
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F : Set ℕ).pi (α := E) U
Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u
n : ℕ
hn : n ∈ upperBounds (↑F : Set ℕ)
y : (n : ℕ) → E n
hy : y ∈ cylinder (E := E) x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
h_nhds : x i ∈ U i
⊢ y i ∈ U i

Tactic:
rw [this]
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F : Set ℕ).pi (α := E) U
Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u
n : ℕ
hn : n ∈ upperBounds (↑F : Set ℕ)
y : (n : ℕ) → E n
hy : y ∈ cylinder (E := E) x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
⊢ ∀ i ∈ F, x i ∈ U i

Tactic:
simp only [Set.mem_pi, Finset.mem_coe] at xU

Premises used: Set.mem_pi, Finset.mem_coe
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u
n : ℕ
hn : n ∈ upperBounds (↑F : Set ℕ)
y : (n : ℕ) → E n
hy : y ∈ cylinder (E := E) x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
xU : ∀ i ∈ F, x i ∈ U i
⊢ x i ∈ U i

Tactic:
xU i hi
-- 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
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
Uu : (↑F : Set ℕ).pi (α := E) U ⊆ u
n : ℕ
hn : n ∈ upperBounds (↑F : Set ℕ)
y : (n : ℕ) → E n
hy : y ∈ cylinder (E := E) x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
xU : ∀ i ∈ F, x i ∈ U i
⊢ x i ∈ U i

Tactic:
exact xU i hi
-- 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)
mp : IsOpen[Pi.topologicalSpace] s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
mpr : (∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s) → IsOpen[Pi.topologicalSpace] s
⊢ IsOpen[Pi.topologicalSpace] s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Tactic:
constructor
-- 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 : IsOpen[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∈ s
⊢ ∃ (v : 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} v ∧
      x ∈ v ∧ v ⊆ s

Tactic:
(isTopologicalBasis_cylinders E).exists_subset_of_mem_open hx hs

Premises used: PiNat.isTopologicalBasis_cylinders, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 : IsOpen[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∈ s
mp :
  ∀ (y : (n : ℕ) → E n) (n : ℕ) (h'x : x ∈ cylinder (E := E) y n) (h's : cylinder (E := E) y n ⊆ s),
    ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ 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

Premises used: PiNat.isTopologicalBasis_cylinders, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 : IsOpen[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder (E := E) y n
h's : cylinder (E := E) y n ⊆ s
⊢ cylinder (E := E) x n ⊆ s

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

Premises used: PiNat.mem_cylinder_iff_eq, 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 : IsOpen[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder (E := E) y n
h's : cylinder (E := E) x n ⊆ s
⊢ (1 / 2) ^ n > 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)
s : Set ((n : ℕ) → E n)
hs : IsOpen[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder (E := E) y n
h's : cylinder (E := E) 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⟩
-- 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
⊢ IsOpen[Pi.topologicalSpace] s

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

Premises used: Iff.mpr, TopologicalSpace.IsTopologicalBasis.isOpen_iff, PiNat.isTopologicalBasis_cylinders