awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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 : ℤ)))
⊢ 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))
have 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)
Tactic: refine Finset.sum_le_sum (fun i hi => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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
⊢ |HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval x i)| ≤
    HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval 1 i)
have 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)
Tactic: obtain ⟨m, hm, hi⟩ := (Set.mem_image ..).mp (hfsupp hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema (goal)
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]) → ℕ) i : ℕ) (eval x i)| ≤
    HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) i : ℕ) (eval 1 i)
have grw : HSMul.hSMul (α := ℕ) (β := ℝ) ((f : (a : ℝ[X]) → ℕ) (T ℝ (↑m : ℤ)) : ℕ) 1 ≤
  HSMul.hSMul (α := ℕ) ((f : (a : ℝ[X]) → ℕ) (T ℝ (↑m : ℤ)) : ℕ) (eval 1 (T ℝ (↑m : ℤ)))
Tactic: grw [abs_nsmul, ← hi, abs_eval_T_real_le_one m hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
θ : ℂ
⊢ (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
have rw : cexp (θ * I - -θ * I) = -1 ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
Goal:
θ : ℂ
⊢ cos θ = 0 ↔ ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
have h : (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
⊢ cos θ = 0 ↔ ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
have rw : (∃ (n : ℤ), 2 * I * θ = (↑π : ℂ) * I + (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔
  ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
Tactic: rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
have refine : ∀ (x : ℤ),
  2 * I * θ = (↑π : ℂ) * I + (↑x : ℂ) * (2 * (↑π : ℂ) * I) ↔ θ = (HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) * (↑π : ℂ) / 2
Tactic: refine exists_congr fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
have refine : (↑π : ℂ) * I + (↑x : ℂ) * (2 * (↑π : ℂ) * I) = 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
θ : ℂ
⊢ cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
have contrapose! : cos θ = 0 ↔ ∃ (k : ℤ), θ = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
θ : ℂ
⊢ sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (↑k : ℂ) * (↑π : ℂ)
have contrapose! : sin θ = 0 ↔ ∃ (k : ℤ), θ = (↑k : ℂ) * (↑π : ℂ)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
θ : ℂ
⊢ tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 = θ
have rw : (∃ (k : ℤ), 2 * θ = (↑k : ℂ) * (↑π : ℂ)) ↔ ∃ (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
θ : ℂ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 ≠ θ
have contrapose! : tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 = θ
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
n w : ℤ
⊢ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) / 2 = (↑n : ℂ) * (↑π : ℂ) / 2
have h : (↑n : ℂ) * (↑π : ℂ) / 2 = (↑n : ℂ) * (↑π : ℂ) / 2
Tactic: use n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
θ : ℂ
hθ : cos θ ≠ 0
⊢ tan θ = 0 ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) = θ
have simp : (∃ (k : ℤ), θ = (↑k : ℂ) * (↑π : ℂ)) ∨ False ↔ ∃ (k : ℤ), (↑k : ℂ) * (↑π : ℂ) = θ
Tactic: simp only [tan, hθ, div_eq_zero_iff, sin_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
⊢ cos x - cos y = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0
have rw : -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0
Tactic: rw [cos_sub_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
⊢ sin ((x - y) / 2) = 0 ∨ sin ((x + y) / 2) = 0 ↔
    (∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x) ∨
      ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - x
have h₁ : sin ((x - y) / 2) = 0 ↔ ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x
Tactic: apply or_congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
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
have h₂ : sin ((x + y) / 2) = 0 ↔ ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - x
Tactic: apply or_congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
⊢ sin ((x - y) / 2) = 0 ↔ ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x
have h₁ : (∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y) ↔ ∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + 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 : ℂ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
⊢ (∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y) ↔ ∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + x
have h₁ : (∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y) → ∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
h₁ : (∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y) → ∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + x
⊢ (∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y) ↔ ∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + x
have h₂ : (∃ (k : ℤ), y = (↑k : ℂ) * (↑π : ℂ) * 2 + x) → ∃ (k : ℤ), x = (↑k : ℂ) * (↑π : ℂ) * 2 + y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
y : ℂ
k : ℤ
⊢ ∃ (k_1 : ℤ), y = (↑k_1 : ℂ) * (↑π : ℂ) * 2 + ((↑k : ℂ) * (↑π : ℂ) * 2 + y)
have h : y = (↑(-k) : ℂ) * (↑π : ℂ) * 2 + ((↑k : ℂ) * (↑π : ℂ) * 2 + y)
Tactic: use -k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
k : ℤ
⊢ ∃ (k_1 : ℤ), x = (↑k_1 : ℂ) * (↑π : ℂ) * 2 + ((↑k : ℂ) * (↑π : ℂ) * 2 + x)
have h : x = (↑(-k) : ℂ) * (↑π : ℂ) * 2 + ((↑k : ℂ) * (↑π : ℂ) * 2 + x)
Tactic: use -k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
⊢ sin x = sin y ↔
    ∃ (k : ℤ), y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x ∨ y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x
have 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
Tactic: simp only [← Complex.cos_sub_pi_div_two, cos_eq_cos_iff, sub_eq_iff_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
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
have refine_1 : ∀ (k : ℤ),
  y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
    y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x
Tactic: refine exists_congr fun k => or_congr ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
refine_1 :
  ∀ (k : ℤ),
    y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
      y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + 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
have refine_2 : ∀ (k : ℤ),
  y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
    y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x
Tactic: refine exists_congr fun k => or_congr ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
k : ℤ
⊢ y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
    y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x
have refine_1 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 =
  HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x
Tactic: refine Eq.congr rfl ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
k : ℤ
⊢ y = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 ↔
    y = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x
have refine_2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 =
  (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x
Tactic: refine Eq.congr rfl ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
k : ℤ
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 =
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x
have refine_1 : HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑k : ℂ) * (↑π : ℂ) + (2 * x - (↑π : ℂ)) + (↑π : ℂ) =
  2 * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + x)
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
k : ℤ
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - (x - (↑π : ℂ) / 2) + (↑π : ℂ) / 2 =
    (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) - x
have refine_2 : HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑k : ℂ) * (↑π : ℂ) - (2 * x - (↑π : ℂ)) + (↑π : ℂ) =
  2 * ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) - x)
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ cos x = 1 ↔ ∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x
have rw : (∃ (k : ℤ), x = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) + 0 ∨ x = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * (↑π : ℂ) - 0) ↔
  ∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x
Tactic: rw [← cos_zero, eq_comm, cos_eq_cos_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ cos x = -1 ↔ ∃ (k : ℤ), (↑π : ℂ) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x
have rw : (∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x - (↑π : ℂ)) ↔ ∃ (k : ℤ), (↑π : ℂ) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x
Tactic: rw [← neg_eq_iff_eq_neg, ← cos_sub_pi, cos_eq_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ sin x = 1 ↔ ∃ (k : ℤ), (↑π : ℂ) / 2 + (↑k : ℂ) * (2 * (↑π : ℂ)) = x
have rw : (∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x - (↑π : ℂ) / 2) ↔ ∃ (k : ℤ), (↑π : ℂ) / 2 + (↑k : ℂ) * (2 * (↑π : ℂ)) = x
Tactic: rw [← cos_sub_pi_div_two, cos_eq_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x : ℂ
⊢ sin x = -1 ↔ ∃ (k : ℤ), -((↑π : ℂ) / 2) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x
have rw : (∃ (k : ℤ), (↑k : ℂ) * (2 * (↑π : ℂ)) = x + (↑π : ℂ) / 2) ↔ ∃ (k : ℤ), -((↑π : ℂ) / 2) + (↑k : ℂ) * (2 * (↑π : ℂ)) = x
Tactic: rw [← neg_eq_iff_eq_neg, ← cos_add_pi_div_two, cos_eq_one_iff]
-- 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
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
have 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)
Tactic: rcases h with (⟨h1, h2⟩ | ⟨⟨k, rfl⟩, ⟨l, rfl⟩⟩)
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 :
  ∀ (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)
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
have 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))
Tactic: rcases h with (⟨h1, h2⟩ | ⟨⟨k, rfl⟩, ⟨l, rfl⟩⟩)
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (goal)
Goal:
x y : ℂ
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)
have inl : (sin x * cos y / (cos x * cos y) + cos x * sin y / (cos x * cos y)) /
    (cos x * cos y / (cos x * cos y) - sin x * sin y / (cos x * cos y)) =
  (tan x + tan y) / (1 - tan x * tan y)
Tactic: rw [tan, sin_add, cos_add, ←
      div_div_div_cancel_right₀ (mul_ne_zero (cos_ne_zero_iff.mpr h1) (cos_ne_zero_iff.mpr h2)),
      add_div, sub_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
Goal:
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))
have t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
Tactic: haveI t := tan_int_mul_pi_div_two
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 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 hx : tan ((↑(2 * k + 1) : ℂ) * (↑π : ℂ) / 2) = 0
Tactic: obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
hx : tan ((↑(2 * k + 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 hy : tan ((↑(2 * l + 1) : ℂ) * (↑π : ℂ) / 2) = 0
Tactic: obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
hx : tan ((↑(2 * k + 1) : ℂ) * (↑π : ℂ) / 2) = 0
hy : tan ((↑(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 hxy : tan ((↑(2 * k + 1 + (2 * l + 1)) : ℂ) * (↑π : ℂ) / 2) = 0
Tactic: obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
hx : tan ((↑(2 * k + 1) : ℂ) * (↑π : ℂ) / 2) = 0
hy : tan ((↑(2 * l + 1) : ℂ) * (↑π : ℂ) / 2) = 0
hxy : tan ((↑(2 * k + 1 + (2 * l + 1)) : ℂ) * (↑π : ℂ) / 2) = 0
⊢ tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2 + (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 hx₁ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) = 0
Tactic: simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one] at hx hy hxy
Cleared hypotheses: hx, hy, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
hx : tan ((↑(2 * k + 1) : ℂ) * (↑π : ℂ) / 2) = 0
hy : tan ((↑(2 * l + 1) : ℂ) * (↑π : ℂ) / 2) = 0
hxy : tan ((↑(2 * k + 1 + (2 * l + 1)) : ℂ) * (↑π : ℂ) / 2) = 0
hx₁ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) = 0
⊢ tan ((HMul.hMul (α := ℂ) 2 (↑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 hy₁ : tan ((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = 0
Tactic: simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one] at hx hy hxy
Cleared hypotheses: hx, hy, hxy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (hypothesis)
Goal:
k l : ℤ
t : ∀ (n : ℤ), tan ((↑n : ℂ) * (↑π : ℂ) / 2) = 0
hx : tan ((↑(2 * k + 1) : ℂ) * (↑π : ℂ) / 2) = 0
hy : tan ((↑(2 * l + 1) : ℂ) * (↑π : ℂ) / 2) = 0
hxy : tan ((↑(2 * k + 1 + (2 * l + 1)) : ℂ) * (↑π : ℂ) / 2) = 0
hx₁ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) = 0
hy₁ : tan ((HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) = 0
⊢ tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 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 hxy₁ : tan ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 + (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1)) * (↑π : ℂ) / 2) = 0
Tactic: simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one] at hx hy hxy
Cleared hypotheses: hx, hy, hxy