awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
⊢ 0 < eval x (cyclotomic n R)
have hn' : 0 < n
Tactic: have hn' : 0 < n := pos_of_gt hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
⊢ 0 < eval x (cyclotomic n R)
have hn'' : 1 < n
Tactic: have hn'' : 1 < n := one_lt_two.trans hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
⊢ 0 < eval x (cyclotomic n R)
have this : Eq.{u_1 + 1} (α := R[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
Tactic: have := prod_cyclotomic_eq_geom_sum hn' R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : Eq.{u_1 + 1} (α := R[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
⊢ 0 < eval x (cyclotomic n R)
have this₁ : eval x (∏ i ∈ n.divisors.erase 1, cyclotomic i R) = eval x (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
Tactic: apply_fun eval x at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (∏ i ∈ n.divisors.erase 1, cyclotomic i R) = eval x (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
⊢ 0 < eval x (cyclotomic n R)
have this₁ : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
Tactic: rw [← cons_self_properDivisors hn'.ne', Finset.erase_cons_of_ne _ hn''.ne', Finset.prod_cons,
    eval_mul, eval_geom_sum] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
⊢ 0 < eval x (cyclotomic n R)
have h : ∀ (h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)), 0 < eval x (cyclotomic n R)
Tactic: rcases lt_trichotomy 0 (∑ i ∈ Finset.range n, x ^ i) with (h | h | h)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∀ (h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)), 0 < eval x (cyclotomic n R)
⊢ 0 < eval x (cyclotomic n R)
have h₁ : ∀ (h : Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i)), 0 < eval x (cyclotomic n R)
Tactic: rcases lt_trichotomy 0 (∑ i ∈ Finset.range n, x ^ i) with (h | h | h)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∀ (h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)), 0 < eval x (cyclotomic n R)
h₁ : ∀ (h : Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i)), 0 < eval x (cyclotomic n R)
⊢ 0 < eval x (cyclotomic n R)
have h₂ : ∀ (h : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0), 0 < eval x (cyclotomic n R)
Tactic: rcases lt_trichotomy 0 (∑ i ∈ Finset.range n, x ^ i) with (h | h | h)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ 0 < eval x (cyclotomic n R)
have h₁ : 0 < eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R)
Tactic: apply pos_of_mul_pos_left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
h₁ : 0 < eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R)
⊢ 0 < eval x (cyclotomic n R)
have h₂ : 0 ≤ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R)
Tactic: apply pos_of_mul_pos_left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ 0 ≤ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R)
have h₁ : LE.le.{u_1} (α := R) 0 (∏ j ∈ n.properDivisors.erase 1, eval x (cyclotomic j R))
Tactic: rw [eval_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ LE.le.{u_1} (α := R) 0 (∏ j ∈ n.properDivisors.erase 1, eval x (cyclotomic j R))
have h₁ : ∀ (i : ℕ) (hi : i ∈ n.properDivisors.erase 1), 0 ≤ eval x (cyclotomic i R)
Tactic: refine Finset.prod_nonneg fun i hi => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
i : ℕ
hi : i ∈ n.properDivisors.erase 1
⊢ 0 ≤ eval x (cyclotomic i R)
have hi₁ : i ≠ 1 ∧ i ∣ n ∧ i < n
Tactic: simp only [Finset.mem_erase, mem_properDivisors] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ 0 ≤ eval x (cyclotomic i R)
have h₁ : ∀ (h : Odd n ∨ 0 < x + 1) (i : ℕ) (hi : i ≠ 1 ∧ i ∣ n ∧ i < n), 0 ≤ eval x (cyclotomic i R)
Tactic: rw [geom_sum_pos_iff hn'.ne'] at h
Cleared hypotheses: h, i, hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Odd n ∨ 0 < x + 1
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ 0 ≤ eval x (cyclotomic i R)
have h₁ : ∀ (hk : Odd n), 0 ≤ eval x (cyclotomic i R)
Tactic: rcases h with hk | hx
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Odd n ∨ 0 < x + 1
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
h₁ : ∀ (hk : Odd n), 0 ≤ eval x (cyclotomic i R)
⊢ 0 ≤ eval x (cyclotomic i R)
have h₂ : ∀ (hx : 0 < x + 1), 0 ≤ eval x (cyclotomic i R)
Tactic: rcases h with hk | hx
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ 0 ≤ eval x (cyclotomic i R)
have h : i ≠ 0
Tactic: refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
h : i ≠ 0
⊢ 0 ≤ eval x (cyclotomic i R)
have h₁ : i ≠ 2
Tactic: refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
⊢ 0 ≤ eval x (cyclotomic i R)
have h : ∀ (hi : Ne (α := ℕ) 2 1 ∧ 2 ∣ n ∧ 2 < n), 0 ≤ eval x (cyclotomic 2 R)
Tactic: rcases eq_or_ne i 2 with (rfl | hk)
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
h : ∀ (hi : Ne (α := ℕ) 2 1 ∧ 2 ∣ n ∧ 2 < n), 0 ≤ eval x (cyclotomic 2 R)
⊢ 0 ≤ eval x (cyclotomic i R)
have h₁ : ∀ (hk : i ≠ 2), 0 ≤ eval x (cyclotomic i R)
Tactic: rcases eq_or_ne i 2 with (rfl | hk)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
hk : i ≠ 2
⊢ 0 ≤ eval x (cyclotomic i R)
have h : i ≠ 0
Tactic: refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 hk)).le
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ 0 < eval x (cyclotomic n R)
have h₁ : x = -1 ∧ Even n
Tactic: rw [eq_comm, geom_sum_eq_zero_iff_neg_one hn'.ne'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ 0 < eval x (cyclotomic n R)
have h₁ : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) < 0
Tactic: apply pos_of_mul_neg_left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
h₁ : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) < 0
⊢ 0 < eval x (cyclotomic n R)
have h₂ : eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0
Tactic: apply pos_of_mul_neg_left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0
have h₁ : Even n ∧ x + 1 < 0
Tactic: rw [geom_sum_neg_iff hn'.ne'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ 2 ∈ n.properDivisors.erase 1
have rw : Ne (α := ℕ) 2 1 ∧ 2 ∣ n ∧ 2 < n
Tactic: rw [Finset.mem_erase, mem_properDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0
have h2 : 2 ∈ n.properDivisors.erase 1
Tactic: have h2 : 2 ∈ n.properDivisors.erase 1 := by
      rw [Finset.mem_erase, mem_properDivisors]
      exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
⊢ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0
have h₁ : (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R)) * eval x (cyclotomic 2 R) ≤ 0
Tactic: rw [eval_prod, ← Finset.prod_erase_mul _ _ h2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
⊢ (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R)) * eval x (cyclotomic 2 R) ≤ 0
have h₁ : LE.le.{u_1} (α := R) 0 (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R))
Tactic: apply mul_nonpos_of_nonneg_of_nonpos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
h₁ : LE.le.{u_1} (α := R) 0 (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R))
⊢ (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R)) * eval x (cyclotomic 2 R) ≤ 0
have h₂ : eval x (cyclotomic 2 R) ≤ 0
Tactic: apply mul_nonpos_of_nonneg_of_nonpos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
⊢ LE.le.{u_1} (α := R) 0 (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R))
have h₁ : ∀ (i : ℕ) (hi : i ∈ (n.properDivisors.erase 1).erase 2), 0 < eval x (cyclotomic i R)
Tactic: refine Finset.prod_nonneg fun i hi => le_of_lt ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
i : ℕ
hi : i ∈ (n.properDivisors.erase 1).erase 2
⊢ 0 < eval x (cyclotomic i R)
have hi₁ : i ≠ 2 ∧ i ≠ 1 ∧ i ∣ n ∧ i < n
Tactic: simp only [Finset.mem_erase, mem_properDivisors] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
i : ℕ
hi : i ≠ 2 ∧ i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ 0 < eval x (cyclotomic i R)
have h₁ : i ≠ 0
Tactic: refine ih _ hi.2.2.2 (Nat.two_lt_of_ne ?_ hi.2.1 hi.1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
hi : Ne (α := ℕ) 0 2 ∧ Ne (α := ℕ) 0 1 ∧ 0 ∣ n ∧ 0 < n
⊢ False
have hi₁ : Ne (α := ℕ) 0 2 ∧ Ne (α := ℕ) 0 1 ∧ n = 0 ∧ 0 < n
Tactic: rw [zero_dvd_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))
have zero : (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))
Tactic: rcases n with (_ | _ | _ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
zero : (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))
⊢ (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))
have succ : (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R)) ∧
  (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R))
Tactic: rcases n with (_ | _ | _ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
zero : (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))
succ :
  (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R))
⊢ (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))
have succ₁ : (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R)) ∧
  (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R))
Tactic: rcases n with (_ | _ | _ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
zero : (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))
succ :
  (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R))
succ₁ :
  (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R))
⊢ (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))
have succ₂ : ∀ (n : ℕ), (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))
Tactic: rcases n with (_ | _ | _ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R))
have succ : (1 < x → 0 < x + 1) ∧ (1 ≤ x → 0 ≤ x + 1)
Tactic: simp only [zero_add, reduceAdd, cyclotomic_two, eval_add, eval_X, eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < x + 1) ∧ (1 ≤ x → 0 ≤ x + 1)
have succ : 1 < x → 0 < x + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
succ : 1 < x → 0 < x + 1
⊢ (1 < x → 0 < x + 1) ∧ (1 ≤ x → 0 ≤ x + 1)
have succ₁ : 1 ≤ x → 0 ≤ x + 1
Tactic: constructor