x y : ℂ
⊢ exp (x + -x) = exp x * (exp x)⁻¹
x y : ℂ
⊢ exp (-x) = (exp x)⁻¹
rw [← mul_right_inj' (exp_ne_zero x), ← exp_add]
no goals
x y : ℂ
⊢ exp (x + -x) = exp x * (exp x)⁻¹
simp [mul_inv_cancel (exp_ne_zero x)]