-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem PseudoMetricSpace.ext {α : Type*} {m m' : PseudoMetricSpace α}
    (h : m.toDist = m'.toDist) : m = m'

Proof state:
case mk
α : 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
d : Dist α := toDist
d' : Dist α := toDist
⊢ mk dist_self✝ dist_comm✝ dist_triangle✝ edist✝ hed toUniformSpace✝ hU toBornology✝ hB = m'

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

Result:
case mk.mk
α : 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 α
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
d' : Dist α := toDist
⊢ mk dist_self✝¹ dist_comm✝¹ dist_triangle✝¹ edist✝¹ hed toUniformSpace✝¹ hU toBornology✝¹ hB =
    mk dist_self✝ dist_comm✝ dist_triangle✝ edist✝ hed' toUniformSpace✝ hU' toBornology✝ hB'

Proof state:
case mk.mk
α : 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 α
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
d' : Dist α := toDist
⊢ mk dist_self✝¹ dist_comm✝¹ dist_triangle✝¹ edist✝¹ hed toUniformSpace✝¹ hU toBornology✝¹ hB =
    mk dist_self✝ dist_comm✝ dist_triangle✝ edist✝ hed' toUniformSpace✝ hU' toBornology✝ hB'

Tactic:
obtain rfl : d = d' := h

Result:
case mk.mk
α : 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
edist✝ : α → α → ℝ≥0∞
toUniformSpace✝ : UniformSpace α
toBornology✝ : Bornology α
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
hed' : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α := toDist
⊢ mk dist_self✝¹ dist_comm✝¹ dist_triangle✝¹ edist✝¹ hed toUniformSpace✝¹ hU toBornology✝¹ hB =
    mk dist_self✝ dist_comm✝ dist_triangle✝ edist✝ hed' toUniformSpace✝ hU' toBornology✝ hB'

Proof state:
α : Type u_3
m m' : PseudoMetricSpace α
h : toDist = toDist
⊢ m = m'

Tactic:
let d := m.toDist

Result:
α : Type u_3
m m' : PseudoMetricSpace α
h : toDist = toDist
d : Dist α := toDist
⊢ m = m'