awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
⊢ dist x z ≤ max (dist x y) (dist y z)
have inr : ∀ (hxz : x ≠ y), dist x y ≤ max (dist x y) (dist y y)
Tactic: rcases eq_or_ne y z with (rfl | hyz)
Cleared hypotheses: z, hxz
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
inr : ∀ (hxz : x ≠ y), dist x y ≤ max (dist x y) (dist y y)
⊢ dist x z ≤ max (dist x y) (dist y z)
have inr₁ : ∀ (hyz : y ≠ z), dist x z ≤ max (dist x y) (dist y z)
Tactic: rcases eq_or_ne y z with (rfl | hyz)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
⊢ x = y
have inl : ∀ (hxy : dist x x = 0), x = x
Tactic: rcases eq_or_ne x y with (rfl | h)
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
inl : ∀ (hxy : dist x x = 0), x = x
⊢ x = y
have inr : ∀ (h : x ≠ y), x = y
Tactic: rcases eq_or_ne x y with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder (E := E) x n ↔ dist y x ≤ (1 / 2) ^ n
have inl : y ∈ cylinder (E := E) y n ↔ dist y y ≤ (1 / 2) ^ n
Tactic: rcases eq_or_ne y x with (rfl | hne)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
inl : y ∈ cylinder (E := E) y n ↔ dist y y ≤ (1 / 2) ^ n
⊢ y ∈ cylinder (E := E) x n ↔ dist y x ≤ (1 / 2) ^ n
have inr : ∀ (hne : y ≠ x), y ∈ cylinder (E := E) x n ↔ dist y x ≤ (1 / 2) ^ n
Tactic: rcases eq_or_ne y x with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ y ∈ cylinder (E := E) x n ↔ dist y x ≤ (1 / 2) ^ n
have inr : (∀ i < n, y i = x i) ↔ n ≤ firstDiff (E := E) y x
Tactic: suffices (∀ i : ℕ, i < n → y i = x i) ↔ n ≤ firstDiff y x by simpa [dist_eq_of_ne hne]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ i < n, y i = x i) ↔ n ≤ firstDiff (E := E) y x
have inr : (∀ i < n, y i = x i) → n ≤ firstDiff (E := E) y x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ (∀ i < n, y i = x i) ↔ n ≤ firstDiff (E := E) y x
have inr₁ : n ≤ firstDiff (E := E) y x → ∀ i < n, y i = x i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
⊢ n ≤ firstDiff (E := E) y x
have inr : ∀ (H : firstDiff (E := E) y x < n), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
⊢ x i = y i
have inl : ∀ (h : dist x x < (1 / 2) ^ n), x i = x i
Tactic: rcases eq_or_ne x y with (rfl | hne)
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ x i = y i
have inr : ∀ (hne : x ≠ y), x i = y i
Tactic: rcases eq_or_ne x y with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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
⊢ x i = y i
have this : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
α : Type u_2
inst : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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 (f x) (f y) ≤ (1 / 2) ^ n
have mp : dist x y ≤ (1 / 2) ^ n
Tactic: apply (H x y).trans
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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 x y ≤ (1 / 2) ^ n
have mp : dist y x ≤ (1 / 2) ^ n
Tactic: rw [PiNat.dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ dist (f x) (f y) ≤ dist x y
have mpr : dist (f x) (f x) ≤ dist x x
Tactic: rcases eq_or_ne x y with (rfl | hne)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ dist (f x) (f y) ≤ dist x y
have mpr₁ : ∀ (hne : x ≠ y), dist (f x) (f y) ≤ dist x y
Tactic: rcases eq_or_ne x y with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ dist (f x) (f y) ≤ dist x y
have mpr : dist (f x) (f y) ≤ (1 / 2) ^ firstDiff (E := E) x y
Tactic: rw [dist_eq_of_ne hne]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ dist (f x) (f y) ≤ (1 / 2) ^ firstDiff (E := E) x y
have mpr : y ∈ cylinder (E := E) x (firstDiff (E := E) x y)
Tactic: apply H x y (firstDiff x y)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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) x y)
have mpr : y ∈ cylinder (E := E) x (firstDiff (E := E) y x)
Tactic: rw [firstDiff_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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)
have rw : IsOpen[Pi.topologicalSpace] ((↑(Finset.range n) : Set ℕ).pi (α := E) fun (i : ℕ) ↦ {x i})
Tactic: rw [PiNat.cylinder_eq_pi]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
⊢ IsTopologicalBasis.{u_1} (α := (n : ℕ) → E n)
    {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n}
have 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
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ IsTopologicalBasis.{u_1} (α := (n : ℕ) → E n)
    {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder (E := E) x n}
have 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
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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 ((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
have 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
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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases Finset.bddAbove F with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
have h_nhds : cylinder (E := E) x (n + 1) ⊆ (↑F : Set ℕ).pi (α := E) U
Tactic: refine ⟨cylinder x (n + 1), ⟨x, n + 1, rfl⟩, self_mem_cylinder _ _, Subset.trans ?_ Uu⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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 ∈ U i
have this : y i = x i
Tactic: have : y i = x i := mem_cylinder_iff.1 hy i ((hn hi).trans_lt (lt_add_one n))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ y i ∈ U i
have h_nhds : x i ∈ U i
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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
⊢ x i ∈ U i
have xU₁ : ∀ i ∈ F, x i ∈ U i
Tactic: simp only [Set.mem_pi, Finset.mem_coe] at xU
Cleared hypotheses: xU
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
inst : (n : ℕ) → TopologicalSpace (E n)
inst_1 : ∀ (n : ℕ), DiscreteTopology.{u_1} (E n)
s : Set ((n : ℕ) → E n)
⊢ IsOpen[Pi.topologicalSpace] s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
have mp : IsOpen[Pi.topologicalSpace] s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ IsOpen[Pi.topologicalSpace] s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
have mpr : (∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s) → IsOpen[Pi.topologicalSpace] s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
have 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
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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
have h's₁ : cylinder (E := E) x n ⊆ s
Tactic: rw [← mem_cylinder_iff_eq.1 h'x] at h's
Cleared hypotheses: h's
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
have 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
Tactic: refine (isTopologicalBasis_cylinders E).isOpen_iff.2 fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases h x hx with ⟨ε, εpos, hε⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2 : ℝ) ^ n < ε := exists_pow_lt_of_lt_one εpos one_half_lt_one
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
have mpr : ∀ (y : (n : ℕ) → E n) (hy : y ∈ cylinder (E := E) x n), dist x y < ε
Tactic: refine ⟨cylinder x n, ⟨x, n, rfl⟩, self_mem_cylinder x n, fun y hy => hε y ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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 x y < ε
have mpr : dist y x < ε
Tactic: rw [PiNat.dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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)
⊢ 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 < ε})
have 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 < ε})
Tactic: simp only [Pi.uniformity, h, SetRel.id, comap_principal, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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)
⊢ 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 < ε})
have 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 < ε})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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 < ε})
⊢ 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 < ε})
have 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})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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)
⊢ 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 < ε})
have 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}
Tactic: simp only [le_iInf_iff, le_principal_iff]