mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mpr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist ⟨i, x⟩ y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist x y < ε

Tactic:
]

Goal state after:
case mpr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist ⟨i, x⟩ y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist x y < ε
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
⊢ ∃ t, (∀ y ∈ t, dist ((inducedMap A).snd y) ((inducedMap A).snd x) < ε) ∧ IsOpen[instTopologicalSpaceSubtype] t ∧ x ∈ t

Tactic:
]

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
⊢ ∃ t, (∀ y ∈ t, dist ((inducedMap A).snd y) ((inducedMap A).snd x) < ε) ∧ IsOpen[instTopologicalSpaceSubtype] t ∧ x ∈ t
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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).pi U
Uu : (↑F).pi U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
⊢ x i ∈ U i

Tactic:
]

Goal state after:
case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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).pi U
Uu : (↑F).pi U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
⊢ x i ∈ U i
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s)ᶜ
n : ℕ
this : 0 < infDist (↑(u n)) (↑s)ᶜ
⊢ 1 ≤ C * infDist (↑(u n)) (↑s)ᶜ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s)ᶜ
n : ℕ
this : 0 < infDist (↑(u n)) (↑s)ᶜ
⊢ 1 ≤ C * infDist (↑(u n)) (↑s)ᶜ
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case refine_1
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ dist ((inducedMap A).snd y) ((inducedMap A).snd x) < ε

Tactic:
]

Goal state after:
case refine_1
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ dist ((inducedMap A).snd y) ((inducedMap A).snd x) < ε
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = 0
⊢ 0 < 1

Tactic:
]

Goal state after:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = 0
⊢ 0 < 1
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd y ∈ A (res (↑y) n)

Tactic:
]

Goal state after:
case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd y ∈ A (res (↑y) n)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 y n
h's : cylinder x n ⊆ s
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Tactic:
]

Goal state after:
case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 y n
h's : cylinder x n ⊆ s
⊢ ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ PolishSpace α

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ PolishSpace α
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
⊢ ∀ (x : ℕ → β), x ∈ (inducedMap A).fst

Tactic:
]

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
⊢ ∀ (x : ℕ → β), x ∈ (inducedMap A).fst
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen[instTopologicalSpaceSubtype] (Sum.inl ⁻¹' ⇑f ⁻¹' s) ∧
    IsOpen[instTopologicalSpaceSubtype] (Sum.inr ⁻¹' ⇑f ⁻¹' s)

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen[instTopologicalSpaceSubtype] (Sum.inl ⁻¹' ⇑f ⁻¹' s) ∧
    IsOpen[instTopologicalSpaceSubtype] (Sum.inr ⁻¹' ⇑f ⁻¹' s)
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
]

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
p q : Z
⊢ |dist p q - dist p q| ≤ 2 * 0

Tactic:
]

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
p q : Z
⊢ |dist p q - dist p q| ≤ 2 * 0
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε

Tactic:
]

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ i < n, x i = y i
⊢ ∀ i < n, (x, y).1 i = (x, y).2 i

Tactic:
]

Goal state after:
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ i < n, x i = y i
⊢ ∀ i < n, (x, y).1 i = (x, y).2 i
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ ε ≠ 0 ∧ 2 ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ ε ≠ 0 ∧ 2 ≠ ∞
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ eball x (ε / 2) ∩ C ⊆ C

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ eball x (ε / 2) ∩ C ⊆ C
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ediam (eball x (ε / 2) ∩ C) ≤ ε

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ediam (eball x (ε / 2) ∩ C) ≤ ε
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case e'_4
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ε = ε

pp: case e'_4.ha₀
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ 2 ≠ 0

pp: case e'_4.ha
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ 2 ≠ ∞

Tactic:
]

Goal state after:
case e'_4.ha₀
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ 2 ≠ 0

case e'_4.ha
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ 2 ≠ ∞
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∃ C, ∀ (a b : (n : ℕ) → E n), dist a b ≤ C

Tactic:
]

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∃ C, ∀ (a b : (n : ℕ) → E n), dist a b ≤ C
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ ∀ (i : ℕ), y ∈ A (res x i)

Tactic:
]

Goal state after:
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ ∀ (i : ℕ), y ∈ A (res x i)
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → u b ∈ A (x n :: res x n)

Tactic:
]

Goal state after:
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → u b ∈ A (x n :: res x n)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 : x ∈ cylinder y n
⊢ dist x y ≤ (1 / 2) ^ n

Tactic:
]

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 : x ∈ cylinder y n
⊢ dist x y ≤ (1 / 2) ^ n
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ m.succ
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn xm (fun {k} ↦ f k) x.snd) (leRecOn ym (fun {k} ↦ f k) y.snd)

Tactic:
]

Goal state after:
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ m.succ
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn xm (fun {k} ↦ f k) x.snd) (leRecOn ym (fun {k} ↦ f k) y.snd)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 x n)
⊢ firstDiff x y < Nat.find A

Tactic:
]

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 x n)
⊢ firstDiff x y < Nat.find A
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 x n)
B : Nat.find A ≤ firstDiff x y
⊢ (s ∩ cylinder x (Nat.find A)).Nonempty

Tactic:
]

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 x n)
B : Nat.find A ≤ firstDiff x y
⊢ (s ∩ cylinder x (Nat.find A)).Nonempty
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 x n)
B : Nat.find A ≤ firstDiff x y
⊢ x ∈ cylinder y (Nat.find A)

Tactic:
]

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (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 x n)
B : Nat.find A ≤ firstDiff x y
⊢ x ∈ cylinder y (Nat.find A)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
⊢ dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hx (fun {k} ↦ f k) x.snd) =
    dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hx (fun {k} ↦ f k) x.snd)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y + 1 ≤ shortestPrefixDiff x s

pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s

Tactic:
]

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y + 1 ≤ shortestPrefixDiff x s

E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s

Tactic:
exact shortestPrefixDiff_pos hs ⟨y, hy⟩ hx

Goal state after:
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max x.fst y.fst) z.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
hz : z.fst ≤ m
⊢ dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd) +
      dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hz (fun {k} ↦ f k) z.snd) =
    dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd) +
      dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hz (fun {k} ↦ f k) z.snd)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ dist ⟨n, x⟩.snd ⟨n, y⟩.snd = dist x y

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case neg
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
⊢ (s ∩ cylinder x (Nat.find A - 1)).Nonempty

Tactic:
]

Goal state after:
case neg
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
⊢ (s ∩ cylinder x (Nat.find A - 1)).Nonempty