-- Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
theorem arctan_tan {z : ℂ} (h₀ : z ≠ π / 2) (h₁ : -(π / 2) < z.re) (h₂ : z.re ≤ π / 2) :
    arctan (tan z) = z

Proof state:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + sin z * I) / (cos (-z) + sin (-z) * I)) = z

Tactic:
rw [← exp_mul_I, ← exp_mul_I, ← exp_sub, show z * I - -z * I = 2 * (I * z) by ring, log_exp,
  show -I / 2 * (2 * (I * z)) = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]

Result:
case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < (2 * (I * z)).im

case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ (2 * (I * z)).im ≤ π

Proof state:
case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < 2 * z.re

Tactic:
rwa [← div_lt_iff₀' two_pos, neg_div]

Result:
no goals

Proof state:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I)) = z

Tactic:
conv_lhs =>
  enter [2, 1, 2]
  rw [sub_eq_add_neg, ← neg_mul, ← sin_neg, ← cos_neg]

Result:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + sin z * I) / (cos (-z) + sin (-z) * I)) = z

Proof state:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ (tan z).arctan = z

Tactic:
unfold arctan tan

Result:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((1 + sin z / cos z * I) / (1 - sin z / cos z * I)) = z

Proof state:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((1 + sin z / cos z * I) / (1 - sin z / cos z * I)) = z

Tactic:
rw [← mul_div_mul_right (1 + _) _ h, add_mul, sub_mul, one_mul, ← mul_rotate, mul_div_cancel₀ _ h]

Result:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I)) = z

Proof state:
case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ 2 * z.re ≤ π

Tactic:
rwa [← le_div_iff₀' two_pos]

Result:
no goals

Proof state:
case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < (2 * (I * z)).im

case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ (2 * (I * z)).im ≤ π

Tactic:
all_goals norm_num

Result:
case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < 2 * z.re

case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ 2 * z.re ≤ π

Proof state:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
⊢ (tan z).arctan = z

Tactic:
have h := cos_ne_zero_of_arctan_bounds h₀ h₁ h₂

Result:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ (tan z).arctan = z

Proof state:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ z * I - -z * I = 2 * (I * z)

Tactic:
ring

Result:
no goals

Proof state:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * (2 * (I * z)) = -(I * I) * z

Tactic:
ring

Result:
no goals

Proof state:
case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ (2 * (I * z)).im ≤ π

Tactic:
norm_num

Result:
case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ 2 * z.re ≤ π