mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝ : x = y
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝ : ¬x = y
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝ : x = y
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝ : ¬x = y
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
x : X
y : Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) q = glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝) q

pp: case inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
x : X
y val✝ : Y
⊢ Sum.dist (Sum.inr val✝) q = glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝) q

Tactic:
<;>

Goal state after:
case inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
x : X
y : Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) q = glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝) q

case inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
x : X
y val✝ : Y
⊢ Sum.dist (Sum.inr val✝) q = glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝) q
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : x = y
h✝ : x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : x = y
h✝ : ¬x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : ¬x = y
h✝ : x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : ¬x = y
h✝ : ¬x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : x = y
h✝ : x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : x = y
h✝ : ¬x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : ¬x = y
h✝ : x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝¹ : ¬x = y
h✝ : ¬x = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
y : X ⊕ Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) y = Sum.dist y (Sum.inl val✝)

pp: case inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
y : X ⊕ Y
val✝ : Y
⊢ Sum.dist (Sum.inr val✝) y = Sum.dist y (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
y : X ⊕ Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) y = Sum.dist y (Sum.inl val✝)

case inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
y : X ⊕ Y
val✝ : Y
⊢ Sum.dist (Sum.inr val✝) y = Sum.dist y (Sum.inr val✝)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) = Sum.dist (Sum.inl val✝) (Sum.inl val✝¹)

pp: case inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) = Sum.dist (Sum.inr val✝) (Sum.inl val✝¹)

pp: case inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) = Sum.dist (Sum.inl val✝) (Sum.inr val✝¹)

pp: case inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) = Sum.dist (Sum.inr val✝) (Sum.inr val✝¹)

Tactic:
<;>

Goal state after:
case inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) = Sum.dist (Sum.inl val✝) (Sum.inl val✝¹)

case inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) = Sum.dist (Sum.inr val✝) (Sum.inl val✝¹)

case inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) = Sum.dist (Sum.inl val✝) (Sum.inr val✝¹)

case inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) = Sum.dist (Sum.inr val✝) (Sum.inr val✝¹)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg.ha
a b : ℝ
x y z : ↑(Icc a b)
h : ¬↑z - ↑x = 0
hxy : ↑x ≤ ↑y
hyz : ↑y ≤ ↑z
⊢ 0 ≤ ↑y - ↑x

pp: case hb
a b : ℝ
x y z : ↑(Icc a b)
h : ¬↑z - ↑x = 0
hxy : ↑x ≤ ↑y
hyz : ↑y ≤ ↑z
⊢ 0 ≤ ↑z - ↑x

Tactic:
<;>

Goal state after:
case neg.ha
a b : ℝ
x y z : ↑(Icc a b)
h : ¬↑z - ↑x = 0
hxy : ↑x ≤ ↑y
hyz : ↑y ≤ ↑z
⊢ 0 ≤ ↑y - ↑x

case hb
a b : ℝ
x y z : ↑(Icc a b)
h : ¬↑z - ↑x = 0
hxy : ↑x ≤ ↑y
hyz : ↑y ≤ ↑z
⊢ 0 ≤ ↑z - ↑x
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg.h
a b : ℝ
x y z : ↑(Icc a b)
h : ¬↑z - ↑x = 0
hxy : ↑x ≤ ↑y
hyz : ↑y ≤ ↑z
⊢ ↑y - ↑x ≤ ↑z - ↑x

pp: case hb
a b : ℝ
x y z : ↑(Icc a b)
h : ¬↑z - ↑x = 0
hxy : ↑x ≤ ↑y
hyz : ↑y ≤ ↑z
⊢ 0 ≤ ↑z - ↑x

Tactic:
<;>

Goal state after:
case neg.h
a b : ℝ
x y z : ↑(Icc a b)
h : ¬↑z - ↑x = 0
hxy : ↑x ≤ ↑y
hyz : ↑y ≤ ↑z
⊢ ↑y - ↑x ≤ ↑z - ↑x

case hb
a b : ℝ
x y z : ↑(Icc a b)
h : ¬↑z - ↑x = 0
hxy : ↑x ≤ ↑y
hyz : ↑y ≤ ↑z
⊢ 0 ≤ ↑z - ↑x
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case zero
α : Type u_2
x : ℕ → α
⊢ (res x 0).length = 0

pp: case succ
α : Type u_2
x : ℕ → α
n✝ : ℕ
a✝ : (res x n✝).length = n✝
⊢ (res x (n✝ + 1)).length = n✝ + 1

Tactic:
<;>

Goal state after:
case zero
α : Type u_2
x : ℕ → α
⊢ (res x 0).length = 0

case succ
α : Type u_2
x : ℕ → α
n✝ : ℕ
a✝ : (res x n✝).length = n✝
⊢ (res x (n✝ + 1)).length = n✝ + 1
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp
α : Type u_2
x y : ℕ → α
n : ℕ
⊢ res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m

pp: case mpr
α : Type u_2
x y : ℕ → α
n : ℕ
⊢ (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
x y : ℕ → α
n : ℕ
⊢ res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m

case mpr
α : Type u_2
x y : ℕ → α
n : ℕ
⊢ (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mpr.left
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)

pp: case mpr.right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)

Tactic:
<;>

Goal state after:
case mpr.left
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)

case mpr.right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mpr.left
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s

pp: case mpr.right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s

Tactic:
<;>

Goal state after:
case mpr.left
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s

case mpr.right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) (Sum.inl val✝) = 0

pp: case inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝ : Y
⊢ Sum.dist (Sum.inr val✝) (Sum.inr val✝) = 0

Tactic:
<;>

Goal state after:
case inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) (Sum.inl val✝) = 0

case inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝ : Y
⊢ Sum.dist (Sum.inr val✝) (Sum.inr val✝) = 0
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
p : X
h : Sum.dist (Sum.inl p) q = 0
⊢ Sum.inl p = q

pp: case inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
p : Y
h : Sum.dist (Sum.inr p) q = 0
⊢ Sum.inr p = q

Tactic:
<;>

Goal state after:
case inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
p : X
h : Sum.dist (Sum.inl p) q = 0
⊢ Sum.inl p = q

case inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
p : Y
h : Sum.dist (Sum.inr p) q = 0
⊢ Sum.inr p = q
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
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: case a
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)
n : ℕ
⊢ {a | a.1 n = a.2 n} ∈ 𝓟 {p | dist p.1 p.2 < (1 / 2) ^ n}

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

Goal state after:
case a
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)
n : ℕ
⊢ ∀ (a b : (n : ℕ) → E n), dist a b < (1 / 2) ^ n → a n = b n
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case h.x
β : 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)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₀ ∈ A (res x n)

pp: case h.x
β : 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)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₁ ∈ A (res x n)

Tactic:
<;>

Goal state after:
case h.x
β : 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)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₀ ∈ A (res x n)

case h.x
β : 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)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₁ ∈ A (res x n)
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case h.x
β : 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)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₀

pp: case h.x
β : 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)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₁

Tactic:
<;>

Goal state after:
case h.x
β : 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)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₀

case h.x
β : 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)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₁
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (eball x₀ (ε / 2) ∩ D₀))
non0' : (closure (eball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (eball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : ediam (closure (eball x₀ (ε / 2) ∩ D₀)) ≤ ε
perf1' : Perfect (closure (eball x₁ (ε / 2) ∩ D₁))
non1' : (closure (eball x₁ (ε / 2) ∩ D₁)).Nonempty
sub1' : closure (eball x₁ (ε / 2) ∩ D₁) ⊆ D₁
diam1 : ediam (closure (eball x₁ (ε / 2) ∩ D₁)) ≤ ε
⊢ closure (eball x₀ (ε / 2) ∩ D₀) ⊆ D₀

pp: α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (eball x₀ (ε / 2) ∩ D₀))
non0' : (closure (eball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (eball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : ediam (closure (eball x₀ (ε / 2) ∩ D₀)) ≤ ε
perf1' : Perfect (closure (eball x₁ (ε / 2) ∩ D₁))
non1' : (closure (eball x₁ (ε / 2) ∩ D₁)).Nonempty
sub1' : closure (eball x₁ (ε / 2) ∩ D₁) ⊆ D₁
diam1 : ediam (closure (eball x₁ (ε / 2) ∩ D₁)) ≤ ε
⊢ closure (eball x₁ (ε / 2) ∩ D₁) ⊆ D₁

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (eball x₀ (ε / 2) ∩ D₀))
non0' : (closure (eball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (eball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : ediam (closure (eball x₀ (ε / 2) ∩ D₀)) ≤ ε
perf1' : Perfect (closure (eball x₁ (ε / 2) ∩ D₁))
non1' : (closure (eball x₁ (ε / 2) ∩ D₁)).Nonempty
sub1' : closure (eball x₁ (ε / 2) ∩ D₁) ⊆ D₁
diam1 : ediam (closure (eball x₁ (ε / 2) ∩ D₁)) ≤ ε
⊢ closure (eball x₀ (ε / 2) ∩ D₀) ⊆ D₀

α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (eball x₀ (ε / 2) ∩ D₀))
non0' : (closure (eball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (eball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : ediam (closure (eball x₀ (ε / 2) ∩ D₀)) ≤ ε
perf1' : Perfect (closure (eball x₁ (ε / 2) ∩ D₁))
non1' : (closure (eball x₁ (ε / 2) ∩ D₁)).Nonempty
sub1' : closure (eball x₁ (ε / 2) ∩ D₁) ⊆ D₁
diam1 : ediam (closure (eball x₁ (ε / 2) ∩ D₁)) ≤ ε
⊢ closure (eball x₁ (ε / 2) ∩ D₁) ⊆ D₁
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
⊢ CantorScheme.Antitone D

Tactic:
intro l a

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
l : List Bool
a : Bool
⊢ D (a :: l) ⊆ D l