case inl.intro
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

case inr.intro.intro.intro
k l : ℤ
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
rcases h with (⟨h1, h2⟩ | ⟨⟨k, rfl⟩, ⟨l, rfl⟩⟩)
case inl.intro
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ (sin x * cos y / (cos x * cos y) + cos x * sin y / (cos x * cos y)) /
      (cos x * cos y / (cos x * cos y) - sin x * sin y / (cos x * cos y)) =
    (tan x + tan y) / (1 - tan x * tan y)
case inl.intro
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
rw [tan, sin_add, cos_add, ←
  div_div_div_cancel_right (sin x * cos y + cos x * sin y)
    (mul_ne_zero (cos_ne_zero_iff.mpr h1) (cos_ne_zero_iff.mpr h2)),
  add_div, sub_div]
no goals
case inl.intro
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ (sin x * cos y / (cos x * cos y) + cos x * sin y / (cos x * cos y)) /
      (cos x * cos y / (cos x * cos y) - sin x * sin y / (cos x * cos y)) =
    (tan x + tan y) / (1 - tan x * tan y)
simp only [← div_mul_div_comm, tan, mul_one, one_mul, div_self (cos_ne_zero_iff.mpr h1),
  div_self (cos_ne_zero_iff.mpr h2)]
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
case inr.intro.intro.intro
k l : ℤ
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
haveI t := tan_int_mul_pi_div_two
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan (↑(2 * k + 1) * ↑π / 2) = 0
hy : tan (↑(2 * l + 1) * ↑π / 2) = 0
hxy : tan (↑(2 * k + 1 + (2 * l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan (↑(2 * k + 1) * ↑π / 2) = 0
hy : tan (↑(2 * l + 1) * ↑π / 2) = 0
hxy : tan (↑(2 * k + 1 + (2 * l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one, hx, hy] at hx hy hxy
no goals
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
rw [hx, hy, add_zero, zero_div, mul_div_assoc, mul_div_assoc, ←
  add_mul (2 * (k : ℂ) + 1) (2 * l + 1) (π / 2), ← mul_div_assoc, hxy]