awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 ≤ π
have linarith₂ : π < π / 2 → 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 θ = 0
h₂ : cos (π / 2) = 0
linarith : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
⊢ π / 2 ≤ π
have linarith₃ : π < π / 2 → 2 * π - 1 * π + (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 θ = 1 / 2
h₂ : cos (π / 3) = 1 / 2
⊢ π / 3 ≤ π
have linarith : π < π / 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 (π / 3) = 1 / 2
linarith : π < π / 3 → 3 / 3 = 1
⊢ π / 3 ≤ π
have linarith₁ : π < π / 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 (π / 3) = 1 / 2
linarith : π < π / 3 → 3 / 3 = 1
linarith₁ : π < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
⊢ π / 3 ≤ π
have linarith₂ : π < π / 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 (π / 3) = 1 / 2
linarith : π < π / 3 → 3 / 3 = 1
linarith₁ : π < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π < π / 3 → GT.gt (α := ℝ) 3 0
⊢ π / 3 ≤ π
have linarith₃ : π < π / 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 (π / 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
⊢ π / 3 ≤ π
have linarith₄ : π < π / 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 (π / 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
⊢ π / 3 ≤ π
have linarith₅ : π < π / 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 (π / 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
⊢ π / 3 ≤ π
have linarith₉ : π < π / 3 → 3 * π - 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 : Membership.mem (γ := Set ℝ) {1} (cos θ)
h₂ : cos 0 = 1
⊢ 0 ≤ π
have linarith : π < 0 → π - 0 + (0 - π) = 0
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : Membership.mem (γ := Set ℚ) (Set.Icc 0 1) r
⊢ Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3, 1} r
have apply : Membership.mem (γ := Set ℝ) ((fun (x : ℚ) ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}) (r • π)
Tactic: apply smul_left_injective ℚ pi_ne_zero |>.mem_set_image.mp
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : Membership.mem (γ := Set ℚ) (Set.Icc 0 1) r
⊢ (↑r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π)
have hr : 0 ≤ r
Tactic: obtain ⟨hr, hr'⟩ := h_bnd
Cleared hypotheses: h_bnd
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : Membership.mem (γ := Set ℚ) (Set.Icc 0 1) r
hr : 0 ≤ r
⊢ (↑r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π)
have hr' : r ≤ 1
Tactic: obtain ⟨hr, hr'⟩ := h_bnd
Cleared hypotheses: h_bnd
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hr : 0 ≤ r
hr' : r ≤ 1
⊢ (↑r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π)
have left : 0 * π ≤ (↑r : ℝ) * π
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hr : 0 ≤ r
hr' : r ≤ 1
left : 0 * π ≤ (↑r : ℝ) * π
⊢ (↑r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π)
have right : (↑r : ℝ) * π ≤ 1 * π
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hr : 0 ≤ r
hr' : r ≤ 1
⊢ 0 * π ≤ (↑r : ℝ) * π
have left : LE.le (α := ℝ) 0 (↑r : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
hr : 0 ≤ r
hr' : r ≤ 1
⊢ (↑r : ℝ) * π ≤ 1 * π
have right : LE.le (α := ℝ) (↑r : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : Membership.mem (γ := Set ℚ) (Set.Icc 0 1) r
⊢ Membership.mem (γ := Set ℝ) ((fun (x : ℚ) ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}) (r • π)
have h_bnd₁ : (↑r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π)
Tactic: replace h_bnd : (r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π) := by
    obtain ⟨hr, hr'⟩ := h_bnd; constructor <;> gcongr <;> norm_cast
Cleared hypotheses: h_bnd
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
h_bnd : (↑r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π)
⊢ Membership.mem (γ := Set ℝ) ((fun (x : ℚ) ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}) (r • π)
have 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 • π)
Tactic: generalize h : (r : ℝ) * π = θ at *
Cleared hypotheses: hcos, h_bnd
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
θ : ℝ
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 • π)
have this : Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
Tactic: have := niven_angle_eq ⟨r, h.symm⟩ hcos (by simpa using h_bnd)
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
θ : ℝ
h : (↑r : ℝ) * π = θ
hcos : ∃ (q : ℚ), cos θ = (↑q : ℝ)
h_bnd : θ ∈ Set.Icc (0 * π) (1 * π)
this : Membership.mem (γ := Set ℝ) {0, π / 3, π / 2, π * (2 / 3), π} θ
⊢ Membership.mem (γ := Set ℝ) ((fun (x : ℚ) ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}) (r • π)
have simp_all : ∀ (h_bnd : 0 ≤ θ ∧ θ ≤ π) (this : θ = 0 ∨ θ = π / 3 ∨ θ = π / 2 ∨ θ = π * (2 / 3) ∨ θ = π),
  0 = θ ∨ 3⁻¹ * π = θ ∨ 2⁻¹ * π = θ ∨ HDiv.hDiv (α := ℝ) 2 3 * π = θ ∨ π = θ
Tactic: simp_all [Rat.smul_def]
Cleared hypotheses: h_bnd, this
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3} (Int.fract r)
have suffices : Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3, 1} (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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ Membership.mem (γ := Set ℚ) {0, 1 / 3, 1 / 2, 2 / 3, 1} (Int.fract r)
have refine : ∃ (q : ℚ), cos ((↑(Int.fract r) : ℝ) * π) = (↑q : ℝ)
Tactic: refine niven_angle_div_pi_eq (r := Int.fract r) ?_ (by simp [le_of_lt <| Int.fract_lt_one r])
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hcos : ∃ (q : ℚ), cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ ∃ (q : ℚ), cos ((↑(Int.fract r) : ℝ) * π) = (↑q : ℝ)
have obtain : ∀ (q : ℚ) (hq : cos ((↑r : ℝ) * π) = (↑q : ℝ)), ∃ (q : ℚ), cos ((↑(Int.fract r) : ℝ) * π) = (↑q : ℝ)
Tactic: obtain ⟨q, hq⟩ := hcos
Cleared hypotheses: hcos
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r q : ℚ
hq : cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ cos ((↑(r - (↑⌊r⌋ : ℚ)) : ℝ) * π) = (↑(HPow.hPow (α := ℚ) (-1) ⌊r⌋ * q) : ℝ)
have push_cast : cos (HSub.hSub (α := ℝ) (↑r : ℝ) (↑⌊r⌋ : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r q : ℚ
hq : cos ((↑r : ℝ) * π) = (↑q : ℝ)
⊢ cos (HSub.hSub (α := ℝ) (↑r : ℝ) (↑⌊r⌋ : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
have rw : cos ((↑r : ℝ) * π - (↑⌊r⌋ : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
Tactic: rw [sub_mul, cos_sub_int_mul_pi, hq]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r q : ℚ
hq : cos ((↑r : ℝ) * π) = (↑q : ℝ)
rw : cos ((↑r : ℝ) * π - (↑⌊r⌋ : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
⊢ cos (HSub.hSub (α := ℝ) (↑r : ℝ) (↑⌊r⌋ : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
have rw₁ : HPow.hPow (α := ℝ) (-1) ⌊r⌋ * cos ((↑r : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
Tactic: rw [sub_mul, cos_sub_int_mul_pi, hq]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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 : ℝ)
⊢ cos (HSub.hSub (α := ℝ) (↑r : ℝ) (↑⌊r⌋ : ℝ) * π) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
have rw₂ : HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ) = HPow.hPow (α := ℝ) (-1) ⌊r⌋ * (↑q : ℝ)
Tactic: rw [sub_mul, cos_sub_int_mul_pi, hq]
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hr : 3 < r.den
⊢ Irrational (cos ((↑r : ℝ) * π))
have hr₁ : 3 < (Int.fract r).den
Tactic: rw [← Rat.den_intFract] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
⊢ Irrational (cos ((↑r : ℝ) * π))
have by_contra! : ∀ (hnz : ¬Irrational (cos ((↑r : ℝ) * π))), False
Tactic: by_contra! hnz
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
⊢ False
have inl : ∀ (hr' : Int.fract r = 0), False
Tactic: rcases niven_fract_angle_div_pi_eq (exists_rat_of_not_irrational hnz) with (hr' | hr' | hr' | hr')
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
inl : ∀ (hr' : Int.fract r = 0), False
⊢ False
have inr : ∀ (hr' : Int.fract r = 1 / 3), False
Tactic: rcases niven_fract_angle_div_pi_eq (exists_rat_of_not_irrational hnz) with (hr' | hr' | hr' | hr')
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ False
have inr₁ : ∀ (hr' : Int.fract r = 1 / 2), False
Tactic: rcases niven_fract_angle_div_pi_eq (exists_rat_of_not_irrational hnz) with (hr' | hr' | hr' | hr')
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (goal)
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
⊢ False
have inr₂ : ∀ (hr' : Membership.mem (γ := Set ℚ) {2 / 3} (Int.fract r)), False
Tactic: rcases niven_fract_angle_div_pi_eq (exists_rat_of_not_irrational hnz) with (hr' | hr' | hr' | hr')
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 0
⊢ False
have hr₁ : 3 < Rat.den 0
Tactic: rw [hr'] at hr
Cleared hypotheses: hr, hnz, hr'
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 3
⊢ False
have hr₁ : 3 < (1 / 3).den
Tactic: rw [hr'] at hr
Cleared hypotheses: hr, hnz, hr'
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 1 / 2
⊢ False
have hr₁ : 3 < (1 / 2).den
Tactic: rw [hr'] at hr
Cleared hypotheses: hr, hnz, hr'
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Membership.mem (γ := Set ℚ) {2 / 3} (Int.fract r)
⊢ False
have hr'₁ : Int.fract r = 2 / 3
Tactic: rw [Set.mem_singleton_iff] at hr'
Cleared hypotheses: hr'
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Membership.mem (γ := Set ℚ) {2 / 3} (Int.fract r)
⊢ False
have hr'₁ : Int.fract r = 2 / 3
Tactic: try rw [Set.mem_singleton_iff] at hr'
Cleared hypotheses: hr'
-- Lean 4 proof step from Mathlib.NumberTheory.Niven (hypothesis)
Goal:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos ((↑r : ℝ) * π))
hr' : Int.fract r = 2 / 3
⊢ False
have hr₁ : 3 < (2 / 3).den
Tactic: rw [hr'] at hr
Cleared hypotheses: hr, hnz, hr'
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
⊢ Eq.{u_4 + 1} (α := 𝓞 L)
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
        ((f : (a : K) → L) (↑1 : K)) ⋯ :
      ↥(integralClosure ℤ L))
    (1 : 𝓞 L)
have h : Eq.{u_4 + 1} (α := L)
  ((↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑1 : K)) sorry) :
      L) :
    L)
  ((↑1 : L) : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
x y : 𝓞 K
⊢ Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
      ((f : (a : K) → L) (↑(x * y) : K)) ⋯ =
    HMul.hMul (α := 𝓞 L) (β := 𝓞 L)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑x : K)) ⋯ :
        ↥(integralClosure ℤ L))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑y : K)) ⋯ :
        ↥(integralClosure ℤ L))
have h : (↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
        ((f : (a : K) → L) (↑(x * y) : K)) sorry) :
    L) =
  (↑(HMul.hMul (α := 𝓞 L) (β := 𝓞 L)
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            ((f : (a : K) → L) (↑x : K)) sorry :
          ↥(integralClosure ℤ L))
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            ((f : (a : K) → L) (↑y : K)) sorry :
          ↥(integralClosure ℤ L))) :
    L)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
⊢ Eq.{u_4 + 1} (α := 𝓞 L)
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
        ((f : (a : K) → L) (↑0 : K)) ⋯ :
      ↥(integralClosure ℤ L))
    (0 : 𝓞 L)
have h : Eq.{u_4 + 1} (α := L)
  ((↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑0 : K)) sorry) :
      L) :
    L)
  ((↑0 : L) : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
x y : 𝓞 K
⊢ Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
      ((f : (a : K) → L) (↑(x + y) : K)) ⋯ =
    HAdd.hAdd (α := 𝓞 L) (β := 𝓞 L)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑x : K)) ⋯ :
        ↥(integralClosure ℤ L))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑y : K)) ⋯ :
        ↥(integralClosure ℤ L))
have h : (↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
        ((f : (a : K) → L) (↑(x + y) : K)) sorry) :
    L) =
  (↑(HAdd.hAdd (α := 𝓞 L) (β := 𝓞 L)
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            ((f : (a : K) → L) (↑x : K)) sorry :
          ↥(integralClosure ℤ L))
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            ((f : (a : K) → L) (↑y : K)) sorry :
          ↥(integralClosure ℤ L))) :
    L)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
⊢ IsIntegral ℤ x
have obtain : ∀ (P : Polynomial ℤ) (hPm : P.Monic)
  (hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P = 0), IsIntegral ℤ x
Tactic: obtain ⟨P, hPm, hP⟩ := x.isIntegral_coe
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P = 0
⊢ IsIntegral ℤ x
have refine : Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
Tactic: refine ⟨P, hPm, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
have rwa : ∀
  (hP :
    Polynomial.eval₂ (@RingHom.comp _ (𝓞 K) _ _ Semiring.toNonAssocSemiring _ (algebraMap (𝓞 K) K) (algebraMap ℤ (𝓞 K)))
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P =
      0),
  Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
Tactic: rwa [IsScalarTower.algebraMap_eq (S := 𝓞 K), ← Polynomial.hom_eval₂, coe_eq_zero_iff] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P = 0
rwa :
  ∀
    (hP :
      Polynomial.eval₂
          (@RingHom.comp _ (𝓞 K) _ _ Semiring.toNonAssocSemiring _ (algebraMap (𝓞 K) K) (algebraMap ℤ (𝓞 K)))
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P =
        0),
    Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
have rwa₁ : ∀ (hP : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P) : K) (0 : K)),
  Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
Tactic: rwa [IsScalarTower.algebraMap_eq (S := 𝓞 K), ← Polynomial.hom_eval₂, coe_eq_zero_iff] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P = 0
rwa :
  ∀
    (hP :
      Polynomial.eval₂
          (@RingHom.comp _ (𝓞 K) _ _ Semiring.toNonAssocSemiring _ (algebraMap (𝓞 K) K) (algebraMap ℤ (𝓞 K)))
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P =
        0),
    Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
rwa₁ :
  ∀ (hP : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P) : K) (0 : K)),
    Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
have rwa₂ : ∀ (hP : Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0), Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
Tactic: rwa [IsScalarTower.algebraMap_eq (S := 𝓞 K), ← Polynomial.hom_eval₂, coe_eq_zero_iff] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ ¬IsField.{u_1} (𝓞 K)
have h_inj : Injective.{1, u_1 + 1} (α := ℤ) (β := 𝓞 K) (⇑(algebraMap ℤ (𝓞 K)) : (a : ℤ) → 𝓞 K)
Tactic: have h_inj : Function.Injective (algebraMap ℤ (𝓞 K)) := RingHom.injective_int (algebraMap ℤ (𝓞 K))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
⊢ restrict (⇑f : (a : M) → K) h 0 = 0
have simp : Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) 0 sorry = 0
Tactic: simp only [restrict, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
x y : M
⊢ restrict (⇑f : (a : M) → K) h (x + y) = restrict (⇑f : (a : M) → K) h x + restrict (⇑f : (a : M) → K) h y
have simp : Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
    (HAdd.hAdd (α := K) (β := K) ((f : (a : M) → K) x : K) ((f : (a : M) → K) y : K)) sorry =
  HAdd.hAdd (α := 𝓞 K) (β := 𝓞 K)
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) ((f : (a : M) → K) x)
        sorry :
      ↥(integralClosure ℤ K))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) ((f : (a : M) → K) y)
        sorry :
      ↥(integralClosure ℤ K))
Tactic: simp only [restrict, map_add]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
⊢ restrict (⇑f : (a : M) → K) h 1 = 1
have simp : Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) 1 sorry = 1
Tactic: simp only [restrict, map_one]