[GOAL]
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K L : ConvexBody V
h : K.carrier = L.carrier
⊢ K = L
[PROOFSTEP]
cases K
[GOAL]
case mk
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
L : ConvexBody V
carrier✝ : Set V
convex'✝ : Convex ℝ carrier✝
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : Set.Nonempty carrier✝
h : { carrier := carrier✝, convex' := convex'✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }.carrier = L.carrier
⊢ { carrier := carrier✝, convex' := convex'✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ } = L
[PROOFSTEP]
cases L
[GOAL]
case mk.mk
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
carrier✝¹ : Set V
convex'✝¹ : Convex ℝ carrier✝¹
isCompact'✝¹ : IsCompact carrier✝¹
nonempty'✝¹ : Set.Nonempty carrier✝¹
carrier✝ : Set V
convex'✝ : Convex ℝ carrier✝
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : Set.Nonempty carrier✝
h :
  { carrier := carrier✝¹, convex' := convex'✝¹, isCompact' := isCompact'✝¹, nonempty' := nonempty'✝¹ }.carrier =
    { carrier := carrier✝, convex' := convex'✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }.carrier
⊢ { carrier := carrier✝¹, convex' := convex'✝¹, isCompact' := isCompact'✝¹, nonempty' := nonempty'✝¹ } =
    { carrier := carrier✝, convex' := convex'✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }
[PROOFSTEP]
congr
[GOAL]
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K✝ L✝ K L : ConvexBody V
⊢ EMetric.hausdorffEdist ↑K ↑L ≠ ⊤
[PROOFSTEP]
apply_rules [Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded, ConvexBody.nonempty, ConvexBody.bounded]
[GOAL]
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K L x✝¹ x✝ : ConvexBody V
⊢ (fun x y => ↑{ val := Metric.hausdorffDist ↑x ↑y, property := (_ : 0 ≤ Metric.hausdorffDist ↑x ↑y) }) x✝¹ x✝ =
    ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K L : ConvexBody V
⊢ EMetric.hausdorffEdist ↑K ↑L = edist K L
[PROOFSTEP]
rw [edist_dist]
[GOAL]
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K L : ConvexBody V
⊢ EMetric.hausdorffEdist ↑K ↑L = ENNReal.ofReal (dist K L)
[PROOFSTEP]
exact (ENNReal.ofReal_toReal hausdorffEdist_ne_top).symm
