awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
⊢ Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔ ∀ (i j : Fin p), α i = α j
have hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
Tactic: have hP (i : Fin p) : α i = P.coeff i := by simp [P, ← Fin.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
x : Fin p
h : Membership.mem (γ := Finset (Fin p)) Finset.univ x
⊢ (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α x) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑x : ℕ))).degree ≤
    (↑(p - 1) : WithBot ℕ)
have grw : LE.le (α := WithBot ℕ) (↑(↑x : ℕ) : WithBot ℕ) (↑(p - 1) : WithBot ℕ)
Tactic: grw [degree_C_mul_X_pow_le]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
x : Fin p
h : Membership.mem (γ := Finset (Fin p)) Finset.univ x
⊢ LE.le (α := WithBot ℕ) (↑(↑x : ℕ) : WithBot ℕ) (↑(p - 1) : WithBot ℕ)
have simp : (↑x : ℕ) ≤ p - 1
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
⊢ Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔ ∀ (i j : Fin p), α i = α j
have hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
Tactic: have hP' : P.degree ≤ ↑(p - 1) :=
    (degree_sum_le ..).trans (Finset.sup_le fun _ _ ↦ by grw [degree_C_mul_X_pow_le]; simp; grind)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
⊢ Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔ ∀ (i j : Fin p), α i = α j
have trans : Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔
  Eq (α := K) ((aeval ζ : (a : ℚ[X]) → K) P : K) (0 : K)
Tactic: trans aeval ζ P = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
trans :
  Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔
    Eq (α := K) ((aeval ζ : (a : ℚ[X]) → K) P : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔ ∀ (i j : Fin p), α i = α j
have trans₁ : Eq (α := K) ((aeval ζ : (a : ℚ[X]) → K) P : K) (0 : K) ↔ ∀ (i j : Fin p), α i = α j
Tactic: trans aeval ζ P = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
⊢ Eq (α := K) ((aeval ζ : (a : ℚ[X]) → K) P : K) (0 : K) ↔ ∀ (i j : Fin p), α i = α j
have rw : cyclotomic p ℚ ∣ P ↔ ∀ (i j : Fin p), α i = α j
Tactic: rw [← minpoly.dvd_iff, ← cyclotomic_eq_minpoly_rat hζ hp.pos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
⊢ cyclotomic p ℚ ∣ P ↔ ∀ (i j : Fin p), α i = α j
have refine_1 : cyclotomic p ℚ ∣ P → ∀ (c : ℚ[X]) (hc : P = cyclotomic p ℚ * c) (i j : Fin p), α i = α j
Tactic: refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun H ↦ ⟨C (α 0), Polynomial.ext fun i ↦ if h : i < p then ?_ else ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
refine_1 : cyclotomic p ℚ ∣ P → ∀ (c : ℚ[X]) (hc : P = cyclotomic p ℚ * c) (i j : Fin p), α i = α j
⊢ cyclotomic p ℚ ∣ P ↔ ∀ (i j : Fin p), α i = α j
have refine_2 : ∀ (H : ∀ (i j : Fin p), α i = α j) (i : ℕ) (h : i < p),
  P.coeff i = (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff i
Tactic: refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun H ↦ ⟨C (α 0), Polynomial.ext fun i ↦ if h : i < p then ?_ else ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
refine_1 : cyclotomic p ℚ ∣ P → ∀ (c : ℚ[X]) (hc : P = cyclotomic p ℚ * c) (i j : Fin p), α i = α j
refine_2 :
  ∀ (H : ∀ (i j : Fin p), α i = α j) (i : ℕ) (h : i < p),
    P.coeff i = (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff i
⊢ cyclotomic p ℚ ∣ P ↔ ∀ (i j : Fin p), α i = α j
have refine_3 : ∀ (H : ∀ (i j : Fin p), α i = α j) (i : ℕ) (h : ¬i < p),
  P.coeff i = (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff i
Tactic: refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun H ↦ ⟨C (α 0), Polynomial.ext fun i ↦ if h : i < p then ?_ else ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ[X]
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j
have hP'₁ : (↑(p - 1) : WithBot ℕ) + c.degree ≤ (↑(p - 1) : WithBot ℕ)
Tactic: rw [hc, degree_mul, degree_cyclotomic, Nat.totient_prime hp] at hP'
Cleared hypotheses: hP', hc
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : (↑(p - 1) : WithBot ℕ) + c.degree ≤ (↑(p - 1) : WithBot ℕ)
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j
have this₁ : c.degree ≤ 0
Tactic: have : c.degree ≤ 0 := (WithBot.add_le_add_iff_left (x := ↑(p - 1)) (by simp)).mp (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this_1 : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : (↑(p - 1) : WithBot ℕ) + c.degree ≤ (↑(p - 1) : WithBot ℕ)
hc : P = cyclotomic p ℚ * c
this : c.degree ≤ 0
⊢ ∀ (i j : Fin p), α i = α j
have refine_1 : ∀ (c : ℚ) (hP' : (↑(p - 1) : WithBot ℕ) + degree (R := ℚ) ((C : (a : ℚ) → ℚ[X]) c) ≤ (↑(p - 1) : WithBot ℕ))
  (hc : P = HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) c : ℚ[X]))
  (this : degree (R := ℚ) ((C : (a : ℚ) → ℚ[X]) c) ≤ 0) (i j : Fin p), α i = α j
Tactic: obtain ⟨c, rfl⟩ := natDegree_eq_zero.mp (natDegree_eq_zero_iff_degree_le_zero.mpr this)
Cleared hypotheses: c, hP', hc, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : i < p
⊢ P.coeff i = (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff i
have refine_2 : ∀ (i : Fin p),
  P.coeff (↑i : ℕ) =
    (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff (↑i : ℕ)
Tactic: lift i to Fin p using h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
n : ℕ
⊢ dickson k a (n + 2) =
    HMul.hMul (α := R[X]) X (dickson k a (n + 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a n)
have rw : HMul.hMul (α := R[X]) X (dickson k a (n + 1)) -
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a n) =
  HMul.hMul (α := R[X]) X (dickson k a (n + 1)) -
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a n)
Tactic: rw [dickson]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ n
⊢ dickson k a n =
    HMul.hMul (α := R[X]) X (dickson k a (n - 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (n - 2))
have obtain : ∀ (n : ℕ) (h : 2 ≤ 2 + n),
  dickson k a (2 + n) =
    HMul.hMul (α := R[X]) X (dickson k a (2 + n - 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (2 + n - 2))
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (2 + n) =
    HMul.hMul (α := R[X]) X (dickson k a (2 + n - 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (2 + n - 2))
have rw : dickson k a (n + 2) =
  HMul.hMul (α := R[X]) X (dickson k a (n + 2 - 1)) -
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (n + 2 - 2))
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f (dickson k a 0) = dickson k ((f : (a : R) → S) a) 0
have simp_rw : map f (HSub.hSub (α := R[X]) 3 (↑k : R[X])) = HSub.hSub (α := S[X]) 3 (↑k : S[X])
Tactic: simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_natCast, Polynomial.map_ofNat]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
simp_rw : map f (HSub.hSub (α := R[X]) 3 (↑k : R[X])) = HSub.hSub (α := S[X]) 3 (↑k : S[X])
⊢ map f (dickson k a 0) = dickson k ((f : (a : R) → S) a) 0
have simp_rw₁ : map f 3 - map f (↑k : R[X]) = HSub.hSub (α := S[X]) 3 (↑k : S[X])
Tactic: simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_natCast, Polynomial.map_ofNat]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
simp_rw : map f (HSub.hSub (α := R[X]) 3 (↑k : R[X])) = HSub.hSub (α := S[X]) 3 (↑k : S[X])
simp_rw₁ : map f 3 - map f (↑k : R[X]) = HSub.hSub (α := S[X]) 3 (↑k : S[X])
⊢ map f (dickson k a 0) = dickson k ((f : (a : R) → S) a) 0
have simp_rw₂ : map f 3 - (↑k : S[X]) = HSub.hSub (α := S[X]) 3 (↑k : S[X])
Tactic: simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_natCast, Polynomial.map_ofNat]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ map f (dickson k a (n + 2)) = dickson k ((f : (a : R) → S) a) (n + 2)
have simp : X * map f (dickson k a (n + 1)) -
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X]) (map f (dickson k a n)) =
  HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
      (dickson k ((f : (a : R) → S) a) n : S[X])
Tactic: simp only [dickson_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, map_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ X * map f (dickson k a (n + 1)) -
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X]) (map f (dickson k a n)) =
    HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X])
have rw : X * map f (dickson k a (n + 1)) -
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
      (dickson k ((f : (a : R) → S) a) n : S[X]) =
  HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
      (dickson k ((f : (a : R) → S) a) n : S[X])
Tactic: rw [map_dickson f n, map_dickson f (n + 1)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
rw :
  X * map f (dickson k a (n + 1)) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X]) =
    HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X])
⊢ X * map f (dickson k a (n + 1)) -
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X]) (map f (dickson k a n)) =
    HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X])
have rw₁ : HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
      (dickson k ((f : (a : R) → S) a) n : S[X]) =
  HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
      (dickson k ((f : (a : R) → S) a) n : S[X])
Tactic: rw [map_dickson f n, map_dickson f (n + 1)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ dickson 2 0 (n + 2) = HPow.hPow (α := R[X]) X (n + 2)
have simp : HMul.hMul (α := R[X]) X (dickson 2 0 (n + 1)) = HPow.hPow (α := R[X]) X (n + 2)
Tactic: simp only [dickson_add_two, C_0, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ HMul.hMul (α := R[X]) X (dickson 2 0 (n + 1)) = HPow.hPow (α := R[X]) X (n + 2)
have rw : X * HPow.hPow (α := R[X]) X (n + 1) = HPow.hPow (α := R[X]) X (n + 2)
Tactic: rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
rw : X * HPow.hPow (α := R[X]) X (n + 1) = HPow.hPow (α := R[X]) X (n + 2)
⊢ HMul.hMul (α := R[X]) X (dickson 2 0 (n + 1)) = HPow.hPow (α := R[X]) X (n + 2)
have rw₁ : X * HPow.hPow (α := R[X]) X (n + 1) = HPow.hPow (α := R[X]) X (n + 1) * HPow.hPow (α := R[X]) (β := ℕ) X 1
Tactic: rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
rw : X * HPow.hPow (α := R[X]) X (n + 1) = HPow.hPow (α := R[X]) X (n + 2)
rw₁ : X * HPow.hPow (α := R[X]) X (n + 1) = HPow.hPow (α := R[X]) X (n + 1) * HPow.hPow (α := R[X]) (β := ℕ) X 1
⊢ HMul.hMul (α := R[X]) X (dickson 2 0 (n + 1)) = HPow.hPow (α := R[X]) X (n + 2)
have rw₂ : HPow.hPow (α := R[X]) X (n + 1) * X = HPow.hPow (α := R[X]) X (n + 1) * HPow.hPow (α := R[X]) (β := ℕ) X 1
Tactic: rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
rw : X * HPow.hPow (α := R[X]) X (n + 1) = HPow.hPow (α := R[X]) X (n + 2)
rw₁ : X * HPow.hPow (α := R[X]) X (n + 1) = HPow.hPow (α := R[X]) X (n + 1) * HPow.hPow (α := R[X]) (β := ℕ) X 1
rw₂ : HPow.hPow (α := R[X]) X (n + 1) * X = HPow.hPow (α := R[X]) X (n + 1) * HPow.hPow (α := R[X]) (β := ℕ) X 1
⊢ HMul.hMul (α := R[X]) X (dickson 2 0 (n + 1)) = HPow.hPow (α := R[X]) X (n + 2)
have rw₃ : HPow.hPow (α := R[X]) X (n + 1) * X = HPow.hPow (α := R[X]) X (n + 1) * X
Tactic: rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
⊢ eval (x + y) (dickson 1 1 0) = HPow.hPow (β := ℕ) x 0 + HPow.hPow (β := ℕ) y 0
have simp : eval (x + y) (HSub.hSub (α := R[X]) 3 (↑1 : R[X])) = HAdd.hAdd (α := R) 1 1
Tactic: simp only [pow_zero, dickson_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ eval (x + y) (dickson 1 1 (n + 2)) = x ^ (n + 2) + y ^ (n + 2)
have simp : (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
Tactic: simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv x y h _, eval_X, dickson_add_two,
      C_1, eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
n : ℕ
| (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n)
have simp : x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n)
Tactic: simp only [pow_succ', add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
have conv_lhs : x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
Tactic: conv_lhs => simp only [pow_succ', add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
⊢ HMul.hMul (α := R[X]) 2 ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) = 1
have rw : HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
    ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
  1
Tactic: rw [two_mul, ← C_add, invOf_two_add_invOf_two, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
rw :
  HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
      ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    1
⊢ HMul.hMul (α := R[X]) 2 ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) = 1
have rw₁ : Eq (α := R[X])
  ((C : (a : R) → R[X])
      (HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
    R[X])
  (1 : R[X])
Tactic: rw [two_mul, ← C_add, invOf_two_add_invOf_two, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
rw :
  HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
      ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    1
rw₁ :
  Eq (α := R[X])
    ((C : (a : R) → R[X])
        (HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
      R[X])
    (1 : R[X])
⊢ HMul.hMul (α := R[X]) 2 ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) = 1
have rw₂ : Eq.{u_1 + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
Tactic: rw [two_mul, ← C_add, invOf_two_add_invOf_two, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
rw :
  HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
      ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    1
rw₁ :
  Eq (α := R[X])
    ((C : (a : R) → R[X])
        (HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) :
      R[X])
    (1 : R[X])
rw₂ : Eq.{u_1 + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
⊢ HMul.hMul (α := R[X]) 2 ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) = 1
have rw₃ : Eq.{u_1 + 1} (α := R[X]) 1 1
Tactic: rw [two_mul, ← C_add, invOf_two_add_invOf_two, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Dickson (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) 2 = 1
have rw : HMul.hMul (α := R[X]) 2 ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) = 1
Tactic: rw [mul_comm, two_mul_C_half_eq_one]