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
h✝ : y = 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
h✝ : ¬y = 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
h✝ : y = 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
h✝ : ¬y = 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
h✝ : y = 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
h✝ : ¬y = 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
h✝ : y = 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
h✝ : ¬y = 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
h✝ : y = 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
h✝ : ¬y = 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
h✝ : y = 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
h✝ : ¬y = 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
h✝ : y = 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
h✝ : ¬y = 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
h✝ : y = 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
h✝ : ¬y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1