awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
h2 : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
inl :
  (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)
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Tactic:
rw [tan, sin_add, cos_add, ←
      div_div_div_cancel_right₀ (mul_ne_zero (cos_ne_zero_iff.mpr h1) (cos_ne_zero_iff.mpr h2)),
      add_div, sub_div]

Premises used: Iff.mpr, div_div_div_cancel_right₀, sub_div, Complex.cos_add, Complex.sin_add, Complex.tan, Complex.cos_ne_zero_iff, mul_ne_zero, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
h2 : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 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)

Tactic:
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)]

Premises used: Iff.mpr, div_mul_div_comm, Complex.tan, Complex.cos_ne_zero_iff, mul_one, one_mul, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
k l : ℤ
⊢ ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0

Tactic:
haveI t := tan_int_mul_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
⊢ tan ((↑(2 * k + 1) : ℂ) * (↑π : ℂ) / 2) = 0

Tactic:
obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
hx : tan ((↑(2 * k + 1) : ℂ) * (↑π : ℂ) / 2) = 0
⊢ tan ((↑(2 * l + 1) : ℂ) * (↑π : ℂ) / 2) = 0

Tactic:
obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
hx : tan ((↑(2 * k + 1) : ℂ) * (↑π : ℂ) / 2) = 0
hy : tan ((↑(2 * l + 1) : ℂ) * (↑π : ℂ) / 2) = 0
⊢ tan ((↑(2 * k + 1 + (2 * l + 1)) : ℂ) * (↑π : ℂ) / 2) = 0

Tactic:
obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
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 ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) = 0

Tactic:
simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one] at hx hy hxy

Premises used: Int.cast_two, Int.cast_add, Int.cast_mul, Int.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
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
hx₁ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) = 0
⊢ tan ((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = 0

Tactic:
simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one] at hx hy hxy

Premises used: Int.cast_two, Int.cast_add, Int.cast_mul, Int.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
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
hx₁ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) = 0
hy₁ : tan ((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = 0
⊢ tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1)) * (↑π : ℂ) / 2) = 0

Tactic:
simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one] at hx hy hxy

Premises used: Int.cast_two, Int.cast_add, Int.cast_mul, Int.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
hx : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) = 0
hy : tan ((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = 0
hxy : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1)) * (↑π : ℂ) / 2) = 0
inr :
  tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) =
    (0 + tan ((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2)) /
      (1 - 0 * tan ((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2))
inr₁ :
  tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) =
    HAdd.hAdd (α := ℂ) 0 0 / (1 - HMul.hMul (α := ℂ) 0 0)
inr₂ :
  tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) =
    0 / (1 - HMul.hMul (α := ℂ) 0 0)
inr₃ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = 0
inr₄ :
  tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * ((↑π : ℂ) / 2) + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = 0
inr₅ :
  tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * ((↑π : ℂ) / 2) + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * ((↑π : ℂ) / 2)) = 0
inr₆ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1)) * ((↑π : ℂ) / 2)) = 0
inr₇ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1)) * (↑π : ℂ) / 2) = 0
inr₈ inr₉ : Eq (α := ℂ) 0 0
⊢ tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) =
    (tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) +
        tan ((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2)) /
      (1 -
        tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) *
          tan ((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2))

Tactic:
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]

Premises used: add_mul, Int.cast, Real.pi, HMul.hMul, mul_div_assoc, zero_div, HDiv.hDiv, Complex.ofReal, HAdd.hAdd, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h :
  (∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
    ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Tactic:
tan_add (Or.inl h)

Premises used: Complex.tan_add, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
inl :
  ∀ (x_ne : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2)
    (minus_y_ne : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2),
    ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
        ∀ (l : ℤ), -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
      (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
        ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
inr :
  ∀ (x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2)
    (minus_y_eq : ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2),
    ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
        ∀ (l : ℤ), -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
      (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
        ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
rcases h with ⟨x_ne, minus_y_ne⟩ | ⟨x_eq, minus_y_eq⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
.inl ⟨x_ne, fun l => ?_⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
inl : ∀ (l : ℤ), -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
refine .inl ⟨x_ne, fun l => ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
inl : ¬y = -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2)
⊢ -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
rw [Ne, neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg, Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
⊢ y ≠ (HMul.hMul (α := ℂ) 2 (↑(-l - 1) : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
minus_y_ne (-l - 1)

Premises used: HSub.hSub, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
h : -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑(-l - 1) : ℂ) + 1) * (↑π : ℂ) / 2
⊢ ¬y = -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2)

Tactic:
convert! minus_y_ne (-l - 1) using 2

Premises used: HSub.hSub, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
h : -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (2 * HSub.hSub (α := ℂ) (-(↑l : ℂ)) 1 + 1) * (↑π : ℂ) / 2
⊢ -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑(-l - 1) : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
⊢ -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (2 * HSub.hSub (α := ℂ) (-(↑l : ℂ)) 1 + 1) * (↑π : ℂ) / 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_eq : ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
.inr ⟨x_eq, ?_⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_eq : ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
inr : ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
refine .inr ⟨x_eq, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_eq : ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
inr :
  ∀ (l : ℤ),
    ∃ (l_1 : ℤ),
      -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑l_1 : ℂ) + 1) * (↑π : ℂ) / 2
⊢ ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
rcases minus_y_eq with ⟨l, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
h : -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑(-l - 1) : ℂ) + 1) * (↑π : ℂ) / 2
⊢ ∃ (l_1 : ℤ),
    -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑l_1 : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
use -l - 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
h : -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (2 * HSub.hSub (α := ℂ) (-(↑l : ℂ)) 1 + 1) * (↑π : ℂ) / 2
⊢ -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑(-l - 1) : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
⊢ -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (2 * HSub.hSub (α := ℂ) (-(↑l : ℂ)) 1 + 1) * (↑π : ℂ) / 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ tan (x + -y) = (tan x + tan (-y)) / (1 - tan x * tan (-y))

Tactic:
have := tan_add (x := x) (y := -y) <| by
    rcases h with ⟨x_ne, minus_y_ne⟩ | ⟨x_eq, minus_y_eq⟩
    · refine .inl ⟨x_ne, fun l => ?_⟩
      rw [Ne, neg_eq_iff_eq_neg]
      convert! minus_y_ne (-l - 1) using 2
      push_cast
      ring
    · refine .inr ⟨x_eq, ?_⟩
      rcases minus_y_eq with ⟨l, rfl⟩
      use -l - 1
      push_cast
      ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
this : tan (x + -y) = (tan x + tan (-y)) / (1 - tan x * tan (-y))
⊢ tan (x + -y) = (tan x + -tan y) / (1 - tan x * -tan y)

Tactic:
rw [tan_neg] at this

Premises used: Complex.tan_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
this : tan (x + -y) = (tan x + -tan y) / (1 - tan x * -tan y)
⊢ tan (x + -y) = (tan x + -tan y) / (1 - tan x * -tan y)

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
this : tan (x + -y) = (tan x + -tan y) / (1 - tan x * -tan y)
h₁ : 1 + tan x * tan y = 1 - tan x * -tan y
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

Tactic:
convert! this using 2
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
this : tan (x + -y) = (tan x + -tan y) / (1 - tan x * -tan y)
⊢ 1 + tan x * tan y = 1 - tan x * -tan y

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h :
  (∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
    ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

Tactic:
tan_sub (Or.inl h)

Premises used: Complex.tan_sub, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z : ℂ
pos :
  ∀ (h : ∀ (k : ℤ), z ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2),
    tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
neg :
  ∀ (h : ∃ (k : ℤ), z = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2),
    tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)

Tactic:
by_cases! h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z : ℂ
h : ∀ (k : ℤ), z ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
pos : tan (z + z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
pos₁ : tan (z + z) = (tan z + tan z) / (1 - HPow.hPow (β := ℕ) (tan z) 2)
pos₂ : tan (z + z) = (tan z + tan z) / (1 - tan z * tan z)
pos₃ pos₄ : (tan z + tan z) / (1 - tan z * tan z) = (tan z + tan z) / (1 - tan z * tan z)
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)

Tactic:
rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]

Premises used: two_mul, Complex.tan_add, sq, And.intro, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z : ℂ
h : ∃ (k : ℤ), z = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
neg : tan (z + z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
neg₁ : tan (z + z) = (tan z + tan z) / (1 - HPow.hPow (β := ℕ) (tan z) 2)
neg₂ : tan (z + z) = (tan z + tan z) / (1 - tan z * tan z)
neg₃ neg₄ : (tan z + tan z) / (1 - tan z * tan z) = (tan z + tan z) / (1 - tan z * tan z)
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)

Tactic:
rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]

Premises used: two_mul, Complex.tan_add, sq, And.intro, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), y * I ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), y * I = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
rw : (tan x + tan (y * I)) / (1 - tan x * tan (y * I)) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
rw₁ : (tan x + tanh y * I) / (1 - tan x * (tanh y * I)) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
rw₂ rw₃ : (tan x + tanh y * I) / (1 - tan x * (tanh y * I)) = (tan x + tanh y * I) / (1 - tan x * (tanh y * I))
⊢ tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)

Tactic:
rw [tan_add h, tan_mul_I, mul_assoc]

Premises used: mul_assoc, Complex.tan_add, Complex.tan_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z : ℂ
h :
  ((∀ (k : ℤ), (↑z.re : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), (↑z.im : ℂ) * I ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), (↑z.re : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), (↑z.im : ℂ) * I = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ tan ((↑z.re : ℂ) + (↑z.im : ℂ) * I) =
    (tan (↑z.re : ℂ) + tanh (↑z.im : ℂ) * I) / (1 - tan (↑z.re : ℂ) * tanh (↑z.im : ℂ) * I)

Tactic:
tan_add_mul_I h

Premises used: Complex.tan_add_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z : ℂ
h :
  ((∀ (k : ℤ), (↑z.re : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), (↑z.im : ℂ) * I ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), (↑z.re : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), (↑z.im : ℂ) * I = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
h₁ : z = (↑z.re : ℂ) + (↑z.im : ℂ) * I
⊢ tan z = (tan (↑z.re : ℂ) + tanh (↑z.im : ℂ) * I) / (1 - tan (↑z.re : ℂ) * tanh (↑z.im : ℂ) * I)

Tactic:
convert! tan_add_mul_I h

Premises used: Complex.tan_add_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z : ℂ
h :
  ((∀ (k : ℤ), (↑z.re : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), (↑z.im : ℂ) * I ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), (↑z.re : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), (↑z.im : ℂ) * I = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ z = (↑z.re : ℂ) + (↑z.im : ℂ) * I

Tactic:
(re_add_im z).symm

Premises used: Complex.re_add_im, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z : ℂ
h :
  ((∀ (k : ℤ), (↑z.re : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), (↑z.im : ℂ) * I ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), (↑z.re : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), (↑z.im : ℂ) * I = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ z = (↑z.re : ℂ) + (↑z.im : ℂ) * I

Tactic:
exact (re_add_im z).symm

Premises used: Complex.re_add_im, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : cos x = 0
obtain : ∀ (k : ℤ) (hxk : x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2), tan x = 0
⊢ tan x = 0

Tactic:
obtain ⟨k, hxk⟩ := cos_eq_zero_iff.mp h

Premises used: Complex.cos_eq_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : cos x = 0
k : ℤ
hxk : x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
⊢ (↑(2 * k + 1) : ℂ) * (↑π : ℂ) / 2 = x

Tactic:
simp [hxk]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : cos x = 0
k : ℤ
hxk : x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
⊢ tan x = 0

Tactic:
exact tan_eq_zero_iff.mpr ⟨2 * k + 1, by simp [hxk]⟩

Premises used: Iff.mpr, HMul.hMul, HAdd.hAdd, Complex.tan_eq_zero_iff, Exists.intro, OfNat.ofNat