case mk
α✝ : Type u
β : Type v
X : Type ?u.547543
ι : Type ?u.547546
inst✝ : PseudoMetricSpace α✝
α : Type u_1
m' : MetricSpace α
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ mk eq_of_dist_eq_zero✝ = m'
α✝ : Type u
β : Type v
X : Type ?u.547543
ι : Type ?u.547546
inst✝ : PseudoMetricSpace α✝
α : Type u_1
m m' : MetricSpace α
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ m = m'
cases m
case mk.mk
α✝ : Type u
β : Type v
X : Type ?u.547543
ι : Type ?u.547546
inst✝ : PseudoMetricSpace α✝
α : Type u_1
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ mk eq_of_dist_eq_zero✝¹ = mk eq_of_dist_eq_zero✝
case mk
α✝ : Type u
β : Type v
X : Type ?u.547543
ι : Type ?u.547546
inst✝ : PseudoMetricSpace α✝
α : Type u_1
m' : MetricSpace α
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ mk eq_of_dist_eq_zero✝ = m'
cases m'
case mk.mk.e_toPseudoMetricSpace
α✝ : Type u
β : Type v
X : Type ?u.547543
ι : Type ?u.547546
inst✝ : PseudoMetricSpace α✝
α : Type u_1
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ toPseudoMetricSpace✝¹ = toPseudoMetricSpace✝
case mk.mk
α✝ : Type u
β : Type v
X : Type ?u.547543
ι : Type ?u.547546
inst✝ : PseudoMetricSpace α✝
α : Type u_1
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ mk eq_of_dist_eq_zero✝¹ = mk eq_of_dist_eq_zero✝
congr
case mk.mk.e_toPseudoMetricSpace.h
α✝ : Type u
β : Type v
X : Type ?u.547543
ι : Type ?u.547546
inst✝ : PseudoMetricSpace α✝
α : Type u_1
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
case mk.mk.e_toPseudoMetricSpace
α✝ : Type u
β : Type v
X : Type ?u.547543
ι : Type ?u.547546
inst✝ : PseudoMetricSpace α✝
α : Type u_1
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ toPseudoMetricSpace✝¹ = toPseudoMetricSpace✝
ext1
no goals
case mk.mk.e_toPseudoMetricSpace.h
α✝ : Type u
β : Type v
X : Type ?u.547543
ι : Type ?u.547546
inst✝ : PseudoMetricSpace α✝
α : Type u_1
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
assumption