Theorem: proportion_inv_iff (Pythagoras/proportion.lean)

State before:
r s t u : ℝ
⊢ proportion r s t u ↔ proportion s r u t
Tactic:
constructor
State after:
case mp
r s t u : ℝ
⊢ proportion r s t u → proportion s r u t

case mpr
r s t u : ℝ
⊢ proportion s r u t → proportion r s t u

State before:
case mp
r s t u : ℝ
⊢ proportion r s t u → proportion s r u t

case mpr
r s t u : ℝ
⊢ proportion s r u t → proportion r s t u
Tactic:
all_goals exact fun h => proportion_inv h
State after:
no goals

State before:
case mpr
r s t u : ℝ
⊢ proportion s r u t → proportion r s t u
Tactic:
exact fun h => proportion_inv h
State after:
no goals