awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
ε : ℝ
εpos : ε > 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 < ε}
have 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 < ε}
Tactic: obtain ⟨n, hn⟩ : ∃ n, (1 / 2 : ℝ) ^ n < ε := exists_pow_lt_of_lt_one εpos (by norm_num)
-- 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)
ε : ℝ
εpos : ε > 0
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 < ε}
have 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 : ℕ)}
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 }
-- 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)
ε : ℝ
ε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 : ℕ)}
⊢ 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 < ε}
have 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 < ε}
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 }
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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)
⊢ Membership.mem (γ := Set (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε} (x, y)
have hxy₁ : ∀ (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
Cleared hypotheses: hxy
-- 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)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ (i : ℕ) (i_1 : i < n), x i = y i
⊢ Membership.mem (γ := Set (((n : ℕ) → E n) × ((n : ℕ) → E n)))
    {p : ((n : ℕ) → E n) × ((n : ℕ) → E n) | dist p.1 p.2 < ε} (x, y)
have apply : dist (x, y).1 (x, y).2 ≤ (1 / 2) ^ n
Tactic: apply lt_of_le_of_lt _ hn
-- 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)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ (i : ℕ) (i_1 : i < n), x i = y i
⊢ dist (x, y).1 (x, y).2 ≤ (1 / 2) ^ n
have rw : ∀ i < n, (x, y).1 i = (x, y).2 i
Tactic: rw [← mem_cylinder_iff_dist_le, mem_cylinder_iff]
-- 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)))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 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})
have 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}
Tactic: simp only [le_iInf_iff, le_principal_iff]
-- 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)
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}
have 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}
Tactic: refine mem_iInf_of_mem ((1 / 2) ^ n : ℝ) ?_
-- 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)
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}
have 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}
Tactic: refine mem_iInf_of_mem (by positivity) ?_
-- 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)
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}
have a : ∀ (a b : (n : ℕ) → E n), dist a b < (1 / 2) ^ n → a n = b n
Tactic: simp only [mem_principal, setOf_subset_setOf, Prod.forall]
-- 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)
⊢ CompleteSpace.{u_1} ((n : ℕ) → E n)
have 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)
Tactic: refine Metric.complete_of_convergent_controlled_sequences (fun n => (1 / 2) ^ n) (by simp) ?_
-- 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)
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)
have refine : ∀ (i : ℕ), Tendsto (fun (i_1 : ℕ) ↦ u i_1 i) atTop (𝓝 (u i i))
Tactic: refine ⟨fun n => u n n, tendsto_pi_nhds.2 fun i => ?_⟩
-- 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)
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))
have refine : EventuallyEq.{0, u_1} (β := E i) atTop (fun (x : ℕ) ↦ u i i) fun (i_1 : ℕ) ↦ u i_1 i
Tactic: refine tendsto_const_nhds.congr' ?_
-- 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)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (n : ℕ) ↦ (1 / 2) ^ n) N
i : ℕ
⊢ EventuallyEq.{0, u_1} (β := E i) atTop (fun (x : ℕ) ↦ u i i) fun (i_1 : ℕ) ↦ u i_1 i
have h : ∀ (n : ℕ) (hn : n ∈ Ici i), u i i = u n i
Tactic: filter_upwards [Filter.Ici_mem_atTop i] 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)
⊢ BoundedSpace.{u_1} ((n : ℕ) → E n)
have rw : ∃ (C : ℝ), ∀ (a b : (n : ℕ) → E n), dist a b ≤ C
Tactic: rw [Metric.boundedSpace_iff]
-- 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)
⊢ ∃ (C : ℝ), ∀ (a b : (n : ℕ) → E n), dist a b ≤ C
have h : ∀ (a b : (n : ℕ) → E n), dist a b ≤ 1
Tactic: use 1
-- 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 : IsClosed[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∉ s
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
have inl : ∀ (hs : IsClosed[Pi.topologicalSpace] ∅) (hx : x ∉ ∅), ∃ (n : ℕ), Disjoint ∅ (cylinder (E := E) x n)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hne)
Cleared hypotheses: s, hs, 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)
hs : IsClosed[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∉ s
inl : ∀ (hs : IsClosed[Pi.topologicalSpace] ∅) (hx : x ∉ ∅), ∃ (n : ℕ), Disjoint ∅ (cylinder (E := E) x n)
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
have inr : ∀ (hne : s.Nonempty), ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hne)
-- 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 : IsClosed[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
have A : 0 < infDist x s
Tactic: have A : 0 < infDist x s := (hs.notMem_iff_infDist_pos hne).1 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)
hs : IsClosed[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
A : 0 < infDist x s
⊢ ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
have inr : ∀ (n : ℕ) (hn : (1 / 2) ^ n < infDist x s), ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
Tactic: obtain ⟨n, hn⟩ : ∃ n, (1 / 2 : ℝ) ^ n < infDist x s := exists_pow_lt_of_lt_one A 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)
hs : IsClosed[Pi.topologicalSpace] 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 (E := E) x n)
have inr : ∀ (y : (n : ℕ) → E n) (ys : y ∈ s) (hy : y ∈ cylinder (E := E) x n), False
Tactic: refine ⟨n, disjoint_left.2 fun y ys hy => ?_⟩
-- 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 : IsClosed[Pi.topologicalSpace] 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 (E := E) x n
⊢ False
have inr : infDist x s < infDist x s
Tactic: apply lt_irrefl (infDist x s)
-- 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 : IsClosed[Pi.topologicalSpace] 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 (E := E) x n
⊢ dist x y ≤ (1 / 2) ^ n
have hy₁ : x ∈ cylinder (E := E) y n
Tactic: rw [mem_cylinder_comm] at hy
Cleared hypotheses: hy
-- 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 : IsClosed[Pi.topologicalSpace] 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 (E := E) x n
⊢ infDist x s < infDist x s
have infDist : dist x y ≤ (1 / 2) ^ n
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
-- 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 : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff (E := E) x y < shortestPrefixDiff (E := E) x s
have A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
Tactic: have A := exists_disjoint_cylinder hs 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)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
⊢ firstDiff (E := E) x y < shortestPrefixDiff (E := E) x s
have rw : firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
Tactic: rw [shortestPrefixDiff, dif_pos A]
-- 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 : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
⊢ firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have B : Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))
Tactic: have B := Nat.find_spec A
-- 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 : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B : Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))
⊢ firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have contrapose! : ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
  ¬Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))
Tactic: contrapose! B
Cleared hypotheses: B
-- 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 : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y
⊢ ¬Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))
have rw : (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)).Nonempty
Tactic: rw [not_disjoint_iff_nonempty_inter]
-- 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 : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y
⊢ (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)).Nonempty
have refine : y ∈ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)
Tactic: refine ⟨y, hy, ?_⟩
-- 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 : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y
⊢ y ∈ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)
have rw : x ∈ cylinder (E := E) y (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)
Tactic: rw [mem_cylinder_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)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
⊢ firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have have : ∀ (B : Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))),
  firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
Tactic: classical
  have B := Nat.find_spec A
  contrapose! B
  rw [not_disjoint_iff_nonempty_inter]
  refine ⟨y, hy, ?_⟩
  rw [mem_cylinder_comm]
  exact cylinder_anti y B (mem_cylinder_firstDiff x 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)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
have have₁ have₂ :
  ∀ (B : Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))),
    firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
⊢ firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have have₃ : ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
  ¬Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))
Tactic: classical
  have B := Nat.find_spec A
  contrapose! B
  rw [not_disjoint_iff_nonempty_inter]
  refine ⟨y, hy, ?_⟩
  rw [mem_cylinder_comm]
  exact cylinder_anti y B (mem_cylinder_firstDiff x 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)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ (n : ℕ), Disjoint s (cylinder (E := E) x n)
have have₁ have₂ :
  ∀ (B : Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))),
    firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have₃ :
  ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
    ¬Disjoint s (cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A))
⊢ firstDiff (E := E) x y < Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A
have have₄ : ∀ (B : Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A ≤ firstDiff (E := E) x y),
  (s ∩ cylinder (E := E) x (Nat.find (p := fun (n : ℕ) ↦ Disjoint s (cylinder (E := E) x n)) A)).Nonempty
Tactic: classical
  have B := Nat.find_spec A
  contrapose! B
  rw [not_disjoint_iff_nonempty_inter]
  refine ⟨y, hy, ?_⟩
  rw [mem_cylinder_comm]
  exact cylinder_anti y B (mem_cylinder_firstDiff x y)