feat(data/complex/exponential): added @[mono] tag to exp_le_exp and exp_lt_exp (#3318)

added @[mono] tag to exp_le_exp and exp_lt_exp.

Author: chrispvm

src/data/complex/exponential.lean

@@ -927,6 +927,8 @@ lemma exp_strict_mono : strict_mono exp :=
   exact (lt_mul_iff_one_lt_left (exp_pos _)).2
     (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))
 
+@[mono] lemma exp_monotone : ∀ {x y : ℝ}, x ≤ y → exp x ≤ exp y := exp_strict_mono.monotone 
+
 lemma exp_lt_exp {x y : ℝ} : exp x < exp y ↔ x < y := exp_strict_mono.lt_iff_lt
 
 lemma exp_le_exp {x y : ℝ} : exp x ≤ exp y ↔ x ≤ y := exp_strict_mono.le_iff_le