Theorem: ball_prod_same' (Ray/Misc/Prod.lean)

State before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r
Tactic:
have s := ball_prod_same x.fst x.snd r
State after:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
s : ball x.1 r ×ˢ ball x.2 r = ball (x.1, x.2) r
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r

State before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
s : ball x.1 r ×ˢ ball x.2 r = ball (x.1, x.2) r
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r
Tactic:
simp only [Prod.mk.eta] at s
State after:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
s : ball x.1 r ×ˢ ball x.2 r = ball x r
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r

State before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
s : ball x.1 r ×ˢ ball x.2 r = ball x r
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r
Tactic:
exact s.symm
State after:
no goals