awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv :
  Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
hf :
  ∀ (y : ℝ),
    ∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p) =
      eval y ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
refine :
  ∀ (i : ℝ[X]) (hi : i ∈ f.support),
    |HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval x i)| ≤
      HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval 1 i)
⊢ LE.le (α := ℝ) (∑ i ∈ f.support, |HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval x i)|)
    (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval 1 p))

Tactic:
refine Finset.sum_le_sum (fun i hi => ?_)

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv :
  Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
hf :
  ∀ (y : ℝ),
    ∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p) =
      eval y ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
i : ℝ[X]
hi : i ∈ f.support
obtain :
  ∀ (m : ℕ) (hm : m ∈ Set.Icc 0 (n - k)) (hi : T ℝ (↑m : ℤ) = i),
    |HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval x i)| ≤
      HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval 1 i)
⊢ |HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval x i)| ≤
    HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval 1 i)

Tactic:
obtain ⟨m, hm, hi⟩ := (Set.mem_image ..).mp (hfsupp hi)

Premises used: Set.mem_image, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv :
  Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
hf :
  ∀ (y : ℝ),
    ∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p) =
      eval y ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
i : ℝ[X]
hi_1 : i ∈ f.support
m : ℕ
hm : m ∈ Set.Icc 0 (n - k)
hi : T ℝ (↑m : ℤ) = i
grw :
  HSMul.hSMul (α := ℕ) (β := ℝ) ((f : (a : ℝ[X]) → ℕ) (T ℝ (↑m : ℤ)) : ℕ) 1 ≤
    HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) (T ℝ (↑m : ℤ)) : ℕ) (eval 1 (T ℝ (↑m : ℤ)))
⊢ |HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval x i)| ≤
    HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval 1 i)

Tactic:
grw [abs_nsmul, ← hi, abs_eval_T_real_le_one m hx]

Premises used: Polynomial.Chebyshev.abs_eval_T_real_le_one, Nat.cast, abs_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this :
  Membership.mem (γ := Submodule ℕ ℝ[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
f : ℝ[X] →₀ ℕ
hfsupp : (↑f.support : Set ℝ[X]) ⊆ (fun (m : ℕ) ↦ T ℝ (↑m : ℤ)) '' Set.Icc 0 (n - k)
hfderiv :
  Eq (α := ℝ[X]) (∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) p)
    ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
hf :
  ∀ (y : ℝ),
    ∑ p ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) p : ℕ) (eval y p) =
      eval y ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
i : ℝ[X]
hi_1 : i ∈ f.support
m : ℕ
hm : m ∈ Set.Icc 0 (n - k)
hi : T ℝ (↑m : ℤ) = i
⊢ HSMul.hSMul (α := ℕ) (β := ℝ) ((f : (a : ℝ[X]) → ℕ) (T ℝ (↑m : ℤ)) : ℕ) 1 ≤
    HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) (T ℝ (↑m : ℤ)) : ℕ) (eval 1 (T ℝ (↑m : ℤ)))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
rw : cexp (θ * I - -θ * I) = -1 ↔ cexp (2 * θ * I) = -1
⊢ (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1

Tactic:
rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul,
      add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub]

Premises used: Complex.exp_ne_zero, MulZeroClass.zero_mul, add_eq_zero_iff_eq_neg, two_ne_zero, div_eq_iff, neg_eq_neg_one_mul, Complex.exp_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
⊢ cexp (θ * I - -θ * I) = -1 ↔ cexp (2 * θ * I) = -1

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
⊢ (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1

Tactic:
have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1 := by
    rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul,
      add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub]
    ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
rw :
  (∃ (n : ℤ), 2 * I * θ = (↑π : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔
    ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
⊢ cos θ = 0 ↔ ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm]

Premises used: Complex.exp_eq_exp_iff_exists_int, Complex.cos, mul_right_comm, Complex.exp_pi_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
⊢ (∃ (n : ℤ), 2 * I * θ = (↑π : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔
    ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
exists_congr fun x => ?_

Premises used: exists_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
refine :
  ∀ (x : ℤ),
    2 * I * θ = (↑π : ℂ) * I + (↑x : ℂ) * (2 * (↑π : ℂ) * I) ↔ θ = (HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) * (↑π : ℂ) / 2
⊢ (∃ (n : ℤ), 2 * I * θ = (↑π : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔
    ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
refine exists_congr fun x => ?_

Premises used: exists_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ 2 * I * θ = (↑π : ℂ) * I + (↑x : ℂ) * (2 * (↑π : ℂ) * I) ↔ θ = (HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
(iff_of_eq <| congr_arg _ ?_).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero)

Premises used: Complex.I_ne_zero, congr_arg, two_ne_zero, Iff.trans, mul_right_inj', mul_ne_zero, iff_of_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
refine : (↑π : ℂ) * I + (↑x : ℂ) * (2 * (↑π : ℂ) * I) = 2 * I * ((HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) * (↑π : ℂ) / 2)
⊢ 2 * I * θ = (↑π : ℂ) * I + (↑x : ℂ) * (2 * (↑π : ℂ) * I) ↔ θ = (HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
refine (iff_of_eq <| congr_arg _ ?_).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero)

Premises used: Complex.I_ne_zero, congr_arg, two_ne_zero, Iff.trans, mul_right_inj', mul_ne_zero, iff_of_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ (↑π : ℂ) * I + (↑x : ℂ) * (2 * (↑π : ℂ) * I) = 2 * I * ((HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) * (↑π : ℂ) / 2)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
contrapose! : cos θ = 0 ↔ ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
⊢ cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
contrapose!
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
⊢ cos θ = 0 ↔ ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
cos_eq_zero_iff

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

Tactic:
exact cos_eq_zero_iff

Premises used: Complex.cos_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
contrapose! : sin θ = 0 ↔ ∃ (k : ℤ), θ = (↑k : ℂ) * (↑π : ℂ)
⊢ sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (↑k : ℂ) * (↑π : ℂ)

Tactic:
contrapose!
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
⊢ sin θ = 0 ↔ ∃ (k : ℤ), θ = (↑k : ℂ) * (↑π : ℂ)

Tactic:
sin_eq_zero_iff

Premises used: Complex.sin_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
⊢ sin θ = 0 ↔ ∃ (k : ℤ), θ = (↑k : ℂ) * (↑π : ℂ)

Tactic:
exact sin_eq_zero_iff

Premises used: Complex.sin_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
rw : (∃ (k : ℤ), 2 * θ = (↑k : ℂ) * (↑π : ℂ)) ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 = θ
⊢ tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 = θ

Tactic:
rw [tan, div_eq_zero_iff, ← mul_eq_zero, ← mul_right_inj' two_ne_zero, mul_zero,
    ← mul_assoc, ← sin_two_mul, sin_eq_zero_iff]

Premises used: Complex.sin_eq_zero_iff, Complex.sin_two_mul, mul_assoc, mul_eq_zero, MulZeroClass.mul_zero, two_ne_zero, Complex.tan, mul_right_inj', div_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
⊢ (∃ (k : ℤ), 2 * θ = (↑k : ℂ) * (↑π : ℂ)) ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 = θ

Tactic:
simp [field, mul_comm, eq_comm]

Premises used: eq_comm, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
contrapose! : tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 = θ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 ≠ θ

Tactic:
contrapose!
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
⊢ tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 = θ

Tactic:
tan_eq_zero_iff

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

Tactic:
exact tan_eq_zero_iff

Premises used: Complex.tan_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
n w : ℤ
h : (↑n : ℂ) * (↑π : ℂ) / 2 = (↑n : ℂ) * (↑π : ℂ) / 2
⊢ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 = (↑n : ℂ) * (↑π : ℂ) / 2

Tactic:
use n
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
hθ : cos θ ≠ 0
simp : (∃ (k : ℤ), θ = (↑k : ℂ) * (↑π : ℂ)) ∨ False ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) = θ
⊢ tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) = θ

Tactic:
simp only [tan, hθ, div_eq_zero_iff, sin_eq_zero_iff]

Premises used: Complex.sin_eq_zero_iff, Complex.tan, div_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
θ : ℂ
hθ : cos θ ≠ 0
⊢ (∃ (k : ℤ), θ = (↑k : ℂ) * (↑π : ℂ)) ∨ False ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) = θ

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
rw rw₁ : -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0
⊢ cos x - cos y = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0

Tactic:
rw [cos_sub_cos]

Premises used: Complex.cos_sub_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
⊢ Ne (α := ℂ) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h₁ : sin ((x - y) / 2) = 0 ↔ ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x
h₂ : sin ((x + y) / 2) = 0 ↔ ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - x
⊢ sin ((x - y) / 2) = 0 ∨ sin ((x + y) / 2) = 0 ↔
    (∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x) ∨
      ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - x

Tactic:
apply or_congr

Premises used: or_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h₁ : (∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y) ↔ ∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + x
⊢ sin ((x - y) / 2) = 0 ↔ ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x

Tactic:
simp [field, sin_eq_zero_iff, eq_sub_iff_add_eq',
          sub_eq_iff_eq_add, mul_comm (2 : ℂ), mul_right_comm _ (2 : ℂ)]

Premises used: eq_sub_iff_add_eq', Complex.sin_eq_zero_iff, sub_eq_iff_eq_add, mul_right_comm, mul_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
⊢ sin ((x + y) / 2) = 0 ↔ ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - x

Tactic:
simp [field, sin_eq_zero_iff, eq_sub_iff_add_eq',
          sub_eq_iff_eq_add, mul_comm (2 : ℂ), mul_right_comm _ (2 : ℂ)]

Premises used: eq_sub_iff_add_eq', Complex.sin_eq_zero_iff, sub_eq_iff_eq_add, mul_right_comm, mul_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
h₁ : (∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y) → ∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + x
h₂ : (∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + x) → ∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y
⊢ (∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y) ↔ ∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + x

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
y : ℂ
k : ℤ
h : y = (↑(-k) : ℂ) * (↑π : ℂ) * 2 + ((↑k : ℂ) * (↑π : ℂ) * 2 + y)
⊢ ∃ (k_1 : ℤ), y = (↑k_1 : ℂ) * (↑π : ℂ) * 2 + ((↑k : ℂ) * (↑π : ℂ) * 2 + y)

Tactic:
use -k
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
y : ℂ
k : ℤ
⊢ y = (↑(-k) : ℂ) * (↑π : ℂ) * 2 + ((↑k : ℂ) * (↑π : ℂ) * 2 + y)

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

Tactic:
use -k
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
k : ℤ
⊢ x = (↑(-k) : ℂ) * (↑π : ℂ) * 2 + ((↑k : ℂ) * (↑π : ℂ) * 2 + x)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
simp :
  (∃ (k : ℤ),
      y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ∨
        y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2) ↔
    ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x ∨ y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x
⊢ sin x = sin y ↔
    ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x ∨ y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x

Tactic:
simp only [← Complex.cos_sub_pi_div_two, cos_eq_cos_iff, sub_eq_iff_eq_add]

Premises used: Complex.cos_sub_pi_div_two, sub_eq_iff_eq_add, Complex.cos_eq_cos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
⊢ (∃ (k : ℤ),
      y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ∨
        y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2) ↔
    ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x ∨ y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x

Tactic:
exists_congr fun k => or_congr ?_ ?_

Premises used: or_congr, exists_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
refine_1 :
  ∀ (k : ℤ),
    y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
      y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x
refine_2 :
  ∀ (k : ℤ),
    y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
      y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x
⊢ (∃ (k : ℤ),
      y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ∨
        y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2) ↔
    ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x ∨ y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x

Tactic:
refine exists_congr fun k => or_congr ?_ ?_

Premises used: or_congr, exists_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
k : ℤ
⊢ y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
    y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x

Tactic:
Eq.congr rfl ?_

Premises used: Eq.congr, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
k : ℤ
refine_1 :
  HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 =
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x
⊢ y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
    y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x

Tactic:
refine Eq.congr rfl ?_

Premises used: Eq.congr, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
k : ℤ
⊢ y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
    y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x

Tactic:
Eq.congr rfl ?_

Premises used: Eq.congr, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
k : ℤ
refine_2 :
  HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 =
    (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x
⊢ y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
    y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x

Tactic:
refine Eq.congr rfl ?_

Premises used: Eq.congr, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
k : ℤ
refine_1 :
  HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑k : ℂ) * (↑π : ℂ) + (2 * x - (↑π : ℂ)) + (↑π : ℂ) =
    2 * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x)
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 =
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
k : ℤ
refine_2 :
  HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑k : ℂ) * (↑π : ℂ) - (2 * x - (↑π : ℂ)) + (↑π : ℂ) =
    2 * ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) - x)
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 =
    (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
k : ℤ
⊢ HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑k : ℂ) * (↑π : ℂ) + (2 * x - (↑π : ℂ)) + (↑π : ℂ) =
    2 * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x y : ℂ
k : ℤ
⊢ HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑k : ℂ) * (↑π : ℂ) - (2 * x - (↑π : ℂ)) + (↑π : ℂ) =
    2 * ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) - x)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
rw :
  (∃ (k : ℤ), x = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + 0 ∨ x = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - 0) ↔
    ∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x
⊢ cos x = 1 ↔ ∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x

Tactic:
rw [← cos_zero, eq_comm, cos_eq_cos_iff]

Premises used: eq_comm, Complex.cos_zero, Complex.cos_eq_cos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
⊢ (∃ (k : ℤ), x = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + 0 ∨ x = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - 0) ↔
    ∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x

Tactic:
simp [mul_assoc, mul_left_comm, eq_comm]

Premises used: mul_assoc, mul_left_comm, eq_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
rw : (∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x - (↑π : ℂ)) ↔ ∃ (k : ℤ), (↑π : ℂ) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x
⊢ cos x = -1 ↔ ∃ (k : ℤ), (↑π : ℂ) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x

Tactic:
rw [← neg_eq_iff_eq_neg, ← cos_sub_pi, cos_eq_one_iff]

Premises used: Complex.cos_sub_pi, Complex.cos_eq_one_iff, neg_eq_iff_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
⊢ (∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x - (↑π : ℂ)) ↔ ∃ (k : ℤ), (↑π : ℂ) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x

Tactic:
simp only [eq_sub_iff_add_eq']

Premises used: eq_sub_iff_add_eq'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
rw : (∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x - (↑π : ℂ) / 2) ↔ ∃ (k : ℤ), (↑π : ℂ) / 2 + (↑k : ℂ) * (2 * (↑π : ℂ)) = x
⊢ sin x = 1 ↔ ∃ (k : ℤ), (↑π : ℂ) / 2 + (↑k : ℂ) * (2 * (↑π : ℂ)) = x

Tactic:
rw [← cos_sub_pi_div_two, cos_eq_one_iff]

Premises used: Complex.cos_eq_one_iff, Complex.cos_sub_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
⊢ (∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x - (↑π : ℂ) / 2) ↔ ∃ (k : ℤ), (↑π : ℂ) / 2 + (↑k : ℂ) * (2 * (↑π : ℂ)) = x

Tactic:
simp only [eq_sub_iff_add_eq']

Premises used: eq_sub_iff_add_eq'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
rw :
  (∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x + (↑π : ℂ) / 2) ↔ ∃ (k : ℤ), -((↑π : ℂ) / 2) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x
⊢ sin x = -1 ↔ ∃ (k : ℤ), -((↑π : ℂ) / 2) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x

Tactic:
rw [← neg_eq_iff_eq_neg, ← cos_add_pi_div_two, cos_eq_one_iff]

Premises used: Complex.cos_eq_one_iff, neg_eq_iff_eq_neg, Complex.cos_add_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℂ
⊢ (∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x + (↑π : ℂ) / 2) ↔ ∃ (k : ℤ), -((↑π : ℂ) / 2) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x

Tactic:
simp only [← sub_eq_neg_add, sub_eq_iff_eq_add]

Premises used: sub_eq_neg_add, sub_eq_iff_eq_add
-- 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 :
  ∀ (h1 : ∀ (k : ℤ), x ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2)
    (h2 : ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2),
    tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
inr :
  ∀ (k l : ℤ),
    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))
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Tactic:
rcases h with (⟨h1, h2⟩ | ⟨⟨k, rfl⟩, ⟨l, rfl⟩⟩)

Premises used: rfl