awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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))
⊢ 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))
have inr₁ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) =
  HAdd.hAdd (α := ℂ) 0 0 / (1 - HMul.hMul (α := ℂ) 0 0)
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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)
⊢ 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))
have inr₂ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) =
  0 / (1 - HMul.hMul (α := ℂ) 0 0)
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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)
⊢ 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))
have inr₃ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
⊢ 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))
have inr₄ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * ((↑π : ℂ) / 2) + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
⊢ 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))
have inr₅ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * ((↑π : ℂ) / 2) + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * ((↑π : ℂ) / 2)) = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
⊢ 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))
have inr₆ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1)) * ((↑π : ℂ) / 2)) = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
⊢ 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))
have inr₈ : Eq (α := ℂ) 0 0
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
⊢ ((∀ (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
have 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
Tactic: rcases h with ⟨x_ne, minus_y_ne⟩ | ⟨x_eq, minus_y_eq⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
⊢ ((∀ (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
have 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
Tactic: rcases h with ⟨x_ne, minus_y_ne⟩ | ⟨x_eq, minus_y_eq⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
have inl : ∀ (l : ℤ), -y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
Tactic: refine .inl ⟨x_ne, fun l => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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) * (↑π : ℂ) / 2
have inl : ¬y = -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2)
Tactic: rw [Ne, neg_eq_iff_eq_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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) * (↑π : ℂ) / 2)
have h : -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑(-l - 1) : ℂ) + 1) * (↑π : ℂ) / 2
Tactic: convert! minus_y_ne (-l - 1) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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) = (HMul.hMul (α := ℂ) 2 (↑(-l - 1) : ℂ) + 1) * (↑π : ℂ) / 2
have h : -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (2 * HSub.hSub (α := ℂ) (-(↑l : ℂ)) 1 + 1) * (↑π : ℂ) / 2
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
have inr : ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
Tactic: refine .inr ⟨x_eq, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
minus_y_eq : ∃ (l : ℤ), y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ ∃ (l : ℤ), -y = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
have inr : ∀ (l : ℤ),
  ∃ (l_1 : ℤ),
    -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑l_1 : ℂ) + 1) * (↑π : ℂ) / 2
Tactic: rcases minus_y_eq with ⟨l, rfl⟩
Cleared hypotheses: y, minus_y_eq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
⊢ ∃ (l_1 : ℤ),
    -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑l_1 : ℂ) + 1) * (↑π : ℂ) / 2
have h : -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑(-l - 1) : ℂ) + 1) * (↑π : ℂ) / 2
Tactic: use -l - 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
x_eq : ∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
l : ℤ
⊢ -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (HMul.hMul (α := ℂ) 2 (↑(-l - 1) : ℂ) + 1) * (↑π : ℂ) / 2
have h : -((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = (2 * HSub.hSub (α := ℂ) (-(↑l : ℂ)) 1 + 1) * (↑π : ℂ) / 2
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
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)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
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)
have this₁ : tan (x + -y) = (tan x + -tan y) / (1 - tan x * -tan y)
Tactic: rw [tan_neg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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)
have h₁ : 1 + tan x * tan y = 1 - tan x * -tan y
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
z : ℂ
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
have pos : ∀ (h : ∀ (k : ℤ), z ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2),
  tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
Tactic: by_cases! h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
z : ℂ
pos :
  ∀ (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)
have neg : ∀ (h : ∃ (k : ℤ), z = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2),
  tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
Tactic: by_cases! h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
z : ℂ
h : ∀ (k : ℤ), z ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
have pos : tan (z + z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
Tactic: rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]