Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u_3
m' : PseudoMetricSpace α
toDist✝ : Dist α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
h :
  { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
        edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
        toBornology := toBornology✝, cobounded_sets := hB }.toDist =
    m'.toDist
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
      toBornology := toBornology✝, cobounded_sets := hB }.toDist
d' : Dist α := m'.toDist
⊢ { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
      toBornology := toBornology✝, cobounded_sets := hB } =
    m'

Tactic:
obtain ⟨_, _, _, _, hed', _, hU', _, hB'⟩ := m'

Goal state after:
α : Type u_3
toDist✝¹ : Dist α
dist_self✝¹ : ∀ (x : α), dist x x = 0
dist_comm✝¹ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝¹ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝¹ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝¹ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝¹ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝¹ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α :=
  { toDist := toDist✝¹, dist_self := dist_self✝¹, dist_comm := dist_comm✝¹, dist_triangle := dist_triangle✝¹,
      edist := edist✝¹, edist_dist := hed, toUniformSpace := toUniformSpace✝¹, uniformity_dist := hU,
      toBornology := toBornology✝¹, cobounded_sets := hB }.toDist
toDist✝ : Dist α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝ : α → α → ℝ≥0∞
hed' : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝ : UniformSpace α
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝ : Bornology α
hB' : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
h :
  { toDist := toDist✝¹, dist_self := dist_self✝¹, dist_comm := dist_comm✝¹, dist_triangle := dist_triangle✝¹,
        edist := edist✝¹, edist_dist := hed, toUniformSpace := toUniformSpace✝¹, uniformity_dist := hU,
        toBornology := toBornology✝¹, cobounded_sets := hB }.toDist =
    { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
        edist := edist✝, edist_dist := hed', toUniformSpace := toUniformSpace✝, uniformity_dist := hU',
        toBornology := toBornology✝, cobounded_sets := hB' }.toDist
d' : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed', toUniformSpace := toUniformSpace✝, uniformity_dist := hU',
      toBornology := toBornology✝, cobounded_sets := hB' }.toDist
⊢ { toDist := toDist✝¹, dist_self := dist_self✝¹, dist_comm := dist_comm✝¹, dist_triangle := dist_triangle✝¹,
      edist := edist✝¹, edist_dist := hed, toUniformSpace := toUniformSpace✝¹, uniformity_dist := hU,
      toBornology := toBornology✝¹, cobounded_sets := hB } =
    { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed', toUniformSpace := toUniformSpace✝, uniformity_dist := hU',
      toBornology := toBornology✝, cobounded_sets := hB' }