Theorem: proportion_eq (Pythagoras/proportion.lean)

State before:
r s : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
r_ne : r ≠ 0
s_ne : s ≠ 0
⊢ proportion r r s s
Tactic:
rw [(proportion_iff hr hr hs hs r_ne s_ne).symm]
State after:
r s : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
r_ne : r ≠ 0
s_ne : s ≠ 0
⊢ r / r = s / s

State before:
r s : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
r_ne : r ≠ 0
s_ne : s ≠ 0
⊢ r / r = s / s
Tactic:
field_simp
State after:
no goals