-- Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
theorem tan_arctan {z : ℂ} (h₁ : z ≠ I) (h₂ : z ≠ -I) : tan (arctan z) = z

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ tan z.arctan = z

Tactic:
unfold tan sin cos

Result:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (cexp (-z.arctan * I) - cexp (z.arctan * I)) * I / 2 / ((cexp (z.arctan * I) + cexp (-z.arctan * I)) / 2) = z

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (cexp (-z.arctan * I) - cexp (z.arctan * I)) * I / 2 / ((cexp (z.arctan * I) + cexp (-z.arctan * I)) / 2) = z

Tactic:
rw [div_div_eq_mul_div, div_mul_cancel₀ _ two_ne_zero, ← div_mul_eq_mul_div,
  ← mul_div_mul_right _ _ (exp_ne_zero (arctan z * I)), sub_mul, add_mul,
  ← exp_add, neg_mul, neg_add_cancel, exp_zero, ← exp_add, ← two_mul]

Result:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z

Proof state:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : -I = z
⊢ z = -I

Tactic:
exact h₂.symm

Result:
no goals

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ 1 + z * I ≠ 0

Tactic:
contrapose! h₁

Result:
z : ℂ
h₂ : z ≠ -I
h₁ : 1 + z * I = 0
⊢ z = I

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ 2 * (I * (-I / 2)) = 1

Tactic:
field_simp

Result:
no goals

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0

Tactic:
exact div_ne_zero z₁ z₂

Result:
no goals

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z

Tactic:
have z₁ : 1 + z * I ≠ 0 := by
  contrapose! h₁
  rw [add_eq_zero_iff_neg_eq, ← div_eq_iff I_ne_zero, div_I, neg_one_mul, neg_neg] at h₁
  exact h₁.symm

Result:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
⊢ 1 - z * I ≠ 0

Tactic:
contrapose! h₂

Result:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : 1 - z * I = 0
⊢ z = -I

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z

Tactic:
rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
  show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]

Result:
no goals

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
⊢ (1 - z * I - (1 + z * I)) / (1 + z * I + (1 - z * I)) * I = -(I * I) * z

Tactic:
ring

Result:
no goals

Proof state:
z : ℂ
h₂ : z ≠ -I
h₁ : I = z
⊢ z = I

Tactic:
exact h₁.symm

Result:
no goals

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z

Tactic:
have z₂ : 1 - z * I ≠ 0 := by
  contrapose! h₂
  rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂
  exact h₂.symm

Result:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z

Proof state:
z : ℂ
h₂ : z ≠ -I
h₁ : 1 + z * I = 0
⊢ z = I

Tactic:
rw [add_eq_zero_iff_neg_eq, ← div_eq_iff I_ne_zero, div_I, neg_one_mul, neg_neg] at h₁

Result:
z : ℂ
h₂ : z ≠ -I
h₁ : I = z
⊢ z = I

Proof state:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : 1 - z * I = 0
⊢ z = -I

Tactic:
rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂

Result:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : -I = z
⊢ z = -I

Proof state:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)

Tactic:
rw [arctan, ← mul_rotate, ← mul_assoc,
  show 2 * (I * (-I / 2)) = 1 by field_simp, one_mul, exp_log]

Result:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0