Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mk.mk
α : Type u_2
inst✝ : TopologicalSpace α
toEDist✝¹ : EDist α
edist_self✝¹ : ∀ (x : α), edist x x = 0
edist_comm✝¹ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝¹ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le✝¹ : (uniformSpaceOfEDist edist edist_self✝¹ edist_comm✝¹ edist_triangle✝¹).toTopologicalSpace ≤ inst✝
topology_eq_on_restrict✝¹ :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le✝ : (uniformSpaceOfEDist edist edist_self✝ edist_comm✝ edist_triangle✝).toTopologicalSpace ≤ inst✝
topology_eq_on_restrict✝ :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
h :
  { toEDist := toEDist✝¹, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
        topology_le := topology_le✝¹, topology_eq_on_restrict := topology_eq_on_restrict✝¹ }.toEDist =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ }.toEDist
⊢ { toEDist := toEDist✝¹, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
      topology_le := topology_le✝¹, topology_eq_on_restrict := topology_eq_on_restrict✝¹ } =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_2
inst✝ : TopologicalSpace α
toEDist✝¹ : EDist α
edist_self✝¹ : ∀ (x : α), edist x x = 0
edist_comm✝¹ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝¹ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le✝¹ : (uniformSpaceOfEDist edist edist_self✝¹ edist_comm✝¹ edist_triangle✝¹).toTopologicalSpace ≤ inst✝
topology_eq_on_restrict✝¹ :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le✝ : (uniformSpaceOfEDist edist edist_self✝ edist_comm✝ edist_triangle✝).toTopologicalSpace ≤ inst✝
topology_eq_on_restrict✝ :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
h :
  { toEDist := toEDist✝¹, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
        topology_le := topology_le✝¹, topology_eq_on_restrict := topology_eq_on_restrict✝¹ }.toEDist =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ }.toEDist
⊢ { toEDist := toEDist✝¹, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
      topology_le := topology_le✝¹, topology_eq_on_restrict := topology_eq_on_restrict✝¹ } =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ }