no goals
α : Type u_1
x y z : ℝ
l : Filter α
f g : α → ℝ
⊢ ((fun x => exp (f x)) =Θ[l] fun x => exp (g x)) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => abs (f x - g x)
simp only [isBoundedUnder_le_abs, ← isBoundedUnder_le_neg, neg_sub, IsTheta,
  isBigO_exp_comp_exp_comp, Pi.sub_def]