no goals
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
Φ : Z → X
Ψ : Z → Y
ε : ℝ
val✝¹ : X
val✝ : Y
⊢ glueDist Ψ Φ ε (Sum.swap (Sum.inl val✝¹)) (Sum.swap (Sum.inr val✝)) = glueDist Φ Ψ ε (Sum.inl val✝¹) (Sum.inr val✝)
simp only [glueDist, Sum.swap_inl, Sum.swap_inr, dist_comm, add_comm]
no goals
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
Φ : Z → X
Ψ : Z → Y
ε : ℝ
val✝¹ : Y
val✝ : X
⊢ glueDist Ψ Φ ε (Sum.swap (Sum.inr val✝¹)) (Sum.swap (Sum.inl val✝)) = glueDist Φ Ψ ε (Sum.inr val✝¹) (Sum.inl val✝)
simp only [glueDist, Sum.swap_inl, Sum.swap_inr, dist_comm, add_comm]