Theorem: log_neg_log_strict_anti (Ray/Dynamics/Multibrot/Postcritical.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
⊢ (-y.log).log < (-x.log).log ↔ x < y
Tactic:
have lx := neg_pos.mpr (Real.log_neg x0 x1)
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
lx : 0 < -x.log
⊢ (-y.log).log < (-x.log).log ↔ x < y

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
lx : 0 < -x.log
⊢ (-y.log).log < (-x.log).log ↔ x < y
Tactic:
have ly := neg_pos.mpr (Real.log_neg y0 y1)
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
lx : 0 < -x.log
ly : 0 < -y.log
⊢ (-y.log).log < (-x.log).log ↔ x < y

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
lx : 0 < -x.log
ly : 0 < -y.log
⊢ (-y.log).log < (-x.log).log ↔ x < y
Tactic:
rw [Real.log_lt_log_iff ly lx, neg_lt_neg_iff, Real.log_lt_log_iff x0 y0]
State after:
no goals