Theorem: zero_of_proportion_iff (Pythagoras/proportion.lean)

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

case mpr
r s t u : ℝ
h : proportion r s t u
⊢ u = 0 → s = 0

State before:
case mp
r s t u : ℝ
h : proportion r s t u
⊢ s = 0 → u = 0
Tactic:
intro s_ne
State after:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
⊢ u = 0

State before:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
⊢ u = 0
Tactic:
have := (h.2.2.2.2 0 1).1
State after:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
this : ↑0 * r = ↑1 * s → ↑0 * t = ↑1 * u
⊢ u = 0

State before:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
this : ↑0 * r = ↑1 * s → ↑0 * t = ↑1 * u
⊢ u = 0
Tactic:
simp at this
State after:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
this : 0 = s → 0 = u
⊢ u = 0

State before:
case mp
r s t u : ℝ
h : proportion r s t u
s_ne : s = 0
this : 0 = s → 0 = u
⊢ u = 0
Tactic:
exact (this s_ne.symm).symm
State after:
no goals

State before:
case mpr
r s t u : ℝ
h : proportion r s t u
⊢ u = 0 → s = 0
Tactic:
intro u_ne
State after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
⊢ s = 0

State before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
⊢ s = 0
Tactic:
have hh := (h.2.2.2.2 0 1).2.1
State after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : ↑0 * r < ↑1 * s → ↑0 * t < ↑1 * u
⊢ s = 0

State before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : ↑0 * r < ↑1 * s → ↑0 * t < ↑1 * u
⊢ s = 0
Tactic:
simp at hh
State after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
⊢ s = 0

State before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
⊢ s = 0
Tactic:
by_contra s_ne
State after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
⊢ False

State before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
⊢ False
Tactic:
have : 0 < s := Ne.lt_of_le (fun ss => s_ne ss.symm) h.2.1
State after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
this : 0 < s
⊢ False

State before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
this : 0 < s
⊢ False
Tactic:
have := hh this
State after:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
this✝ : 0 < s
this : 0 < u
⊢ False

State before:
case mpr
r s t u : ℝ
h : proportion r s t u
u_ne : u = 0
hh : 0 < s → 0 < u
s_ne : ¬s = 0
this✝ : 0 < s
this : 0 < u
⊢ False
Tactic:
linarith
State after:
no goals