Theorem: proportion_symm' (Pythagoras/proportion.lean)

State before:
r s t u : ℝ
h : proportion r s t u
⊢ proportion t u r s
Tactic:
by_cases s_ne : s = 0
State after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
⊢ proportion t u r s

case neg
r s t u : ℝ
h : proportion r s t u
s_ne : ¬s = 0
⊢ proportion t u r s

State before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
⊢ proportion t u r s
Tactic:
have u_ne := (zero_of_proportion_iff h).mp s_ne
State after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
⊢ proportion t u r s

State before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
⊢ proportion t u r s
Tactic:
have inv := proportion_inv h
State after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
⊢ proportion t u r s

State before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
⊢ proportion t u r s
Tactic:
by_cases r_ne : r = 0
State after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
⊢ proportion t u r s

case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
⊢ proportion t u r s

State before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
⊢ proportion t u r s
Tactic:
have t_ne := (zero_of_proportion_iff inv).mp r_ne
State after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
t_ne : t = 0
⊢ proportion t u r s

State before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
t_ne : t = 0
⊢ proportion t u r s
Tactic:
rw [s_ne, r_ne, t_ne, u_ne]
State after:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
t_ne : t = 0
⊢ proportion 0 0 0 0

State before:
case pos
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : r = 0
t_ne : t = 0
⊢ proportion 0 0 0 0
Tactic:
exact proportion_of_zero
State after:
no goals

State before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
⊢ proportion t u r s
Tactic:
have t_ne := (zero_of_proportion_iff inv).not.mp r_ne
State after:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
t_ne : ¬t = 0
⊢ proportion t u r s

State before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
t_ne : ¬t = 0
⊢ proportion t u r s
Tactic:
rw [proportion_inv_iff]
State after:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
t_ne : ¬t = 0
⊢ proportion u t s r

State before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
u_ne : u = 0
inv : proportion s r u t
r_ne : ¬r = 0
t_ne : ¬t = 0
⊢ proportion u t s r
Tactic:
exact proportion_symm r_ne t_ne inv
State after:
no goals

State before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : ¬s = 0
⊢ proportion t u r s
Tactic:
have u_ne := (zero_of_proportion_iff h).not.mp s_ne
State after:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : ¬s = 0
u_ne : ¬u = 0
⊢ proportion t u r s

State before:
case neg
r s t u : ℝ
h : proportion r s t u
s_ne : ¬s = 0
u_ne : ¬u = 0
⊢ proportion t u r s
Tactic:
exact proportion_symm s_ne u_ne h
State after:
no goals