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

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
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'

Tactic:
congr

Result:
case mk.mk.e_edist
α : 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
⊢ edist✝¹ = edist✝

case mk.mk.e_toUniformSpace
α : 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
⊢ toUniformSpace✝¹ = toUniformSpace✝

case mk.mk.e_toBornology
α : 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
⊢ toBornology✝¹ = toBornology✝

Proof state:
case mk.mk.e_toBornology
α : 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
⊢ toBornology✝¹ = toBornology✝

Tactic:
ext : 2

Result:
case mk.mk.e_toBornology.h_cobounded.h
α : 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
s✝ : Set α
⊢ s✝ ∈ cobounded α ↔ s✝ ∈ cobounded α