awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
this : cos (π - π / 3) = -cos (π / 3)
⊢ cos (π / 3) = 1 / 2

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

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

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

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

Tactic:
have h₂ := cos_pi_div_three
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : Membership.mem (γ := Set ℝ) {1} (cos θ)
⊢ cos 0 = 1

Tactic:
have h₂ := cos_zero
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
inl : ∀ (h : cos θ = -1) (h₂ : cos π = -1), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
inr :
  ∀ (h : cos θ = -1 / 2) (h₂ : cos (π * (2 / 3)) = -1 / 2),
    Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
inr₁ : ∀ (h : cos θ = 0) (h₂ : cos (π / 2) = 0), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
inr₂ : ∀ (h : cos θ = 1 / 2) (h₂ : cos (π / 3) = 1 / 2), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
inr₃ :
  ∀ (h : Membership.mem (γ := Set ℝ) {1} (cos θ)) (h₂ : cos 0 = 1),
    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 <;>
  -- define `h₂` appropriately for each proof branch
  [have h₂ := cos_pi;
    have h₂ : cos (π * (2 / 3)) = -1 / 2 := by
      have := cos_pi_sub (π / 3)
      have := cos_pi_div_three
      grind;;
    have h₂ := cos_pi_div_two;
    have h₂ := cos_pi_div_three;
    have h₂ := cos_zero]

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

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1
h₂ : cos π = -1
linarith : π < π → π - π = 0
⊢ π ≤ π

Tactic:
linarith [pi_nonneg]

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

Tactic:
simp [injOn_cos h_bnd ⟨by positivity, by linarith [pi_nonneg]⟩ (h₂ ▸ h)]

Premises used: And.intro, Real.injOn_cos
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
h₂ : cos (π * (2 / 3)) = -1 / 2
⊢ 0 ≤ π * (2 / 3)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
h₂ : cos (π * (2 / 3)) = -1 / 2
linarith : π < π * (2 / 3) → 3 / 3 = 1
linarith₁ linarith₂ : π < π * (2 / 3) → HMul.hMul (α := ℝ) 1 3 = 3
linarith₃ : π < π * (2 / 3) → GT.gt (α := ℝ) 3 0
linarith₄ : π < π * (2 / 3) → 2 / 2 = 1
linarith₅ : π < π * (2 / 3) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : π < π * (2 / 3) → GT.gt (α := ℝ) 2 0
linarith₇ : π < π * (2 / 3) → 2 / 2 = 1
linarith₈ : π < π * (2 / 3) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : π < π * (2 / 3) → GT.gt (α := ℝ) 2 0
linarith₁₀ : π < π * (2 / 3) → 3 * π - 1 * π * HMul.hMul (α := ℝ) 1 2 + (0 - π) = 0
⊢ π * (2 / 3) ≤ π

Tactic:
linarith [pi_nonneg]

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

Tactic:
simp [injOn_cos h_bnd ⟨by positivity, by linarith [pi_nonneg]⟩ (h₂ ▸ h)]

Premises used: And.intro, Real.injOn_cos
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
h₂ : cos (π / 2) = 0
⊢ 0 ≤ π / 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
h₂ : cos (π / 2) = 0
linarith : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : π < π / 2 → 2 * π - 1 * π + (0 - π) = 0
⊢ π / 2 ≤ π

Tactic:
linarith [pi_nonneg]

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

Tactic:
simp [injOn_cos h_bnd ⟨by positivity, by linarith [pi_nonneg]⟩ (h₂ ▸ h)]

Premises used: And.intro, Real.injOn_cos
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 1 / 2
h₂ : cos (π / 3) = 1 / 2
⊢ 0 ≤ π / 3

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 1 / 2
h₂ : cos (π / 3) = 1 / 2
linarith : π < π / 3 → 3 / 3 = 1
linarith₁ : π < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π < π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ : π < π / 3 → 2 / 2 = 1
linarith₄ : π < π / 3 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π < π / 3 → GT.gt (α := ℝ) 2 0
linarith₆ : π < π / 3 → 2 / 2 = 1
linarith₇ : π < π / 3 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π < π / 3 → GT.gt (α := ℝ) 2 0
linarith₉ : π < π / 3 → 3 * π - 1 * π + 2 * (0 - π) = 0
linarith₁₀ : π < π / 3 → GT.gt (α := ℝ) 2 0
⊢ π / 3 ≤ π

Tactic:
linarith [pi_nonneg]

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

Tactic:
simp [injOn_cos h_bnd ⟨by positivity, by linarith [pi_nonneg]⟩ (h₂ ▸ h)]

Premises used: And.intro, Real.injOn_cos
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : Membership.mem (γ := Set ℝ) {1} (cos θ)
h₂ : cos 0 = 1
⊢ LE.le (α := ℝ) 0 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Niven
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : Membership.mem (γ := Set ℝ) {1} (cos θ)
h₂ : cos 0 = 1
linarith : π < 0 → π - 0 + (0 - π) = 0
⊢ 0 ≤ π

Tactic:
linarith [pi_nonneg]

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

Tactic:
simp [injOn_cos h_bnd ⟨by positivity, by linarith [pi_nonneg]⟩ (h₂ ▸ h)]

Premises used: And.intro, Real.injOn_cos
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : Membership.mem (γ := Set ℚ) (Set.Icc 0 1) r
apply : Membership.mem (γ := Set ℝ) ((fun (x : ℚ) ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}) (r • π)
⊢ Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3, 1} r

Tactic:
apply smul_left_injective ℚ pi_ne_zero |>.mem_set_image.mp

Premises used: Rat, smul_left_injective, Iff.mp, Function.Injective.mem_set_image, Real.pi_ne_zero
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : Membership.mem (γ := Set ℚ) (Set.Icc 0 1) r
⊢ 0 ≤ r

Tactic:
obtain ⟨hr, hr'⟩ := h_bnd
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : Membership.mem (γ := Set ℚ) (Set.Icc 0 1) r
hr : 0 ≤ r
⊢ r ≤ 1

Tactic:
obtain ⟨hr, hr'⟩ := h_bnd
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hr : 0 ≤ r
hr' : r ≤ 1
left : 0 * π ≤ (↑r : ℝ) * π
right : (↑r : ℝ) * π ≤ 1 * π
⊢ (↑r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hr : 0 ≤ r
hr' : r ≤ 1
left : LE.le (α := ℝ) 0 (↑r : ℝ)
⊢ 0 * π ≤ (↑r : ℝ) * π

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hr : 0 ≤ r
hr' : r ≤ 1
right : LE.le (α := ℝ) (↑r : ℝ) 1
⊢ (↑r : ℝ) * π ≤ 1 * π

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hr : 0 ≤ r
hr' : r ≤ 1
left left₁ left₂ left₃ : 0 ≤ r
⊢ LE.le (α := ℝ) 0 (↑r : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hr : 0 ≤ r
hr' : r ≤ 1
right right₁ right₂ right₃ : r ≤ 1
⊢ LE.le (α := ℝ) (↑r : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : Membership.mem (γ := Set ℚ) (Set.Icc 0 1) r
⊢ (↑r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π)

Tactic:
replace h_bnd : (r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π) := by
    obtain ⟨hr, hr'⟩ := h_bnd; constructor <;> gcongr <;> norm_cast
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : (↑r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π)
generalize :
  ∀ (θ : ℝ) (h : (↑r : ℝ) * π = θ) (hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)) (h_bnd : θ ∈ Set.Icc (0 * π) (1 * π)),
    Membership.mem (γ := Set ℝ) ((fun (x : ℚ) ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}) (r • π)
⊢ Membership.mem (γ := Set ℝ) ((fun (x : ℚ) ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}) (r • π)

Tactic:
generalize h : (r : ℝ) * π = θ at *

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

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

Tactic:
have := niven_angle_eq ⟨r, h.symm⟩ hcos (by simpa using h_bnd)
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
θ : ℝ
h : (↑r : ℝ) * π = θ
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc (0 * π) (1 * π)
this : Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
simp_all :
  ∀ (h_bnd : 0 ≤ θ ∧ θ ≤ π) (this : θ = 0 ∨ θ = π / 3 ∨ θ = π / 2 ∨ θ = π * (2 / 3) ∨ θ = π),
    0 = θ ∨ 3⁻¹ * π = θ ∨ 2⁻¹ * π = θ ∨ HDiv.hDiv (α := ℝ) 2 3 * π = θ ∨ π = θ
⊢ Membership.mem (γ := Set ℝ) ((fun (x : ℚ) ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}) (r • π)

Tactic:
simp_all [Rat.smul_def]

Premises used: Rat.smul_def
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
θ : ℝ
h : (↑r : ℝ) * π = θ
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : 0 ≤ θ ∧ θ ≤ π
this : θ = 0 ∨ θ = π / 3 ∨ θ = π / 2 ∨ θ = π * (2 / 3) ∨ θ = π
⊢ 0 = θ ∨ 3⁻¹ * π = θ ∨ 2⁻¹ * π = θ ∨ HDiv.hDiv (α := ℝ) 2 3 * π = θ ∨ π = θ

Tactic:
grind
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
this : Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3, 1} (Int.fract r)
⊢ Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3} (Int.fract r)

Tactic:
grind [ne_of_lt (Int.fract_lt_one r)]

Premises used: Int.fract_lt_one, ne_of_lt
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
suffices : Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3, 1} (Int.fract r)
⊢ Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3} (Int.fract r)

Tactic:
suffices Int.fract r ∈ ({0, 1 / 3, 1 / 2, 2 / 3, 1} : Set ℚ) by
    grind [ne_of_lt (Int.fract_lt_one r)]
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ Membership.mem (γ := Set ℚ) (Set.Icc 0 1) (Int.fract r)

Tactic:
simp [le_of_lt <| Int.fract_lt_one r]

Premises used: le_of_lt, Int.fract_lt_one
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
refine : ∃ (q : ℚ), cos ((↑(Int.fract r) : ℝ) * π) = (↑q : ℝ)
⊢ Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3, 1} (Int.fract r)

Tactic:
refine niven_angle_div_pi_eq (r := Int.fract r) ?_ (by simp [le_of_lt <| Int.fract_lt_one r])

Premises used: niven_angle_div_pi_eq
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
obtain : ∀ (q : ℚ) (hq : cos ((↑r : ℝ) * π) = (↑q : ℝ)), ∃ (q : ℚ), cos ((↑(Int.fract r) : ℝ) * π) = (↑q : ℝ)
⊢ ∃ (q : ℚ), cos ((↑(Int.fract r) : ℝ) * π) = (↑q : ℝ)

Tactic:
obtain ⟨q, hq⟩ := hcos
-- Module: Mathlib.NumberTheory.Niven
Goal:
r q : ℚ
hq : cos ((↑r : ℝ) * π) = (↑q : ℝ)
push_cast : cos (HSub.hSub (α := ℝ) (↑r : ℝ) (↑⌊r⌋ : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
⊢ cos ((↑(r - (↑⌊r⌋ : ℚ)) : ℝ) * π) = (↑(HPow.hPow (α := ℚ) (-1) ⌊r⌋ * q) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Niven
Goal:
r q : ℚ
hq : cos ((↑r : ℝ) * π) = (↑q : ℝ)
rw : cos ((↑r : ℝ) * π - (↑⌊r⌋ : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
rw₁ : HPow.hPow (α := ℝ) (-1) ⌊r⌋ * cos ((↑r : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
rw₂ rw₃ : HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
⊢ cos (HSub.hSub (α := ℝ) (↑r : ℝ) (↑⌊r⌋ : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)

Tactic:
rw [sub_mul, cos_sub_int_mul_pi, hq]

Premises used: sub_mul, Real.cos_sub_int_mul_pi
-- Module: Mathlib.NumberTheory.Niven
Goal:
r q : ℚ
hq : cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ ∃ (q : ℚ), cos ((↑(Int.fract r) : ℝ) * π) = (↑q : ℝ)

Tactic:
exact ⟨(-1) ^ ⌊r⌋ * q, by rw [Int.fract]; push_cast; rw [sub_mul, cos_sub_int_mul_pi, hq]⟩
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < r.den
⊢ 3 < (Int.fract r).den

Tactic:
rw [← Rat.den_intFract] at hr

Premises used: Rat.den_intFract
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
by_contra! : ∀ (hnz : ¬Irrational (cos ((↑r : ℝ) * π))), False
⊢ Irrational (cos ((↑r : ℝ) * π))

Tactic:
by_contra! hnz
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
inl : ∀ (hr' : Int.fract r = 0), False
inr : ∀ (hr' : Int.fract r = 1 / 3), False
inr₁ : ∀ (hr' : Int.fract r = 1 / 2), False
inr₂ : ∀ (hr' : Membership.mem (γ := Set ℚ) {2 / 3} (Int.fract r)), False
⊢ False

Tactic:
rcases niven_fract_angle_div_pi_eq (exists_rat_of_not_irrational hnz) with (hr' | hr' | hr' | hr')

Premises used: exists_rat_of_not_irrational, niven_fract_angle_div_pi_eq
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 0
⊢ 3 < Rat.den 0

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 0
hr₁ : 3 < Rat.den 0
⊢ ¬Irrational (cos ((↑r : ℝ) * π))

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 0
hr₁ : 3 < Rat.den 0
hnz₁ : ¬Irrational (cos ((↑r : ℝ) * π))
⊢ Int.fract r = 0

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < Rat.den 0
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 0
⊢ False

Tactic:
norm_num at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 3
⊢ 3 < (1 / 3).den

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 3
hr₁ : 3 < (1 / 3).den
⊢ ¬Irrational (cos ((↑r : ℝ) * π))

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 3
hr₁ : 3 < (1 / 3).den
hnz₁ : ¬Irrational (cos ((↑r : ℝ) * π))
⊢ Int.fract r = 1 / 3

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (1 / 3).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 3
⊢ False

Tactic:
norm_num at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 2
⊢ 3 < (1 / 2).den

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 2
hr₁ : 3 < (1 / 2).den
⊢ ¬Irrational (cos ((↑r : ℝ) * π))

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 2
hr₁ : 3 < (1 / 2).den
hnz₁ : ¬Irrational (cos ((↑r : ℝ) * π))
⊢ Int.fract r = 1 / 2

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (1 / 2).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 2
⊢ False

Tactic:
norm_num at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Membership.mem (γ := Set ℚ) {2 / 3} (Int.fract r)
⊢ Int.fract r = 2 / 3

Tactic:
rw [Set.mem_singleton_iff] at hr'

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Membership.mem (γ := Set ℚ) {2 / 3} (Int.fract r)
⊢ Int.fract r = 2 / 3

Tactic:
try rw [Set.mem_singleton_iff] at hr'

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 2 / 3
⊢ 3 < (2 / 3).den

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 2 / 3
hr₁ : 3 < (2 / 3).den
⊢ ¬Irrational (cos ((↑r : ℝ) * π))

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 2 / 3
hr₁ : 3 < (2 / 3).den
hnz₁ : ¬Irrational (cos ((↑r : ℝ) * π))
⊢ Int.fract r = 2 / 3

Tactic:
rw [hr'] at hr
-- Module: Mathlib.NumberTheory.Niven
Goal:
r : ℚ
hr : 3 < (2 / 3).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 2 / 3
⊢ False

Tactic:
norm_num at hr
-- Module: Mathlib.NumberTheory.NumberField.AdeleRing
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
v : InfinitePlace K
⊢ Eq (α := v.Completion) (((algebraMap K (AdeleRing R K) : (a : K) → AdeleRing R K) x).1 v)
    (↑(WithAbs.toAbs (↑v : AbsoluteValue K ℝ) x) : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- Module: Mathlib.NumberTheory.NumberField.AdeleRing
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
v : HeightOneSpectrum R
⊢ (((algebraMap K (AdeleRing R K) : (a : K) → AdeleRing R K) x).2 :
        (a : HeightOneSpectrum R) → HeightOneSpectrum.adicCompletion K a)
      v =
    (↑((RingEquiv.symm (WithVal.equiv (HeightOneSpectrum.valuation K v)) :
            (a : K) → WithVal (HeightOneSpectrum.valuation K v))
          x) :
      UniformSpace.Completion (WithVal (HeightOneSpectrum.valuation K v)))

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- Module: Mathlib.NumberTheory.NumberField.AdeleRing
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : NumberField K
⊢ Function.Injective (α := K) (β := AdeleRing R K) (⇑(algebraMap K (AdeleRing R K)) : (a : K) → AdeleRing R K)

Tactic:
fun _ _ hxy => (algebraMap K _).injective (Prod.ext_iff.1 hxy).1

Premises used: Algebra.algebraMap, NumberField.InfiniteAdeleRing, Prod.ext_iff, RingHom.injective, And.left, Iff.mp, Function.Injective
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Algebra.IsAlgebraic ℚ K

Tactic:
Algebra.IsAlgebraic.of_finite _ _

Premises used: Algebra.IsAlgebraic.of_finite
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
inst_3 : NumberField L
inst_4 : Algebra K L
⊢ FiniteDimensional K L

Tactic:
Module.Finite.of_restrictScalars_finite ℚ K L

Premises used: Rat, Module.Finite.of_restrictScalars_finite
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
inst_3 : NumberField L
inst_4 : Algebra K L
E : IntermediateField K L
⊢ NumberField.{u_2} ↥E

Tactic:
of_module_finite K E

Premises used: Membership.mem, Subtype, NumberField.of_module_finite
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
inst_3 : NumberField L
inst_4 : Algebra K L
E : Type u_3
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra E L
inst_8 : IsScalarTower K E L
⊢ NumberField E

Tactic:
letI := Module.Finite.left K E L
  of_module_finite K E

Premises used: NumberField.of_module_finite
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
e : K ≃+* L
inst_2 : NumberField K
⊢ Eq.{u_2 + 1} (α := L) ((e.toAddMonoidHom : (a : K) → L) 1 : L) (1 : L)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
⊢ CharZero.{u_1} (𝓞 K)

Tactic:
inferInstanceAs (CharZero (integralClosure _ _))

Premises used: _private.0.NumberField.RingOfIntegers.instCharZero._proof_1
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
⊢ IsTorsionFree (𝓞 K) K

Tactic:
inferInstanceAs (IsTorsionFree (integralClosure _ _) _)

Premises used: _private.0.NumberField.RingOfIntegers.instIsTorsionFree._proof_1
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L_1 : Type u_2
inst : Field K
inst_1 : Field L_1
L : Type u_3
inst_2 : Ring L
inst_3 : Algebra K L
⊢ IsScalarTower (𝓞 K) K L

Tactic:
inferInstanceAs (IsScalarTower (integralClosure _ _) K L)

Premises used: _private.0.NumberField.RingOfIntegers.instIsScalarTower._proof_1
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
G : Type u_3
inst_2 : Group G
inst_3 : MulSemiringAction G K
⊢ SMulDistribClass G (𝓞 K) K

Tactic:
inferInstanceAs (SMulDistribClass G (integralClosure ℤ K) K)

Premises used: _private.0.NumberField.RingOfIntegers.instSMulDistribClass._proof_1
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
⊢ Eq (α := Algebra (𝓞 K) K) (instAlgebra K) (instAlgebra_1 K)

Tactic:
rfl