awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
a : ℚ
h : θ = (↑a : ℝ) * π
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), sin θ = (↑q : ℝ)
a : ℚ
h : θ = (↑a : ℝ) * π
linarith : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → 2 / 2 = 1
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith₁ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith₄ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith₅ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith₆ : θ - π / 2 < ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π →
  2 * -(θ - (↑a : ℝ) * π) + (2 * θ - 1 * π - (HMul.hMul (α := ℝ) 2 (↑a : ℝ) - HMul.hMul (α := ℝ) 1 1) * (1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith₈ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith₉ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith₁₀ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith₁₃ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ θ - π / 2 = ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π
have linarith₁₄ : ((↑a : ℝ) - HDiv.hDiv (α := ℝ) 1 2) * π < θ - π / 2 →
  2 * (θ - (↑a : ℝ) * π) + ((HMul.hMul (α := ℝ) 2 (↑a : ℝ) - HMul.hMul (α := ℝ) 1 1) * (1 * π) - (2 * θ - 1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inl : ∀ (h : cos θ = -1), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
Tactic: rcases niven hθ hcos with h | h | h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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), π} θ
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inr : ∀ (h : cos θ = -1 / 2), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
Tactic: rcases niven hθ hcos with h | h | h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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), π} θ
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inr₁ : ∀ (h : cos θ = 0), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
Tactic: rcases niven hθ hcos with h | h | h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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), π} θ
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inr₂ : ∀ (h : cos θ = 1 / 2), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
Tactic: rcases niven hθ hcos with h | h | h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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), π} θ
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inr₃ : ∀ (h : Membership.mem (γ := Set ℝ) {1} (cos θ)), Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
Tactic: rcases niven hθ hcos with h | h | h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have h₂ : cos π = -1
Tactic: have h₂ := cos_pi
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
⊢ cos (π * (2 / 3)) = -1 / 2
have this : cos (π - π / 3) = -cos (π / 3)
Tactic: have := cos_pi_sub (π / 3)
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
this : cos (π - π / 3) = -cos (π / 3)
⊢ cos (π * (2 / 3)) = -1 / 2
have this₁ : cos (π / 3) = 1 / 2
Tactic: have := cos_pi_div_three
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have h₂ : 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;
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have h₂ : cos (π / 2) = 0
Tactic: have h₂ := cos_pi_div_two
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 1 / 2
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have h₂ : cos (π / 3) = 1 / 2
Tactic: have h₂ := cos_pi_div_three
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : Membership.mem (γ := Set ℝ) {1} (cos θ)
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have h₂ : cos 0 = 1
Tactic: have h₂ := cos_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inl : ∀ (h : cos θ = -1) (h₂ : cos π = -1), 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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), π} θ
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inr : ∀ (h : cos θ = -1 / 2) (h₂ : cos (π * (2 / 3)) = -1 / 2),
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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), π} θ
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inr₁ : ∀ (h : cos θ = 0) (h₂ : cos (π / 2) = 0), 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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), π} θ
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inr₂ : ∀ (h : cos θ = 1 / 2) (h₂ : cos (π / 3) = 1 / 2), 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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), π} θ
⊢ Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
have inr₃ : ∀ (h : Membership.mem (γ := Set ℝ) {1} (cos θ)) (h₂ : cos 0 = 1),
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1
h₂ : cos π = -1
⊢ π ≤ π
have linarith : π < π → π - π = 0
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
h₂ : cos (π * (2 / 3)) = -1 / 2
⊢ π * (2 / 3) ≤ π
have linarith : π < π * (2 / 3) → 3 / 3 = 1
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ π * (2 / 3) ≤ π
have linarith₁ : π < π * (2 / 3) → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ π * (2 / 3) ≤ π
have linarith₃ : π < π * (2 / 3) → GT.gt (α := ℝ) 3 0
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ π * (2 / 3) ≤ π
have linarith₄ : π < π * (2 / 3) → 2 / 2 = 1
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ π * (2 / 3) ≤ π
have linarith₅ : π < π * (2 / 3) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ π * (2 / 3) ≤ π
have linarith₆ : π < π * (2 / 3) → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ π * (2 / 3) ≤ π
have linarith₁₀ : π < π * (2 / 3) → 3 * π - 1 * π * HMul.hMul (α := ℝ) 1 2 + (0 - π) = 0
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
θ : ℝ
hθ : ∃ (r : ℚ), θ = (↑r : ℝ) * π
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
h₂ : cos (π / 2) = 0
⊢ π / 2 ≤ π
have linarith : π < π / 2 → 2 / 2 = 1
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ π / 2 ≤ π
have linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_nonneg]