Theorem: exp_neg_div_lt (Ray/Dynamics/Multibrot/Specific.lean)

State before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c⁻¹ ^ b < 2.7182818283 ^ a) _auto✝
⊢ (-(↑a / ↑b)).exp < c
Tactic:
rw [Real.exp_neg, inv_lt (Real.exp_pos _) c0]
State after:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c⁻¹ ^ b < 2.7182818283 ^ a) _auto✝
⊢ c⁻¹ < (↑a / ↑b).exp

State before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c⁻¹ ^ b < 2.7182818283 ^ a) _auto✝
⊢ c⁻¹ < (↑a / ↑b).exp
Tactic:
exact lt_exp_div a0 b0 (inv_pos.mpr c0) h0
State after:
no goals