lean_workbook_plus_43717
OpenOne way is like mcrasher shows: you can multiply by so that you get ( ).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43717 : ∀ x : ℝ, (exp x / (4 + 5 * exp (3 * x))) * (exp (-x) / exp (-x)) = 1 / (4 * exp (-x) + 5 * exp (2 * x)) := by sorry
Source