Theorem: dist_swap (Ray/Misc/Prod.lean)

State before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x y : A × B
⊢ dist x.swap y.swap = dist x y
Tactic:
rw [Prod.dist_eq, Prod.dist_eq]
State after:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x y : A × B
⊢ max (dist x.swap.1 y.swap.1) (dist x.swap.2 y.swap.2) = max (dist x.1 y.1) (dist x.2 y.2)

State before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x y : A × B
⊢ max (dist x.swap.1 y.swap.1) (dist x.swap.2 y.swap.2) = max (dist x.1 y.1) (dist x.2 y.2)
Tactic:
simp only [Prod.fst_swap, Prod.snd_swap, ge_iff_le, max_comm]
State after:
no goals