awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + (↑(padicValNat p n) : ℕ∞)
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have succ₁ : x + (y + 1) ≠ 0
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
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)) + (↑(padicValNat p n) : ℕ∞)
have succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + (↑(padicValNat p n) : ℕ∞)
have succ₁ : n ≠ 0
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n
Tactic: iterate 3 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n
⊢ (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have succ₁ : n ≠ 0
Tactic: iterate 3 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n
succ₁ : n ≠ 0
⊢ (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have succ₂ : x + (y + 1) ≠ 0
Tactic: iterate 3 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n
succ₁ : n ≠ 0
succ₂ : x + (y + 1) ≠ 0
⊢ (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have succ₃ : x ^ n + (y + 1) ^ n ≠ 0
Tactic: iterate 3 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
x : α
h₁ : IsIntegral ℤ x
⊢ (∃ (q : ℚ), x = (↑q : α)) ↔ ∃ (k : ℤ), x = (↑k : α)
have refine : (∃ (q : ℚ), x = (↑q : α)) → ∃ (k : ℤ), x = (↑k : α)
Tactic: refine ⟨?_, fun ⟨w, h⟩ ↦ ⟨w, by simp [h]⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
q : ℚ
h₁ : IsIntegral.{0, u_1} ℤ (A := α) (↑q : α)
⊢ ∃ (k : ℤ), Eq.{u_1 + 1} (α := α) (↑q : α) (↑k : α)
have h₂ : IsIntegral ℤ q
Tactic: rw [ratCast_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
q : ℚ
h₁ : IsIntegral ℤ q
⊢ ∃ (k : ℤ), Eq.{u_1 + 1} (α := α) (↑q : α) (↑k : α)
have h : ∀ (k : ℤ) (h : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) k = q), Eq.{u_1 + 1} (α := α) (↑q : α) (↑k : α)
Tactic: peel IsIntegrallyClosed.algebraMap_eq_of_integral h₁ with h
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
q : ℚ
⊢ cexp ((↑q : ℂ) * (↑π : ℂ) * I) ^ (2 * q.den) = 1
have nth_rw : cexp ((↑(2 * q.den) : ℂ) * ((↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)) : ℂ) * (↑π : ℂ) * I)) = 1
Tactic: nth_rw 1 [← q.num_div_den, ← exp_nat_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
q : ℚ
⊢ cexp ((↑(2 * q.den) : ℂ) * ((↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)) : ℂ) * (↑π : ℂ) * I)) = 1
have push_cast : cexp (HMul.hMul (α := ℂ) 2 (↑q.den : ℂ) * (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ) * (↑π : ℂ) * I)) = 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
q : ℚ
⊢ cexp (HMul.hMul (α := ℂ) 2 (↑q.den : ℂ) * (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ) * (↑π : ℂ) * I)) = 1
have rw : cexp ((↑q.num : ℂ) * (2 * (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
q : ℚ
rw : cexp ((↑q.num : ℂ) * (2 * (↑π : ℂ) * I)) = 1
⊢ cexp (HMul.hMul (α := ℂ) 2 (↑q.den : ℂ) * (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ) * (↑π : ℂ) * I)) = 1
have rw₁ : Eq (α := ℂ) 1 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
q : ℚ
⊢ IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I))
have refine : IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I) ^ (2 * q.den))
Tactic: refine .of_pow (Nat.mul_pos zero_lt_two q.den_pos) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
q : ℚ
⊢ IsIntegral ℤ (2 * sin ((↑q : ℂ) * (↑π : ℂ)))
have rw : IsIntegral ℤ ((cexp (-((↑q : ℂ) * (↑π : ℂ)) * I) - cexp ((↑q : ℂ) * (↑π : ℂ) * I)) * I)
Tactic: rw [sin.eq_1, mul_div_cancel₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
q : ℚ
⊢ IsIntegral ℤ (2 * cos ((↑q : ℂ) * (↑π : ℂ)))
have rw : IsIntegral ℤ (cexp ((↑q : ℂ) * (↑π : ℂ) * I) + cexp (-((↑q : ℂ) * (↑π : ℂ)) * I))
Tactic: rw [cos.eq_1, mul_div_cancel₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos θ)
have obtain : ∀ (r : ℚ) (hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)),
  Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos ((↑r : ℝ) * π))
Tactic: obtain ⟨r, rfl⟩ := hθ
Cleared hypotheses: θ, hθ, hcos
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ ∃ (k : ℤ), 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
have rw : ∃ (q : ℚ), 2 * cos ((↑r : ℝ) * π) = (↑q : ℝ)
Tactic: rw [← (Real.isIntegral_two_mul_cos_rat_mul_pi r).exists_int_iff_exists_rat]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ 2 * cos ((↑r : ℝ) * π) = (↑(2 * hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)
have push_cast : 2 * cos ((↑r : ℝ) * π) = HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ 2 * cos ((↑r : ℝ) * π) = HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)
have 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
Tactic: linarith [hcos.choose_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ 2 * cos ((↑r : ℝ) * π) = HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)
have linarith₁ : 2 * cos ((↑r : ℝ) * π) < HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ) →
  GT.gt (α := ℝ) 2 0
Tactic: linarith [hcos.choose_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ 2 * cos ((↑r : ℝ) * π) = HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)
have 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
Tactic: linarith [hcos.choose_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ 2 * cos ((↑r : ℝ) * π) = HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ)
have linarith₃ : HMul.hMul (α := ℝ) 2 (↑(hcos.choose (p := fun (q : ℚ) ↦ cos ((↑r : ℝ) * π) = (↑q : ℝ))) : ℝ) < 2 * cos ((↑r : ℝ) * π) →
  GT.gt (α := ℝ) 2 0
Tactic: linarith [hcos.choose_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos ((↑r : ℝ) * π))
have obtain : ∀ (k : ℤ) (hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)),
  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]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc (-2) 2) k
have rw : -2 ≤ k ∧ k ≤ 2
Tactic: rw [Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
⊢ -2 ≤ k ∧ k ≤ 2
have rify : LE.le (α := ℝ) (-2) (↑k : ℝ) ∧ LE.le (α := ℝ) (↑k : ℝ) 2
Tactic: rify
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
⊢ LE.le (α := ℝ) (-2) (↑k : ℝ) ∧ LE.le (α := ℝ) (↑k : ℝ) 2
have left : LE.le (α := ℝ) (-2) (↑k : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
left : LE.le (α := ℝ) (-2) (↑k : ℝ)
⊢ LE.le (α := ℝ) (-2) (↑k : ℝ) ∧ LE.le (α := ℝ) (↑k : ℝ) 2
have right : LE.le (α := ℝ) (↑k : ℝ) 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
⊢ LE.le (α := ℝ) (-2) (↑k : ℝ)
have linarith : LT.lt (α := ℝ) (↑k : ℝ) (-2) →
  2 * cos ((↑r : ℝ) * π) - (↑k : ℝ) + HSub.hSub (α := ℝ) (↑k : ℝ) (-2) + 2 * (-1 - cos ((↑r : ℝ) * π)) = 0
Tactic: linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ LE.le (α := ℝ) (-2) (↑k : ℝ)
have linarith₁ : LT.lt (α := ℝ) (↑k : ℝ) (-2) → GT.gt (α := ℝ) 2 0
Tactic: linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
⊢ LE.le (α := ℝ) (↑k : ℝ) 2
have linarith : LT.lt (α := ℝ) 2 (↑k : ℝ) →
  -(2 * cos ((↑r : ℝ) * π) - (↑k : ℝ)) + HSub.hSub (α := ℝ) 2 (↑k : ℝ) + 2 * (cos ((↑r : ℝ) * π) - 1) = 0
Tactic: linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ LE.le (α := ℝ) (↑k : ℝ) 2
have linarith₁ : LT.lt (α := ℝ) 2 (↑k : ℝ) → GT.gt (α := ℝ) 2 0
Tactic: linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos ((↑r : ℝ) * π))
have hk_values : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
hk_values : Membership.mem (γ := Finset ℤ) (Finset.Icc (-2) 2) k
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (cos ((↑r : ℝ) * π))
have rw : Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
Tactic: rw [show cos (r * π) = k / 2 by grind]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
k : ℤ
hk : 2 * cos ((↑r : ℝ) * π) = (↑k : ℝ)
hk_values : Membership.mem (γ := Finset ℤ) (Finset.Icc (-2) 2) k
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
have 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)
Tactic: fin_cases hk_values
Cleared hypotheses: k, hk, hk_values
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
have 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)
Tactic: fin_cases hk_values
Cleared hypotheses: k, hk, hk_values
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
have 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)
Tactic: fin_cases hk_values
Cleared hypotheses: k, hk, hk_values
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
have 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)
Tactic: fin_cases hk_values
Cleared hypotheses: k, hk, hk_values
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (HDiv.hDiv (α := ℝ) (↑k : ℝ) 2)
have 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)
Tactic: fin_cases hk_values
Cleared hypotheses: k, hk, hk_values
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (sin θ)
have h : cos (θ - π / 2) = sin θ
Tactic: convert! ← niven (θ := θ - π / 2) ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
h : cos (θ - π / 2) = sin θ
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (sin θ)
have convert_1 : ∃ (r : ℚ), θ - π / 2 = (↑r : ℝ) * π
Tactic: convert! ← niven (θ := θ - π / 2) ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
h : cos (θ - π / 2) = sin θ
convert_1 : ∃ (r : ℚ), θ - π / 2 = (↑r : ℝ) * π
⊢ Membership.mem (γ := Set ℝ) {-1, -1 / 2, 0, 1 / 2, 1} (sin θ)
have convert_2 : ∃ (q : ℚ), cos (θ - π / 2) = (↑q : ℝ)
Tactic: convert! ← niven (θ := θ - π / 2) ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
a : ℚ
h : θ = (↑a : ℝ) * π
⊢ θ - π / 2 = (↑((fun (x : ℚ) ↦ x - 1 / 2) a) : ℝ) * π
have push_cast : θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
Tactic: push_cast