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

State before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
⊢ ball x.swap r = swap '' ball x r
Tactic:
apply Set.ext
State after:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
⊢ ∀ (x_1 : B × A), x_1 ∈ ball x.swap r ↔ x_1 ∈ swap '' ball x r

State before:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
⊢ ∀ (x_1 : B × A), x_1 ∈ ball x.swap r ↔ x_1 ∈ swap '' ball x r
Tactic:
intro y
State after:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
y : B × A
⊢ y ∈ ball x.swap r ↔ y ∈ swap '' ball x r

State before:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
y : B × A
⊢ y ∈ ball x.swap r ↔ y ∈ swap '' ball x r
Tactic:
rw [swap_mem', Metric.mem_ball, Metric.mem_ball, Prod.dist_eq, Prod.dist_eq]
State after:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
y : B × A
⊢ max (dist y.1 x.swap.1) (dist y.2 x.swap.2) < r ↔ max (dist y.swap.1 x.1) (dist y.swap.2 x.2) < r

State before:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
y : B × A
⊢ max (dist y.1 x.swap.1) (dist y.2 x.swap.2) < r ↔ max (dist y.swap.1 x.1) (dist y.swap.2 x.2) < r
Tactic:
simp only [ge_iff_le, max_lt_iff, Prod.fst_swap, Prod.snd_swap, and_comm]
State after:
no goals