awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : cos x ≠ -1
rw : HPow.hPow (β := ℕ) (cos (x / 2)) 2 - HPow.hPow (β := ℕ) (sin (x / 2)) 2
| cos x

Tactic:
rw [← mul_div_cancel₀ x two_ne_zero, cos_two_mul']

Premises used: Complex.cos_two_mul', mul_div_cancel₀, two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : cos x ≠ -1
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)
⊢ cos x = (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']

Premises used: Complex.cos_two_mul', mul_div_cancel₀, two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : cos x ≠ -1
⊢ cos (x / 2) ≠ 0

Tactic:
grind [cos_ne_zero_iff, cos_eq_neg_one_iff]

Premises used: Complex.cos_ne_zero_iff, Complex.cos_eq_neg_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : cos x ≠ -1
⊢ cos (x / 2) ≠ 0

Tactic:
have : cos (x / 2) ≠ 0 := by grind [cos_ne_zero_iff, cos_eq_neg_one_iff]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
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
⊢ 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:
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]

Premises used: HSub.hSub, HDiv.hDiv, Complex.tan_mul_cos, div_eq_mul_inv, HPow.hPow, HAdd.hAdd, Complex.tan, Complex.inv_one_add_tan_sq, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
⊢ 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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
rw : 2 * sin (x / 2) * cos (x / 2)
| sin x

Tactic:
rw [← mul_div_cancel₀ x two_ne_zero, sin_two_mul]

Premises used: Complex.sin_two_mul, mul_div_cancel₀, two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
conv_lhs : 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)
⊢ sin x = 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]

Premises used: Complex.sin_two_mul, mul_div_cancel₀, two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
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)
neg :
  ∀ (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)

Tactic:
by_cases h : cos (x / 2) = 0

Premises used: Complex.cos, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
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)

Tactic:
simp [h, tan_eq_zero_of_cos_eq_zero]

Premises used: Complex.tan_eq_zero_of_cos_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : ¬cos (x / 2) = 0
neg : 2 * (tan (x / 2) * cos (x / 2)) * cos (x / 2) = 2 * tan (x / 2) * HPow.hPow (β := ℕ) (cos (x / 2)) 2
⊢ 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (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]

Premises used: HMul.hMul, HDiv.hDiv, Complex.tan_mul_cos, div_eq_mul_inv, HPow.hPow, HAdd.hAdd, Complex.tan, Complex.inv_one_add_tan_sq, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
h : ¬cos (x / 2) = 0
⊢ 2 * (tan (x / 2) * cos (x / 2)) * cos (x / 2) = 2 * tan (x / 2) * HPow.hPow (β := ℕ) (cos (x / 2)) 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
rw : 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)
| tan x

Tactic:
rw [← mul_div_cancel₀ x two_ne_zero, tan_two_mul]

Premises used: mul_div_cancel₀, two_ne_zero, Complex.tan_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
conv_lhs : tan x = 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)
conv_lhs₁ :
  2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2) =
    2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)
⊢ 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]

Premises used: mul_div_cancel₀, two_ne_zero, Complex.tan_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
⊢ ContinuousOn tan {x : ℂ | cos x ≠ 0}

Tactic:
continuousOn_sin.div continuousOn_cos fun _x => id

Premises used: Complex.continuousOn_cos, Complex.continuousOn_sin, id, ContinuousOn.div, Complex.tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
⊢ Continuous (Y := ℂ) fun (x : (↑{x : ℂ | cos x ≠ 0} : Type)) ↦ tan (↑x : ℂ)

Tactic:
continuousOn_iff_continuous_restrict.1 continuousOn_tan

Premises used: Complex.continuousOn_tan, Complex.tan, continuousOn_iff_continuous_restrict, Iff.mp, Set.restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z w : ℂ
rw : cos z - w = 0 ↔ HPow.hPow (β := ℕ) (cexp (z * I)) 2 - 2 * w * cexp (z * I) + 1 = 0
⊢ cos z = w ↔ HPow.hPow (β := ℕ) (cexp (z * I)) 2 - 2 * w * cexp (z * I) + 1 = 0

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z w : ℂ
⊢ HPow.hPow (β := ℕ) (cexp (z * I)) 2 + 1 - cexp (z * I) * 2 * w = cexp (z * I) * (cexp (z * I) - 2 * w) + 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z w : ℂ
⊢ cos z - w = 0 ↔ HPow.hPow (β := ℕ) (cexp (z * I)) 2 - 2 * w * cexp (z * I) + 1 = 0

Tactic:
simpa [field, cos, exp_neg] using Eq.congr (by ring) rfl

Premises used: Complex.cos, Complex.exp_neg, Eq.congr, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
rcases : ∀ (w : ℂ) (hw : 1 * (w * w) + -2 * x * w + 1 = 0), ∃ (w : ℂ), w ≠ 0 ∧ 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⟩

Premises used: exists_quadratic_eq_zero, pow_two, two_ne_zero, Exists.intro, Complex.cpow_nat_inv_pow, one_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x w : ℂ
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ ∃ (w : ℂ), w ≠ 0 ∧ 1 * (w * w) + -2 * x * w + 1 = 0

Tactic:
⟨w, ?_, hw⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x w : ℂ
hw : 1 * (w * w) + -2 * x * w + 1 = 0
refine : w ≠ 0
⊢ ∃ (w : ℂ), w ≠ 0 ∧ 1 * (w * w) + -2 * x * w + 1 = 0

Tactic:
refine ⟨w, ?_, hw⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
hw : 1 * HMul.hMul (α := ℂ) 0 0 + -2 * x * 0 + 1 = 0
⊢ False

Tactic:
simp only [zero_add, one_ne_zero, mul_zero] at hw

Premises used: zero_add, MulZeroClass.mul_zero, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
obtain : ∀ (w : ℂ) (w₀ : w ≠ 0) (hw : 1 * (w * w) + -2 * x * w + 1 = 0), ∃ (a : ℂ), cos a = x
⊢ ∃ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ ∃ (a : ℂ), cos a = x

Tactic:
⟨log w / I, cos_eq_iff_quadratic.2 ?_⟩

Premises used: Iff.mpr, Complex.log, Complex.cos_eq_iff_quadratic, HDiv.hDiv, Exists.intro, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
refine : HPow.hPow (β := ℕ) (cexp (log w / I * I)) 2 - 2 * x * cexp (log w / I * I) + 1 = 0
⊢ ∃ (a : ℂ), cos a = x

Tactic:
refine ⟨log w / I, cos_eq_iff_quadratic.2 ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
rw : HPow.hPow (β := ℕ) w 2 - 2 * x * w + 1 = 0
⊢ HPow.hPow (β := ℕ) (cexp (log w / I * I)) 2 - 2 * x * cexp (log w / I * I) + 1 = 0

Tactic:
rw [div_mul_cancel₀ _ I_ne_zero, exp_log w₀]

Premises used: div_mul_cancel₀, Complex.I_ne_zero, Complex.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ 1 * (w * w) + -2 * x * w + 1 = 0

Tactic:
hw
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
h : HPow.hPow (β := ℕ) w 2 - 2 * x * w + 1 = 1 * (w * w) + -2 * x * w + 1
⊢ HPow.hPow (β := ℕ) w 2 - 2 * x * w + 1 = 0

Tactic:
convert! hw using 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ HPow.hPow (β := ℕ) w 2 - 2 * x * w + 1 = 1 * (w * w) + -2 * x * w + 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
⊢ range cos = univ

Tactic:
cos_surjective.range_eq

Premises used: Complex.cos_surjective, Function.Surjective.range_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
rcases : ∀ (z : ℂ), ∃ (a : ℂ), sin a = cos z
⊢ ∃ (a : ℂ), sin a = x

Tactic:
rcases cos_surjective x with ⟨z, rfl⟩

Premises used: Complex.cos_surjective, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z : ℂ
⊢ ∃ (a : ℂ), sin a = cos z

Tactic:
⟨z + π / 2, sin_add_pi_div_two z⟩

Premises used: Real.pi, HDiv.hDiv, Complex.ofReal, HAdd.hAdd, Exists.intro, OfNat.ofNat, Complex.sin_add_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
z : ℂ
⊢ ∃ (a : ℂ), sin a = cos z

Tactic:
exact ⟨z + π / 2, sin_add_pi_div_two z⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
⊢ range sin = univ

Tactic:
sin_surjective.range_eq

Premises used: Function.Surjective.range_eq, Complex.sin_surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℝ
⊢ cos θ = 0 ↔ ∃ (k : ℤ), θ = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2

Tactic:
mod_cast @Complex.cos_eq_zero_iff θ

Premises used: Int.cast, Complex.cos_eq_zero_iff, Real.pi, HMul.hMul, Complex.cos, Real.cos, congrArg, Complex.ofReal_div._simp_1, cast, Exists, Int.cast_add, Complex.ofReal_add, HDiv.hDiv, Int.cast_ofNat, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, funext, Iff, Int.cast_mul, Int.cast_mul._simp_1, Complex.ofReal_cos._simp_1, HAdd.hAdd, congr, Int.cast_add._simp_1, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Int.cast_one, Complex.ofReal_mul, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℝ
⊢ cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2

Tactic:
mod_cast @Complex.cos_ne_zero_iff θ

Premises used: Int.cast, Real.pi, HMul.hMul, Complex.cos, Real.cos, congrArg, Complex.ofReal_div._simp_1, cast, Int.cast_add, Complex.ofReal_add, HDiv.hDiv, Ne, Int.cast_ofNat, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, Iff, Int.cast_mul, Int.cast_mul._simp_1, Complex.ofReal_cos._simp_1, HAdd.hAdd, Complex.cos_ne_zero_iff, congr, Int.cast_add._simp_1, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Not, Int.cast_one, Complex.ofReal_mul, Complex.ofReal_inj._simp_1, Eq.trans, forall_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℝ
⊢ cos x = cos y ↔ ∃ (k : ℤ), y = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + x ∨ y = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π - x

Tactic:
mod_cast @Complex.cos_eq_cos_iff x y

Premises used: Int.cast, Real.pi, HMul.hMul, Real.cos, congrArg, Complex.ofReal_sub._simp_1, HSub.hSub, cast, Exists, Int.cast_ofNat, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, funext, Iff, Int.cast_mul, Int.cast_mul._simp_1, Complex.ofReal_cos._simp_1, HAdd.hAdd, congr, congrFun', Or, OfNat.ofNat, Eq.symm, Eq, Complex.cos_eq_cos_iff, Complex.ofReal_add._simp_1, Complex.ofReal_mul, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℝ
⊢ sin x = sin y ↔ ∃ (k : ℤ), y = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + x ∨ y = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π - x

Tactic:
mod_cast @Complex.sin_eq_sin_iff x y

Premises used: Int.cast, Real.pi, HMul.hMul, congrArg, Complex.ofReal_sub._simp_1, Complex.sin, HSub.hSub, cast, Exists, Int.cast_add, Complex.ofReal_add, Complex.sin_eq_sin_iff, Int.cast_ofNat, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, funext, Iff, Int.cast_mul, Int.cast_mul._simp_1, HAdd.hAdd, congr, Complex.ofReal_sin._simp_1, Int.cast_add._simp_1, congrFun', Or, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Real.sin, Complex.ofReal_add._simp_1, Int.cast_one, Complex.ofReal_mul, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
⊢ cos x = -1 ↔ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x

Tactic:
mod_cast @Complex.cos_eq_neg_one_iff x

Premises used: Int.cast_neg, Int.cast, Real.pi, HMul.hMul, Complex.cos, Real.cos, congrArg, Int.cast_negSucc._simp_1, Complex.ofReal_neg, cast, Exists, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, funext, Iff, Complex.ofReal_cos._simp_1, HAdd.hAdd, congr, congrFun', Complex.cos_eq_neg_one_iff, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Complex.ofReal_add._simp_1, Neg.neg, Int.cast_one, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
rw : ((∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x) ↔ ∃ (k : ℤ), (↑k : ℝ) * π = x
⊢ |cos x| = 1 ↔ ∃ (k : ℤ), (↑k : ℝ) * π = x

Tactic:
rw [← abs_one, abs_eq_abs, cos_eq_one_iff, cos_eq_neg_one_iff]

Premises used: Real.cos_eq_one_iff, abs_one, Real.cos_eq_neg_one_iff, abs_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
mp : ((∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x) → ∃ (k : ℤ), (↑k : ℝ) * π = x
mpr : (∃ (k : ℤ), (↑k : ℝ) * π = x) → (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x
⊢ ((∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x) ↔ ∃ (k : ℤ), (↑k : ℝ) * π = x

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : (↑n : ℝ) * (2 * π) = x
⊢ (↑(2 * n) : ℝ) * π = x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : (↑n : ℝ) * (2 * π) = x
⊢ ∃ (k : ℤ), (↑k : ℝ) * π = x

Tactic:
exact ⟨2 * n, by grind⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : π + (↑n : ℝ) * (2 * π) = x
⊢ (↑(1 + n * 2) : ℝ) * π = x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : π + (↑n : ℝ) * (2 * π) = x
⊢ ∃ (k : ℤ), (↑k : ℝ) * π = x

Tactic:
exact ⟨1 + n * 2, by grind⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : (↑n : ℝ) * π = x
mpr :
  ∀ (n : ℤ) (h : (↑(n + n) : ℝ) * π = x), (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x
mpr₁ :
  ∀ (n : ℤ) (h : (↑(2 * n + 1) : ℝ) * π = x),
    (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x
⊢ (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x

Tactic:
obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd

Premises used: Int.even_or_odd, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : (↑(n + n) : ℝ) * π = x
⊢ (↑n : ℝ) * (2 * π) = x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : (↑(n + n) : ℝ) * π = x
⊢ (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x

Tactic:
exact .inl ⟨n, by grind⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : (↑(2 * n + 1) : ℝ) * π = x
⊢ π + (↑n : ℝ) * (2 * π) = x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : (↑(2 * n + 1) : ℝ) * π = x
⊢ (∃ (n : ℤ), (↑n : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), π + (↑k : ℝ) * (2 * π) = x

Tactic:
exact .inr ⟨n, by grind⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
⊢ sin x = 1 ↔ ∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x

Tactic:
mod_cast @Complex.sin_eq_one_iff x

Premises used: Int.cast, Real.pi, HMul.hMul, congrArg, Complex.sin, Complex.ofReal_div._simp_1, cast, Exists, HDiv.hDiv, Complex.ofReal, Nat.cast, Complex.sin_eq_one_iff, Complex.ofReal_mul._simp_1, funext, Iff, HAdd.hAdd, congr, Complex.ofReal_sin._simp_1, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Real.sin, Complex.ofReal_add._simp_1, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
⊢ sin x = -1 ↔ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x

Tactic:
mod_cast @Complex.sin_eq_neg_one_iff x

Premises used: Int.cast_neg, Int.cast, Real.pi, Complex.sin_eq_neg_one_iff, HMul.hMul, congrArg, Int.cast_negSucc._simp_1, Complex.sin, Complex.ofReal_div._simp_1, Complex.ofReal_neg, cast, Exists, HDiv.hDiv, Complex.ofReal, Nat.cast, Complex.ofReal_neg._simp_1, Complex.ofReal_mul._simp_1, funext, Iff, HAdd.hAdd, congr, Complex.ofReal_sin._simp_1, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Real.sin, Complex.ofReal_add._simp_1, Neg.neg, Int.cast_one, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
rw :
  ((∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x) ↔
    ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x
⊢ |sin x| = 1 ↔ ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x

Tactic:
rw [← abs_one, abs_eq_abs, sin_eq_one_iff, sin_eq_neg_one_iff]

Premises used: Real.sin_eq_neg_one_iff, abs_one, abs_eq_abs, Real.sin_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
mp :
  ((∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x) →
    ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x
mpr :
  (∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x) →
    (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x
⊢ ((∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x) ↔
    ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : π / 2 + (↑n : ℝ) * (2 * π) = x
⊢ π / 2 + (↑(2 * n) : ℝ) * π = x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : π / 2 + (↑n : ℝ) * (2 * π) = x
⊢ ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x

Tactic:
exact ⟨2 * n, by grind⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : -(π / 2) + (↑n : ℝ) * (2 * π) = x
⊢ π / 2 + (↑(-1 + n * 2) : ℝ) * π = x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : -(π / 2) + (↑n : ℝ) * (2 * π) = x
⊢ ∃ (k : ℤ), π / 2 + (↑k : ℝ) * π = x

Tactic:
exact ⟨-1 + n * 2, by grind⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : π / 2 + (↑n : ℝ) * π = x
mpr :
  ∀ (n : ℤ) (h : π / 2 + (↑(n + n) : ℝ) * π = x),
    (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x
mpr₁ :
  ∀ (n : ℤ) (h : π / 2 + (↑(2 * n + 1) : ℝ) * π = x),
    (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x
⊢ (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x

Tactic:
obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd

Premises used: Int.even_or_odd, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : π / 2 + (↑(n + n) : ℝ) * π = x
⊢ π / 2 + (↑n : ℝ) * (2 * π) = x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : π / 2 + (↑(n + n) : ℝ) * π = x
⊢ (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x

Tactic:
exact .inl ⟨n, by grind⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : π / 2 + (↑(2 * n + 1) : ℝ) * π = x
⊢ -(π / 2) + (↑(n + 1) : ℝ) * (2 * π) = x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
n : ℤ
h : π / 2 + (↑(2 * n + 1) : ℝ) * π = x
⊢ (∃ (k : ℤ), π / 2 + (↑k : ℝ) * (2 * π) = x) ∨ ∃ (k : ℤ), -(π / 2) + (↑k : ℝ) * (2 * π) = x

Tactic:
exact .inr ⟨n + 1, by grind⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℝ
⊢ tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℝ) * π / 2 = θ

Tactic:
mod_cast @Complex.tan_eq_zero_iff θ

Premises used: Int.cast, Real.pi, HMul.hMul, congrArg, Complex.ofReal_div._simp_1, cast, Exists, HDiv.hDiv, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, funext, Iff, Complex.tan, congr, Complex.tan_eq_zero_iff, congrFun', Nat.cast_zero, Complex.ofReal_tan._simp_1, OfNat.ofNat, Eq.symm, Eq, Complex.ofReal_inj._simp_1, Eq.trans, Real.tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℝ
hθ : cos θ ≠ 0
revert : ∀ (hθ : cos θ ≠ 0), tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℝ) * π = θ
⊢ tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℝ) * π = θ

Tactic:
revert hθ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℝ
⊢ ∀ (hθ : cos θ ≠ 0), tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℝ) * π = θ

Tactic:
exact_mod_cast @Complex.tan_eq_zero_iff' θ

Premises used: Complex.tan_eq_zero_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℝ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), (↑k : ℝ) * π / 2 ≠ θ

Tactic:
mod_cast @Complex.tan_ne_zero_iff θ

Premises used: Int.cast, Real.pi, HMul.hMul, congrArg, Complex.ofReal_div._simp_1, cast, HDiv.hDiv, Ne, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, Complex.tan_ne_zero_iff, Iff, Complex.tan, congr, congrFun', Nat.cast_zero, Complex.ofReal_tan._simp_1, OfNat.ofNat, Eq.symm, Eq, Not, Complex.ofReal_inj._simp_1, Eq.trans, Real.tan, forall_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
h : cos x = 0
⊢ tan x = 0

Tactic:
mod_cast @Complex.tan_eq_zero_of_cos_eq_zero x (mod_cast h)

Premises used: Complex.cos, Real.cos, congrArg, Complex.tan_eq_zero_of_cos_eq_zero, cast, Complex.ofReal, Nat.cast, Complex.ofReal_cos._simp_1, Complex.tan, congrFun', Nat.cast_zero, Complex.ofReal_tan._simp_1, OfNat.ofNat, Eq.symm, Eq, Complex.ofReal_inj._simp_1, Eq.trans, Real.tan