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

Goal state before:
pp: case mpr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s) →
    (∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s

Tactic:
rintro ⟨ε, ε0, H⟩

Goal state after:
case mpr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε✝ : ℝ
hε : 0 < ε✝
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε✝ a b < ε → (a, b) ∈ s
⊢ (∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
    ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

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

pp: case inr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y : X
h : x ≠ y
⊢ (if x = y then 0 else 1) = if y = x then 0 else 1

Tactic:
·

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y : X
h : x = y
⊢ (if x = y then 0 else 1) = if y = x then 0 else 1
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

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

Tactic:
·

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y : X
h : x ≠ y
⊢ (if x = y then 0 else 1) = if y = x then 0 else 1
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder x n ⊆ cylinder y n

Tactic:
·

Goal state after:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder x n ⊆ cylinder y n
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ cylinder y n = cylinder x n → y ∈ cylinder x n

Tactic:
·

Goal state after:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ cylinder y n = cylinder x n → y ∈ cylinder x n
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
⊢ PseudoMetricSpace.toUniformSpace.toTopologicalSpace = inst✝¹

pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
⊢ CompleteSpace X

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
⊢ PseudoMetricSpace.toUniformSpace.toTopologicalSpace = inst✝¹
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) → ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

pp: case mpr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (X ⊕ Y)

Tactic:
·

Goal state after:
case mp
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) → ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i → i ≤ firstDiff x y

pp: case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ i ≤ firstDiff x y → x ∈ cylinder y i

Tactic:
·

Goal state after:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i → i ≤ firstDiff x y
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ i ≤ firstDiff x y → x ∈ cylinder y i

Tactic:
·

Goal state after:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ i ≤ firstDiff x y → x ∈ cylinder y i
Module: Mathlib.Topology.UnitInterval

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

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

Tactic:
·

Goal state after:
case pos
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ↑z - ↑x = 0
⊢ 0 ≤ (↑y - ↑x) / (↑z - ↑x)
Module: Mathlib.Topology.UnitInterval

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

Tactic:
·

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

Goal state before:
pp: case mp
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1) → ∀ i < n, y i = x i

pp: case mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∀ i < n, y i = x i) → ∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1

Tactic:
·

Goal state after:
case mp
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1) → ∀ i < n, y i = x i
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp.inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : X
h : Sum.dist (Sum.inl a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inl b) ∈ s

pp: case mp.inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : X
b : Y
h : Sum.dist (Sum.inl a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inr b) ∈ s

pp: case mp.inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : Y
b : X
h : Sum.dist (Sum.inr a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inl b) ∈ s

pp: case mp.inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
·

Goal state after:
case mp.inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : X
h : Sum.dist (Sum.inl a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inl b) ∈ s
Module: Mathlib.Topology.UnitInterval

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

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

Tactic:
·

Goal state after:
case pos
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ↑z - ↑x = 0
⊢ (↑y - ↑x) / (↑z - ↑x) ≤ 1
Module: Mathlib.Topology.UnitInterval

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

Tactic:
·

Goal state after:
case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ (↑y - ↑x) / (↑z - ↑x) ≤ 1
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
⊢ CompleteSpace X

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
⊢ CompleteSpace X
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∀ i < n, y i = x i) → ∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1

Tactic:
·

Goal state after:
case mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∀ i < n, y i = x i) → ∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr.inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
h'i : i < n
⊢ y i = update x n (y n) i

pp: case mpr.inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
i : ℕ
H : ∀ i_1 < i, y i_1 = x i_1
hi : i < i + 1
⊢ y i = update x i (y i) i

Tactic:
·

Goal state after:
case mpr.inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
h'i : i < n
⊢ y i = update x n (y n) i
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case pos
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ↑z - ↑x = 0
⊢ ↑y = (1 - (↑y - ↑x) / (↑z - ↑x)) * ↑x + (↑y - ↑x) / (↑z - ↑x) * ↑z

pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ ↑y = (1 - (↑y - ↑x) / (↑z - ↑x)) * ↑x + (↑y - ↑x) / (↑z - ↑x) * ↑z

Tactic:
·

Goal state after:
case pos
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ↑z - ↑x = 0
⊢ ↑y = (1 - (↑y - ↑x) / (↑z - ↑x)) * ↑x + (↑y - ↑x) / (↑z - ↑x) * ↑z
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr.inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
i : ℕ
H : ∀ i_1 < i, y i_1 = x i_1
hi : i < i + 1
⊢ y i = update x i (y i) i

Tactic:
·

Goal state after:
case mpr.inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
i : ℕ
H : ∀ i_1 < i, y i_1 = x i_1
hi : i < i + 1
⊢ y i = update x i (y i) i
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp.inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : X
b : Y
h : Sum.dist (Sum.inl a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inr b) ∈ s

pp: case mp.inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : Y
b : X
h : Sum.dist (Sum.inr a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inl b) ∈ s

pp: case mp.inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
·

Goal state after:
case mp.inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : X
b : Y
h : Sum.dist (Sum.inl a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inr b) ∈ s
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ IsCompletelyMetrizableSpace X

Tactic:
classical
  let m : MetricSpace X :=
    { dist x y := if x = y then 0 else 1
      dist_self x := by simp
      dist_comm x y := by
        obtain h | h := eq_or_ne x y
        · simp [h]
        · simp [h, h.symm]
      dist_triangle x y z := by
        by_cases x = y <;> by_cases x = z <;> by_cases y = z <;> simp_all
      eq_of_dist_eq_zero := by simp }
  refine ⟨m, ?_, ?_⟩
  · rw [DiscreteTopology.eq_bot (α := X)]
    refine eq_bot_of_singletons_open fun x ↦ ?_
    convert! @Metric.isOpen_ball _ _ x 1
    refine subset_antisymm (singleton_subset_iff.2 (Metric.mem_ball_self (by simp)))
      fun y hy ↦ ?_
    simp only [Metric.mem_ball, mem_singleton_iff] at *
    by_contra
    change (if y = x then 0 else 1) < 1 at hy
    simp_all
  · refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
    rw [Metric.cauchySeq_iff'] at hu
    obtain ⟨N, hN⟩ := hu 1 (by simp)
    refine ⟨u N, @tendsto_atTop_of_eventually_const X UniformSpace.toTopologicalSpace (u N) _ _ _ N
      fun n hn ↦ ?_⟩
    specialize hN n hn
    by_contra
    change (if u n = u N then 0 else 1) < 1 at hN
    simp_all

Goal state after:
Module: Mathlib.Topology.UnitInterval

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

Tactic:
·

Goal state after:
case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ ↑y = (1 - (↑y - ↑x) / (↑z - ↑x)) * ↑x + (↑y - ↑x) / (↑z - ↑x) * ↑z
Module: Mathlib.Topology.MetricSpace.PiNat

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

pp: case mpr
α : Type u_2
x y : ℕ → α
n : ℕ
h : ∀ ⦃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 : ℕ
h : res x n = res y n
⊢ ∀ ⦃m : ℕ⦄, m < n → x m = y m
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp.inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : Y
b : X
h : Sum.dist (Sum.inr a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inl b) ∈ s

pp: case mp.inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
·

Goal state after:
case mp.inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : Y
b : X
h : Sum.dist (Sum.inr a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inl b) ∈ s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp.inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
·

Goal state after:
case mp.inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mpr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (X ⊕ Y)

Tactic:
·

Goal state after:
case mpr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (X ⊕ Y)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mpr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (X ⊕ Y)

Tactic:
rintro ⟨ε, ε0, H⟩

Goal state after:
case mpr
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 ∈ 𝓤 (X ⊕ Y)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.succ.inl
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m < n
⊢ x m = y m

pp: case mp.succ.inr
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m = n
⊢ x m = y m

Tactic:
·

Goal state after:
case mp.succ.inl
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m < n
⊢ x m = y m
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
·

Goal state after:
case mpr
α : Type u_2
x y : ℕ → α
n : ℕ
h : ∀ ⦃m : ℕ⦄, m < n → x m = y m
⊢ res x n = res y n
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
x✝ : s.CompleteCopy
⊢ dist x✝ x✝ = 0

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
x✝¹ x✝ : s.CompleteCopy
⊢ dist x✝¹ x✝ = dist x✝ x✝¹

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
x y z : s.CompleteCopy
⊢ dist x z ≤ dist x y + dist y z

pp: case refine_4
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
⊢ IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
x✝ : s.CompleteCopy
⊢ dist x✝ x✝ = 0
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ 0 ≤ dist x x

pp: case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ 0 ≤ dist x y

Tactic:
·

Goal state after:
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ 0 ≤ dist x x
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
x✝¹ x✝ : s.CompleteCopy
⊢ dist x✝¹ x✝ = dist x✝ x✝¹

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
x y z : s.CompleteCopy
⊢ dist x z ≤ dist x y + dist y z

pp: case refine_4
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
⊢ IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
x✝¹ x✝ : s.CompleteCopy
⊢ dist x✝¹ x✝ = dist x✝ x✝¹
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ 0 ≤ dist x y

Tactic:
·

Goal state after:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ 0 ≤ dist x y
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ dist x x ≤ 1

pp: case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ dist x y ≤ 1

Tactic:
·

Goal state after:
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ dist x x ≤ 1
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ dist x y ≤ 1

Tactic:
·

Goal state after:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ dist x y ≤ 1