-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean
lemma Complex.cot_eq_exp_ratio (z : ℂ) :
    cot z = (Complex.exp (2 * I * z) + 1) / (I * (1 - Complex.exp (2 * I * z)))

Proof state:
z : ℂ
h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : (cexp (-(z * I)) - cexp (z * I)) * I = cexp (-(z * I)) * (I * (1 - cexp (2 * I * z)))
⊢ (cexp (z * I) + cexp (-(z * I))) / ((cexp (-(z * I)) - cexp (z * I)) * I) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
rw [h1, h2, mul_div_mul_left _ _ (Complex.exp_ne_zero _)]

Result:
no goals

Proof state:
z : ℂ
h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ I * cexp (-(z * I)) - I * cexp (z * I) = I * cexp (-(z * I)) - I * cexp (-(z * I) + z * I * 2)

Tactic:
ring_nf

Result:
no goals

Proof state:
z : ℂ
h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ I * cexp (-(z * I)) - I * cexp (z * I) = I * cexp (-(z * I)) - I * cexp (-(z * I)) * cexp (z * I * 2)

Tactic:
rw [mul_assoc, ← Complex.exp_add]

Result:
z : ℂ
h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ I * cexp (-(z * I)) - I * cexp (z * I) = I * cexp (-(z * I)) - I * cexp (-(z * I) + z * I * 2)

Proof state:
z : ℂ
h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ (cexp (z * I) + cexp (-(z * I))) / ((cexp (-(z * I)) - cexp (z * I)) * I) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
have h2 : (exp (-(z * I)) - exp (z * I)) * I = exp (-(z * I)) * (I * (1 - exp (2 * I * z))) := by
  ring_nf
  rw [mul_assoc, ← Complex.exp_add]
  ring_nf

Result:
z : ℂ
h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : (cexp (-(z * I)) - cexp (z * I)) * I = cexp (-(z * I)) * (I * (1 - cexp (2 * I * z)))
⊢ (cexp (z * I) + cexp (-(z * I))) / ((cexp (-(z * I)) - cexp (z * I)) * I) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Proof state:
z : ℂ
h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ (cexp (-(z * I)) - cexp (z * I)) * I = cexp (-(z * I)) * (I * (1 - cexp (2 * I * z)))

Tactic:
ring_nf

Result:
z : ℂ
h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ I * cexp (-(z * I)) - I * cexp (z * I) = I * cexp (-(z * I)) - I * cexp (-(z * I)) * cexp (z * I * 2)

Proof state:
z : ℂ
⊢ z.cot = (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
rw [Complex.cot, Complex.sin, Complex.cos]

Result:
z : ℂ
⊢ (cexp (z * I) + cexp (-z * I)) / 2 / ((cexp (-z * I) - cexp (z * I)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Proof state:
z : ℂ
⊢ cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)

Tactic:
rw [mul_add, ← Complex.exp_add]

Result:
z : ℂ
⊢ cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I) + 2 * I * z) + cexp (-(z * I)) * 1

Proof state:
z : ℂ
⊢ (cexp (z * I) + cexp (-z * I)) / 2 / ((cexp (-z * I) - cexp (z * I)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
field_simp

Result:
z : ℂ
⊢ (cexp (z * I) + cexp (-(z * I))) / ((cexp (-(z * I)) - cexp (z * I)) * I) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Proof state:
z : ℂ
⊢ cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I) + 2 * I * z) + cexp (-(z * I)) * 1

Tactic:
simp only [mul_one, add_left_inj]

Result:
z : ℂ
⊢ cexp (z * I) = cexp (-(z * I) + 2 * I * z)

Proof state:
z : ℂ
⊢ cexp (z * I) = cexp (-(z * I) + 2 * I * z)

Tactic:
ring_nf

Result:
no goals

Proof state:
z : ℂ
⊢ (cexp (z * I) + cexp (-(z * I))) / ((cexp (-(z * I)) - cexp (z * I)) * I) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
have h1 : exp (z * I) + exp (-(z * I)) = exp (-(z * I)) * (exp (2 * I * z) + 1) := by
  rw [mul_add, ← Complex.exp_add]
  simp only [mul_one, add_left_inj]
  ring_nf

Result:
z : ℂ
h1 : cexp (z * I) + cexp (-(z * I)) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ (cexp (z * I) + cexp (-(z * I))) / ((cexp (-(z * I)) - cexp (z * I)) * I) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))