awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
z : ℂ
h : ∀ (k : ℤ), z ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
pos : tan (z + z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
have pos₁ : tan (z + z) = (tan z + tan z) / (1 - HPow.hPow (β := ℕ) (tan z) 2)
Tactic: rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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)
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
have pos₂ : tan (z + z) = (tan z + tan z) / (1 - tan z * tan z)
Tactic: rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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)
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
have pos₃ : (tan z + tan z) / (1 - tan z * tan z) = (tan z + tan z) / (1 - tan z * tan z)
Tactic: rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]
-- 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 neg : tan (z + z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
Tactic: rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
z : ℂ
h : ∃ (k : ℤ), z = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
neg : tan (z + z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
have neg₁ : tan (z + z) = (tan z + tan z) / (1 - HPow.hPow (β := ℕ) (tan z) 2)
Tactic: rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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)
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
have neg₂ : tan (z + z) = (tan z + tan z) / (1 - tan z * tan z)
Tactic: rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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)
⊢ tan (2 * z) = 2 * tan z / (1 - HPow.hPow (β := ℕ) (tan z) 2)
have neg₃ : (tan z + tan z) / (1 - tan z * tan z) = (tan z + tan z) / (1 - tan z * tan z)
Tactic: rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, 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 * I ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), y * I = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
⊢ tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
have rw : (tan x + tan (y * I)) / (1 - tan x * tan (y * I)) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
Tactic: rw [tan_add h, tan_mul_I, mul_assoc]
-- 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 * 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)
⊢ tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
have rw₁ : (tan x + tanh y * I) / (1 - tan x * (tanh y * I)) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
Tactic: rw [tan_add h, tan_mul_I, mul_assoc]
-- 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 * 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)
⊢ tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
have rw₂ : (tan x + tanh y * I) / (1 - tan x * (tanh y * I)) = (tan x + tanh y * I) / (1 - tan x * (tanh y * I))
Tactic: rw [tan_add h, tan_mul_I, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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 = (tan (↑z.re : ℂ) + tanh (↑z.im : ℂ) * I) / (1 - tan (↑z.re : ℂ) * tanh (↑z.im : ℂ) * I)
have h₁ : z = (↑z.re : ℂ) + (↑z.im : ℂ) * I
Tactic: convert! tan_add_mul_I h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
h : cos x = 0
⊢ tan x = 0
have obtain : ∀ (k : ℤ) (hxk : x = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2), tan x = 0
Tactic: obtain ⟨k, hxk⟩ := cos_eq_zero_iff.mp h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
h : cos x ≠ -1
| cos x
have rw : HPow.hPow (β := ℕ) (cos (x / 2)) 2 - HPow.hPow (β := ℕ) (sin (x / 2)) 2
Tactic: rw [← mul_div_cancel₀ x two_ne_zero, cos_two_mul']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
h : cos x ≠ -1
⊢ cos x = (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
have conv_lhs : HPow.hPow (β := ℕ) (cos (x / 2)) 2 - HPow.hPow (β := ℕ) (sin (x / 2)) 2 =
  (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
Tactic: conv_lhs => rw [← mul_div_cancel₀ x two_ne_zero, cos_two_mul']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
Goal:
x : ℂ
h : cos x ≠ -1
⊢ HPow.hPow (β := ℕ) (cos (x / 2)) 2 - HPow.hPow (β := ℕ) (sin (x / 2)) 2 =
    (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
have this : cos (x / 2) ≠ 0
Tactic: have : cos (x / 2) ≠ 0 := by grind [cos_ne_zero_iff, cos_eq_neg_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
⊢ HPow.hPow (β := ℕ) (cos (x / 2)) 2 - HPow.hPow (β := ℕ) (sin (x / 2)) 2 =
    (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
have rw : HPow.hPow (β := ℕ) (cos (x / 2)) 2 - HPow.hPow (β := ℕ) (tan (x / 2) * cos (x / 2)) 2 =
  (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2) * HPow.hPow (β := ℕ) (cos (x / 2)) 2
Tactic: rw [div_eq_mul_inv (1 - tan (x / 2) ^ 2) (1 + tan (x / 2) ^ 2), inv_one_add_tan_sq this,
    ← tan_mul_cos this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
| sin x
have rw : 2 * sin (x / 2) * cos (x / 2)
Tactic: rw [← mul_div_cancel₀ x two_ne_zero, sin_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ sin x = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
have conv_lhs : 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
Tactic: conv_lhs => rw [← mul_div_cancel₀ x two_ne_zero, sin_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
have pos : ∀ (h : cos (x / 2) = 0), 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
Tactic: by_cases h : cos (x / 2) = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
pos :
  ∀ (h : cos (x / 2) = 0), 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
⊢ 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
have neg : ∀ (h : ¬cos (x / 2) = 0), 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
Tactic: by_cases h : cos (x / 2) = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
h : ¬cos (x / 2) = 0
⊢ 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
have neg : 2 * (tan (x / 2) * cos (x / 2)) * cos (x / 2) = 2 * tan (x / 2) * HPow.hPow (β := ℕ) (cos (x / 2)) 2
Tactic: rw [div_eq_mul_inv (2 * tan (x / 2)) (1 + tan (x / 2) ^ 2), inv_one_add_tan_sq h,
      ← tan_mul_cos h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
| tan x
have rw : 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)
Tactic: rw [← mul_div_cancel₀ x two_ne_zero, tan_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ tan x = 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)
have conv_lhs : tan x = 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)
Tactic: conv_lhs => rw [← mul_div_cancel₀ x two_ne_zero, tan_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
conv_lhs : tan x = 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)
⊢ tan x = 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)
have conv_lhs₁ : 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2) = 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)
Tactic: conv_lhs => rw [← mul_div_cancel₀ x two_ne_zero, tan_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
z w : ℂ
⊢ cos z = w ↔ HPow.hPow (β := ℕ) (cexp (z * I)) 2 - 2 * w * cexp (z * I) + 1 = 0
have rw : cos z - w = 0 ↔ HPow.hPow (β := ℕ) (cexp (z * I)) 2 - 2 * w * cexp (z * I) + 1 = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ ∃ (w : ℂ), w ≠ 0 ∧ 1 * (w * w) + -2 * x * w + 1 = 0
have rcases : ∀ (w : ℂ) (hw : 1 * (w * w) + -2 * x * w + 1 = 0), ∃ (w : ℂ), w ≠ 0 ∧ 1 * (w * w) + -2 * x * w + 1 = 0
Tactic: rcases exists_quadratic_eq_zero one_ne_zero
        ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with
      ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x w : ℂ
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ ∃ (w : ℂ), w ≠ 0 ∧ 1 * (w * w) + -2 * x * w + 1 = 0
have refine : w ≠ 0
Tactic: refine ⟨w, ?_, hw⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ ∃ (a : ℂ), cos a = x
have obtain : ∀ (w : ℂ) (w₀ : w ≠ 0) (hw : 1 * (w * w) + -2 * x * w + 1 = 0), ∃ (a : ℂ), cos a = x
Tactic: obtain ⟨w, w₀, hw⟩ : ∃ w ≠ 0, 1 * (w * w) + -2 * x * w + 1 = 0 := by
    rcases exists_quadratic_eq_zero one_ne_zero
        ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with
      ⟨w, hw⟩
    refine ⟨w, ?_, hw⟩
    rintro rfl
    simp only [zero_add, one_ne_zero, mul_zero] at hw
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ ∃ (a : ℂ), cos a = x
have refine : HPow.hPow (β := ℕ) (cexp (log w / I * I)) 2 - 2 * x * cexp (log w / I * I) + 1 = 0
Tactic: refine ⟨log w / I, cos_eq_iff_quadratic.2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ HPow.hPow (β := ℕ) (cexp (log w / I * I)) 2 - 2 * x * cexp (log w / I * I) + 1 = 0
have rw : HPow.hPow (β := ℕ) w 2 - 2 * x * w + 1 = 0
Tactic: rw [div_mul_cancel₀ _ I_ne_zero, exp_log w₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ HPow.hPow (β := ℕ) w 2 - 2 * x * w + 1 = 0
have h : HPow.hPow (β := ℕ) w 2 - 2 * x * w + 1 = 1 * (w * w) + -2 * x * w + 1
Tactic: convert! hw using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ ∃ (a : ℂ), sin a = x
have rcases : ∀ (z : ℂ), ∃ (a : ℂ), sin a = cos z
Tactic: rcases cos_surjective x with ⟨z, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
⊢ |cos x| = 1 ↔ ∃ (k : ℤ), (↑k : ℝ) * π = x
have rw : ((∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x) ↔ ∃ (k : ℤ), (↑k : ℝ) * π = x
Tactic: rw [← abs_one, abs_eq_abs, cos_eq_one_iff, cos_eq_neg_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
⊢ ((∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x) ↔ ∃ (k : ℤ), (↑k : ℝ) * π = x
have mp : ((∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x) → ∃ (k : ℤ), (↑k : ℝ) * π = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
mp : ((∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x) → ∃ (k : ℤ), (↑k : ℝ) * π = x
⊢ ((∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x) ↔ ∃ (k : ℤ), (↑k : ℝ) * π = x
have mpr : (∃ (k : ℤ), (↑k : ℝ) * π = x) → (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
n : ℤ
h : (↑n : ℝ) * π = x
⊢ (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x
have mpr : ∀ (n : ℤ) (h : (↑(n + n) : ℝ) * π = x), (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x
Tactic: obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
n : ℤ
h : (↑n : ℝ) * π = x
mpr :
  ∀ (n : ℤ) (h : (↑(n + n) : ℝ) * π = x), (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x
⊢ (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x
have mpr₁ : ∀ (n : ℤ) (h : (↑(2 * n + 1) : ℝ) * π = x), (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x
Tactic: obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
⊢ |sin x| = 1 ↔ ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x
have rw : ((∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x) ↔
  ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x
Tactic: rw [← abs_one, abs_eq_abs, sin_eq_one_iff, sin_eq_neg_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
⊢ ((∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x) ↔
    ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x
have mp : ((∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x) →
  ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
mp :
  ((∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x) →
    ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x
⊢ ((∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x) ↔
    ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x
have mpr : (∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x) →
  (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
n : ℤ
h : π / 2 + (↑n : ℝ) * π = x
⊢ (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x
have mpr : ∀ (n : ℤ) (h : π / 2 + (↑(n + n) : ℝ) * π = x),
  (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x
Tactic: obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℝ
n : ℤ
h : π / 2 + (↑n : ℝ) * π = x
mpr :
  ∀ (n : ℤ) (h : π / 2 + (↑(n + n) : ℝ) * π = x),
    (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x
⊢ (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x
have mpr₁ : ∀ (n : ℤ) (h : π / 2 + (↑(2 * n + 1) : ℝ) * π = x),
  (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x
Tactic: obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
θ : ℝ
hθ : cos θ ≠ 0
⊢ tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℝ) * π = θ
have revert : ∀ (hθ : cos θ ≠ 0), tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℝ) * π = θ
Tactic: revert hθ
Cleared hypotheses: hθ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (goal)
Goal:
x : ℂ
h : cos x ≠ 0
⊢ HasStrictDerivAt tan (1 / HPow.hPow (β := ℕ) (cos x) 2) x
have h₁ : 1 / HPow.hPow (β := ℕ) (cos x) 2 = (cos x * cos x - sin x * -sin x) / HPow.hPow (β := ℕ) (cos x) 2
Tactic: convert! (hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (goal)
Goal:
x : ℂ
h : cos x ≠ 0
⊢ 1 / HPow.hPow (β := ℕ) (cos x) 2 = (cos x * cos x - sin x * -sin x) / HPow.hPow (β := ℕ) (cos x) 2
have h₁ : ∀ (h : ¬cos x = 0),
  (HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2) / HPow.hPow (β := ℕ) (cos x) 2 =
    (cos x * cos x - sin x * -sin x) / HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw_mod_cast [← sin_sq_add_cos_sq x]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (goal)
Goal:
x : ℂ
hx : cos x = 0
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖tan x‖) (𝓝[≠] x) atTop
have simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop
Tactic: simp only [tan_eq_sin_div_cos, norm_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (hypothesis)
Goal:
x : ℂ
hx : cos x = 0
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop
have A : sin x ≠ 0
Tactic: have A : sin x ≠ 0 := fun h => by simpa [*, sq] using sin_sq_add_cos_sq x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (hypothesis)
Goal:
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop
have B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0)
Tactic: have B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0) :=
    hx ▸ (hasDerivAt_cos x).tendsto_nhdsNE (neg_ne_zero.2 A)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (goal)
Goal:
x : ℂ
⊢ ContinuousAt tan x ↔ cos x ≠ 0
have refine : ∀ (hc : ContinuousAt tan x) (h₀ : cos x = 0), False
Tactic: refine ⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (hypothesis)
Goal:
x : ℂ
h : cos x = 0
⊢ deriv tan x = 1 / HPow.hPow (β := ℕ) (cos x) 2
have this : ¬DifferentiableAt ℂ tan x
Tactic: have : ¬DifferentiableAt ℂ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
⊢ cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
have rw : cexp (z * I) + cexp (-z * I) = cexp (-(z * I) + 2 * I * z) + cexp (-(z * I)) * 1
Tactic: rw [mul_add, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
z : ℂ
⊢ (cexp (z * I) + cexp (-z * I)) / 2 / ((cexp (-z * I) - cexp (z * I)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
have h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
Tactic: have h1 : exp (z * I) + exp (-z * I) = exp (-(z * I)) * (exp (2 * I * z) + 1) := by
    rw [mul_add, ← Complex.exp_add]
    ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
have ring_nf : cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I)) * cexp (z * I * 2)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I)) * cexp (z * I * 2)
have rw : cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I) + z * (I * 2))
Tactic: rw [mul_assoc, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ (cexp (z * I) + cexp (-z * I)) / 2 / ((cexp (-z * I) - cexp (z * I)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
have h2 : cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
Tactic: have h2 : (exp (-z * I) - exp (z * I)) = exp (-(z * I)) * ((1 - exp (2 * I * z))) := by
    ring_nf
    rw [mul_assoc, ← Complex.exp_add]
    ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
⊢ (cexp (z * I) + cexp (-z * I)) / 2 / ((cexp (-z * I) - cexp (z * I)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
have rw : cexp (-(z * I)) * (cexp (2 * I * z) + 1) / 2 / (cexp (-(z * I)) * (1 - cexp (2 * I * z)) * I / 2) =
  (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
Tactic: rw [h1, h2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
⊢ ((↑π : ℂ) * z).cot = (cexp (2 * (↑π : ℂ) * I * z) + 1) / (I * (1 - cexp (2 * (↑π : ℂ) * I * z)))
have rw : (cexp (2 * I * ((↑π : ℂ) * z)) + 1) / (I * (1 - cexp (2 * I * ((↑π : ℂ) * z)))) =
  (cexp (2 * (↑π : ℂ) * I * z) + 1) / (I * (1 - cexp (2 * (↑π : ℂ) * I * z)))
Tactic: rw [cot_eq_exp_ratio (π * z)]