perf(Analysis.Complex.Exponential): make Complex.exp an irreducible_def (leanprover-community#32599)

Recall that `irreducible_def` creates a declaration that is not unfolded by both
the elaborator and the kernel (without some special effort). Currently,
`UpperHalfPlane.isometry_vertical_line` takes a long time to type check in the
kernel because it attempts to unfold `Real.exp` during whnf.
Unfolding `Real.exp` quickly leads to unfolding `Complex.exp`.
I don't think there is any good reason to want to unfold `Complex.exp` so this PR makes it an `irreducible_def`.

Co-authored-by: Matthew Ballard <matt@mrb.email>

Author: mattrobball

Mathlib/Analysis/Complex/Exponential.lean

@@ -57,7 +57,7 @@ def exp' (z : ℂ) : CauSeq ℂ (‖·‖) :=
 
 /-- The complex exponential function, defined via its Taylor series -/
 @[pp_nodot]
-def exp (z : ℂ) : ℂ :=
+irreducible_def exp (z : ℂ) : ℂ :=
   CauSeq.lim (exp' z)
 
 /-- scoped notation for the complex exponential function -/
@@ -171,7 +171,7 @@ theorem exp_int_mul (z : ℂ) (n : ℤ) : Complex.exp (n * z) = Complex.exp z ^
 
 @[simp]
 theorem exp_conj : exp (conj x) = conj (exp x) := by
-  dsimp [exp]
+  simp only [exp]
   rw [← lim_conj]
   refine congr_arg CauSeq.lim (CauSeq.ext fun _ => ?_)
   dsimp [exp', Function.comp_def, cauSeqConj]

MathlibTest/Recall.lean

@@ -27,7 +27,7 @@ error: value mismatch
 has value
   id
 but is expected to have value
-  fun z ↦ (Complex.exp' z).lim
+  Complex.wrapped✝.1
 -/
 #guard_msgs in recall Complex.exp : ℂ → ℂ := id