awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n

Tactic:
exact Nat.emultiplicity_pow_add_pow hp.out hp1 hxy hx hn

Premises used: Nat.emultiplicity_pow_add_pow, Fact.out
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ n ≠ 0

Tactic:
(Odd.pos hn).ne'

Premises used: Odd.pos, LT.lt.ne'
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ n ≠ 0

Tactic:
exact (Odd.pos hn).ne'

Premises used: Odd.pos, LT.lt.ne'
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x + (y + 1) ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x ^ n + (y + 1) ^ n ≠ 0

Tactic:
(Nat.lt_add_left _ (pow_pos y.succ_pos _)).ne'

Premises used: pow_pos, LT.lt.ne', Nat.succ_pos, Nat.lt_add_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x ^ n + (y + 1) ^ n ≠ 0

Tactic:
exact (Nat.lt_add_left _ (pow_pos y.succ_pos _)).ne'

Premises used: pow_pos, LT.lt.ne', Nat.succ_pos, Nat.lt_add_left
-- Module: Mathlib.NumberTheory.Niven
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
q : ℚ
⊢ IsIntegral.{0, u_1} ℤ (A := α) (↑q : α) ↔ IsIntegral ℤ q

Tactic:
isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective ℚ α)

Premises used: Rat, isIntegral_algebraMap_iff, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.NumberTheory.Niven
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
x : α
h₁ : IsIntegral ℤ x
h_1 : ∃ (k : ℤ), x = (↑k : α)
w : ℤ
h : x = (↑w : α)
⊢ x = (↑(↑w : ℚ) : α)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Niven
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
x : α
h₁ : IsIntegral ℤ x
refine : (∃ (q : ℚ), x = (↑q : α)) → ∃ (k : ℤ), x = (↑k : α)
⊢ (∃ (q : ℚ), x = (↑q : α)) ↔ ∃ (k : ℤ), x = (↑k : α)

Tactic:
refine ⟨?_, fun ⟨w, h⟩ ↦ ⟨w, by simp [h]⟩⟩
-- Module: Mathlib.NumberTheory.Niven
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
q : ℚ
h₁ : IsIntegral.{0, u_1} ℤ (A := α) (↑q : α)
⊢ IsIntegral ℤ q

Tactic:
rw [ratCast_iff] at h₁

Premises used: IsIntegral.ratCast_iff
-- Module: Mathlib.NumberTheory.Niven
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
q : ℚ
h₁ : IsIntegral ℤ q
h : ∀ (k : ℤ) (h : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) k = q), Eq.{u_1 + 1} (α := α) (↑q : α) (↑k : α)
⊢ ∃ (k : ℤ), Eq.{u_1 + 1} (α := α) (↑q : α) (↑k : α)

Tactic:
peel IsIntegrallyClosed.algebraMap_eq_of_integral h₁ with h

Premises used: IsIntegrallyClosed.algebraMap_eq_of_integral
-- Module: Mathlib.NumberTheory.Niven
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
q : ℚ
h₁ : IsIntegral ℤ q
k : ℤ
h : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) k = q
⊢ Eq.{u_1 + 1} (α := α) (↑q : α) (↑k : α)

Tactic:
simp [← h]
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
nth_rw : cexp ((↑(2 * q.den) : ℂ) * ((↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)) : ℂ) * (↑π : ℂ) * I)) = 1
⊢ cexp ((↑q : ℂ) * (↑π : ℂ) * I) ^ (2 * q.den) = 1

Tactic:
nth_rw 1 [← q.num_div_den, ← exp_nat_mul]

Premises used: Rat.num_div_den, Complex.exp_nat_mul
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
push_cast : cexp (HMul.hMul (α := ℂ) 2 (↑q.den : ℂ) * (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ) * (↑π : ℂ) * I)) = 1
⊢ cexp ((↑(2 * q.den) : ℂ) * ((↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)) : ℂ) * (↑π : ℂ) * I)) = 1

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ HMul.hMul (α := ℂ) 2 (↑q.den : ℂ) * (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ) * (↑π : ℂ) * I) =
    (↑q.num : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
field
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
rw : cexp ((↑q.num : ℂ) * (2 * (↑π : ℂ) * I)) = 1
rw₁ rw₂ : Eq (α := ℂ) 1 1
⊢ cexp (HMul.hMul (α := ℂ) 2 (↑q.den : ℂ) * (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ) * (↑π : ℂ) * I)) = 1

Tactic:
rw [show 2 * q.den * (q.num / q.den * π * I) = q.num * (2 * π * I) by field,
    exp_int_mul_two_pi_mul_I]

Premises used: Complex.exp_int_mul_two_pi_mul_I
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I))

Tactic:
.of_pow (Nat.mul_pos zero_lt_two q.den_pos) ?_

Premises used: IsIntegral.of_pow, Nat.mul_pos, Rat.den_pos, zero_lt_two
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
refine : IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I) ^ (2 * q.den))
⊢ IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I))

Tactic:
refine .of_pow (Nat.mul_pos zero_lt_two q.den_pos) ?_
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I) ^ (2 * q.den))

Tactic:
exp_rat_mul_pi_mul_I_pow_two_mul_den _ ▸ isIntegral_one

Premises used: Eq.rec, isIntegral_one, Complex.exp_rat_mul_pi_mul_I_pow_two_mul_den, Eq.symm
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I) ^ (2 * q.den))

Tactic:
exact exp_rat_mul_pi_mul_I_pow_two_mul_den _ ▸ isIntegral_one
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ (cexp (-((↑q : ℂ) * (↑π : ℂ)) * I))

Tactic:
simpa using isIntegral_exp_rat_mul_pi_mul_I (-q)

Premises used: Complex.isIntegral_exp_rat_mul_pi_mul_I, Neg.neg
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
rw : IsIntegral ℤ ((cexp (-((↑q : ℂ) * (↑π : ℂ)) * I) - cexp ((↑q : ℂ) * (↑π : ℂ) * I)) * I)
⊢ IsIntegral ℤ (2 * sin ((↑q : ℂ) * (↑π : ℂ)))

Tactic:
rw [sin.eq_1, mul_div_cancel₀ _ two_ne_zero]

Premises used: mul_div_cancel₀, two_ne_zero, Complex.sin.eq_1
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ ((cexp (-((↑q : ℂ) * (↑π : ℂ)) * I) - cexp ((↑q : ℂ) * (↑π : ℂ) * I)) * I)

Tactic:
(isIntegral_exp_neg_rat_mul_pi_mul_I q).sub (isIntegral_exp_rat_mul_pi_mul_I q)
    |>.mul isIntegral_int_I

Premises used: IsIntegral.mul, Complex.isIntegral_exp_rat_mul_pi_mul_I, IsIntegral.sub, Complex.isIntegral_exp_neg_rat_mul_pi_mul_I, Complex.isIntegral_int_I
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ ((cexp (-((↑q : ℂ) * (↑π : ℂ)) * I) - cexp ((↑q : ℂ) * (↑π : ℂ) * I)) * I)

Tactic:
exact (isIntegral_exp_neg_rat_mul_pi_mul_I q).sub (isIntegral_exp_rat_mul_pi_mul_I q)
    |>.mul isIntegral_int_I

Premises used: IsIntegral.mul, Complex.isIntegral_exp_rat_mul_pi_mul_I, IsIntegral.sub, Complex.isIntegral_exp_neg_rat_mul_pi_mul_I, Complex.isIntegral_int_I
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
rw : IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I) + cexp (-((↑q : ℂ) * (↑π : ℂ)) * I))
⊢ IsIntegral ℤ (2 * cos ((↑q : ℂ) * (↑π : ℂ)))

Tactic:
rw [cos.eq_1, mul_div_cancel₀ _ two_ne_zero]

Premises used: Complex.cos.eq_1, mul_div_cancel₀, two_ne_zero
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I) + cexp (-((↑q : ℂ) * (↑π : ℂ)) * I))

Tactic:
(isIntegral_exp_rat_mul_pi_mul_I q).add (isIntegral_exp_neg_rat_mul_pi_mul_I q)

Premises used: Complex.isIntegral_exp_rat_mul_pi_mul_I, IsIntegral.add, Complex.isIntegral_exp_neg_rat_mul_pi_mul_I
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I) + cexp (-((↑q : ℂ) * (↑π : ℂ)) * I))

Tactic:
exact (isIntegral_exp_rat_mul_pi_mul_I q).add (isIntegral_exp_neg_rat_mul_pi_mul_I q)

Premises used: Complex.isIntegral_exp_rat_mul_pi_mul_I, IsIntegral.add, Complex.isIntegral_exp_neg_rat_mul_pi_mul_I
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ Membership.mem (α := ℂ) (γ := Submonoid ℂ) (nonZeroDivisors ℂ) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) (↑2 : ℤ) : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsAlgebraic ℤ (tan ((↑q : ℂ) * (↑π : ℂ)))

Tactic:
(isAlgebraic_sin_rat_mul_pi q).mul (isAlgebraic_cos_rat_mul_pi q).inv

Premises used: IsAlgebraic.inv, Complex.isAlgebraic_sin_rat_mul_pi, DivInvMonoid.div', Complex.tan, IsAlgebraic.mul, Complex.isAlgebraic_cos_rat_mul_pi
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ (A := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) (2 * sin ((↑q : ℝ) * π)) : ℂ)

Tactic:
simp [Complex.isIntegral_two_mul_sin_rat_mul_pi]

Premises used: Complex.isIntegral_two_mul_sin_rat_mul_pi
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsIntegral ℤ (A := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) (2 * cos ((↑q : ℝ) * π)) : ℂ)

Tactic:
simp [Complex.isIntegral_two_mul_cos_rat_mul_pi]

Premises used: Complex.isIntegral_two_mul_cos_rat_mul_pi
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ Membership.mem (α := ℝ) (γ := Submonoid ℝ) (nonZeroDivisors ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (↑2 : ℤ) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Niven
Goal:
q : ℚ
⊢ IsAlgebraic ℤ (A := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) (tan ((↑q : ℝ) * π)) : ℂ)

Tactic:
simp [Complex.isAlgebraic_tan_rat_mul_pi]

Premises used: Complex.isAlgebraic_tan_rat_mul_pi
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
obtain :
  ∀ (r : ℚ) (hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)),
    Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos ((↑r : ℝ) * π))
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos θ)

Tactic:
obtain ⟨r, rfl⟩ := hθ

Premises used: rfl
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
rw : ∃ (q : ℚ), 2 * cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ ∃ (k : ℤ), 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)

Tactic:
rw [← (Real.isIntegral_two_mul_cos_rat_mul_pi r).exists_int_iff_exists_rat]

Premises used: Real.isIntegral_two_mul_cos_rat_mul_pi, IsIntegral.exists_int_iff_exists_rat
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
push_cast :
  2 * cos ((↑r : ℝ) * π) = HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)
⊢ 2 * cos ((↑r : ℝ) * π) = (↑(2 * hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
linarith :
  2 * cos ((↑r : ℝ) * π) <
      HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ) →
    2 * cos ((↑r : ℝ) * π) -
          HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ) +
        2 * -(cos ((↑r : ℝ) * π) - (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)) =
      0
linarith₁ :
  2 * cos ((↑r : ℝ) * π) <
      HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ) →
    GT.gt (α := ℝ) 2 0
linarith₂ :
  HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ) <
      2 * cos ((↑r : ℝ) * π) →
    HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ) -
          2 * cos ((↑r : ℝ) * π) +
        2 * (cos ((↑r : ℝ) * π) - (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)) =
      0
linarith₃ :
  HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ) <
      2 * cos ((↑r : ℝ) * π) →
    GT.gt (α := ℝ) 2 0
⊢ 2 * cos ((↑r : ℝ) * π) = HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)

Tactic:
linarith [hcos.choose_spec]

Premises used: Exists.choose_spec
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ ∃ (q : ℚ), 2 * cos ((↑r : ℝ) * π) = (↑q : ℝ)

Tactic:
exact ⟨2 * hcos.choose, by push_cast; linarith [hcos.choose_spec]⟩
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
obtain :
  ∀ (k : ℤ) (hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)),
    Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos ((↑r : ℝ) * π))
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos ((↑r : ℝ) * π))

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℤ, 2 * cos (r * π) = k := by
    rw [← (Real.isIntegral_two_mul_cos_rat_mul_pi r).exists_int_iff_exists_rat]
    exact ⟨2 * hcos.choose, by push_cast; linarith [hcos.choose_spec]⟩

Premises used: Real.pi, HMul.hMul, Real.cos, Rat.cast
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
rw : -2 ≤ k ∧ k ≤ 2
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc (-2) 2) k

Tactic:
rw [Finset.mem_Icc]

Premises used: Finset.mem_Icc
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
rify : LE.le (α := ℝ) (-2) (↑k : ℝ) ∧ LE.le (α := ℝ) (↑k : ℝ) 2
⊢ -2 ≤ k ∧ k ≤ 2

Tactic:
rify
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
left : LE.le (α := ℝ) (-2) (↑k : ℝ)
right : LE.le (α := ℝ) (↑k : ℝ) 2
⊢ LE.le (α := ℝ) (-2) (↑k : ℝ) ∧ LE.le (α := ℝ) (↑k : ℝ) 2

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
linarith :
  LT.lt (α := ℝ) (↑k : ℝ) (-2) →
    2 * cos ((↑r : ℝ) * π) - (↑k : ℝ) + HSub.hSub (α := ℝ) (↑k : ℝ) (-2) + 2 * (-1 - cos ((↑r : ℝ) * π)) = 0
linarith₁ : LT.lt (α := ℝ) (↑k : ℝ) (-2) → GT.gt (α := ℝ) 2 0
⊢ LE.le (α := ℝ) (-2) (↑k : ℝ)

Tactic:
linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]

Premises used: Real.pi, HMul.hMul, Rat.cast, Real.neg_one_le_cos, Real.cos_le_one
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
linarith :
  LT.lt (α := ℝ) 2 (↑k : ℝ) →
    -(2 * cos ((↑r : ℝ) * π) - (↑k : ℝ)) + HSub.hSub (α := ℝ) 2 (↑k : ℝ) + 2 * (cos ((↑r : ℝ) * π) - 1) = 0
linarith₁ : LT.lt (α := ℝ) 2 (↑k : ℝ) → GT.gt (α := ℝ) 2 0
⊢ LE.le (α := ℝ) (↑k : ℝ) 2

Tactic:
linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]

Premises used: Real.pi, HMul.hMul, Rat.cast, Real.neg_one_le_cos, Real.cos_le_one
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc (-2) 2) k

Tactic:
have hk_values : k ∈ Finset.Icc (-2 : ℤ) 2 := by
    rw [Finset.mem_Icc]
    rify
    constructor <;> linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
hk_values : Membership.mem (γ := Finset ℤ) (Finset.Icc (-2) 2) k
⊢ cos ((↑r : ℝ) * π) = HDiv.hDiv (α := ℝ) (↑k : ℝ) 2

Tactic:
grind
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
hk_values : Membership.mem (γ := Finset ℤ) (Finset.Icc (-2) 2) k
rw : Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos ((↑r : ℝ) * π))

Tactic:
rw [show cos (r * π) = k / 2 by grind]
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
hk_values : Membership.mem (γ := Finset ℤ) (Finset.Icc (-2) 2) k
0 :
  ∀
    (hk :
      2 * cos ((↑r : ℝ) * π) =
        (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 0) : ℝ)),
    Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
      (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 0) : ℝ)
        2)
1 :
  ∀
    (hk :
      2 * cos ((↑r : ℝ) * π) =
        (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 1) : ℝ)),
    Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
      (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 1) : ℝ)
        2)
2 :
  ∀
    (hk :
      2 * cos ((↑r : ℝ) * π) =
        (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 2) : ℝ)),
    Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
      (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 2) : ℝ)
        2)
3 :
  ∀
    (hk :
      2 * cos ((↑r : ℝ) * π) =
        (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 3) : ℝ)),
    Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
      (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 3) : ℝ)
        2)
4 :
  ∀
    (hk :
      2 * cos ((↑r : ℝ) * π) =
        (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 4) : ℝ)),
    Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
      (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 4) : ℝ)
        2)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)

Tactic:
fin_cases hk_values
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hk :
  2 * cos ((↑r : ℝ) * π) = (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 0) : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
    (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 0) : ℝ) 2)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hk :
  2 * cos ((↑r : ℝ) * π) = (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 1) : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
    (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 1) : ℝ) 2)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hk :
  2 * cos ((↑r : ℝ) * π) = (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 2) : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
    (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 2) : ℝ) 2)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hk :
  2 * cos ((↑r : ℝ) * π) = (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 3) : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
    (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 3) : ℝ) 2)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hk :
  2 * cos ((↑r : ℝ) * π) = (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 4) : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1}
    (HDiv.hDiv (α := ℝ) (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-2)) : (a : ℕ) → ℤ) 4) : ℝ) 2)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos (θ - π / 2))

Tactic:
niven (θ := θ - π / 2) ?_ ?_

Premises used: niven
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
h : cos (θ - π / 2) = sin θ
convert_1 : ∃ (r : ℚ), θ - π / 2 = (↑r : ℝ) * π
convert_2 : ∃ (q : ℚ), cos (θ - π / 2) = (↑q : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (sin θ)

Tactic:
convert! ← niven (θ := θ - π / 2) ?_ ?_ using 1

Premises used: niven
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
⊢ cos (θ - π / 2) = sin θ

Tactic:
cos_sub_pi_div_two θ

Premises used: Real.cos_sub_pi_div_two
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
⊢ cos (θ - π / 2) = sin θ

Tactic:
exact cos_sub_pi_div_two θ

Premises used: Real.cos_sub_pi_div_two
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
a : ℚ
h : θ = (↑a : ℝ) * π
push_cast : θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
⊢ θ - π / 2 = (↑((fun (x : ℚ) ↦ x - 1 / 2) a) : ℝ) * π

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
a : ℚ
h : θ = (↑a : ℝ) * π
linarith : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → 2 / 2 = 1
linarith₁ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → 2 / 2 = 1
linarith₃ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → HMul.hMul (α := ℝ) 2 1 = 2
linarith₅ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → GT.gt (α := ℝ) 2 0
linarith₆ :
  θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π →
    2 * -(θ - (↑a : ℝ) * π) + (2 * θ - 1 * π - (HMul.hMul (α := ℝ) 2 (↑a : ℝ) - HMul.hMul (α := ℝ) 1 1) * (1 * π)) = 0
linarith₇ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → GT.gt (α := ℝ) 2 0
linarith₈ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → 2 / 2 = 1
linarith₉ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₀ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₁ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → 2 / 2 = 1
linarith₁₂ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → GT.gt (α := ℝ) 2 0
linarith₁₄ :
  ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 →
    2 * (θ - (↑a : ℝ) * π) + ((HMul.hMul (α := ℝ) 2 (↑a : ℝ) - HMul.hMul (α := ℝ) 1 1) * (1 * π) - (2 * θ - 1 * π)) = 0
linarith₁₅ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → GT.gt (α := ℝ) 2 0
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
⊢ ∃ (r : ℚ), θ - π / 2 = (↑r : ℝ) * π

Tactic:
exact hθ.imp' (· - 1 / 2) (by intros; push_cast; linarith)

Premises used: HSub.hSub, HDiv.hDiv, Exists.imp', OfNat.ofNat
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
⊢ ∃ (q : ℚ), cos (θ - π / 2) = (↑q : ℝ)

Tactic:
simpa [cos_sub_pi_div_two]

Premises used: Real.cos_sub_pi_div_two
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
inl : ∀ (h : cos θ = -1), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
inr : ∀ (h : cos θ = -1 / 2), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
inr₁ : ∀ (h : cos θ = 0), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
inr₂ : ∀ (h : cos θ = 1 / 2), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
inr₃ : ∀ (h : Membership.mem (γ := Set ℝ) {1} (cos θ)), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ

Tactic:
rcases niven hθ hcos with h | h | h | h | h

Premises used: niven
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1
⊢ cos π = -1

Tactic:
have h₂ := cos_pi
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
⊢ cos (π - π / 3) = -cos (π / 3)

Tactic:
have := cos_pi_sub (π / 3)