case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

case neg
z : ℂ
h : ¬∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
z : ℂ
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
by_cases h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2
no goals
case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]
case neg
z : ℂ
h : ∃ x, z = (2 * ↑x + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
case neg
z : ℂ
h : ¬∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
rw [not_forall_not] at h
no goals
case neg
z : ℂ
h : ∃ x, z = (2 * ↑x + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]