awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = x * d
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' x K)
have hd₁ : k = d * x
Tactic: rw [mul_comm] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
have Bint : Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) B
Tactic: have Bint : B ∈ lifts (Int.castRingHom K) := by
    refine Subsemiring.prod_mem (lifts (Int.castRingHom K)) ?_
    intro x hx
    have xsmall := (Nat.mem_properDivisors.1 hx).2
    obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1
    rw [mul_comm] at hd
    exact ihk x xsmall (h.pow hpos hd)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
Bint : Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) B
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
have Bint₁ : ∃ (q : ℤ[X]), map (Int.castRingHom K) q = B ∧ q.degree = B.degree ∧ q.Monic
Tactic: replace Bint := lifts_and_degree_eq_and_monic Bint Bmo
Cleared hypotheses: Bint
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
Bint : ∃ (q : ℤ[X]), map (Int.castRingHom K) q = B ∧ q.degree = B.degree ∧ q.Monic
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
have h₁ : ∀ (B₁ : ℤ[X]) (hB₁ : map (Int.castRingHom K) B₁ = B),
  B₁.degree = B.degree →
    ∀ (hB₁mo : B₁.Monic), Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
Tactic: obtain ⟨B₁, hB₁, _, hB₁mo⟩ := Bint
Cleared hypotheses: Bint
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1 ∧ degree.{u_2} (R := K) 0 < B.degree
have left : 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left_1 : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
left : 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1 ∧ degree.{u_2} (R := K) 0 < B.degree
have right : degree.{u_2} (R := K) 0 < B.degree
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
have left : B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
Tactic: rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
        Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left_1 : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
left : B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
have left₁ : cyclotomic' k K * B = HPow.hPow (α := K[X]) X k - 1
Tactic: rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
        Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left_1 : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
left : B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
left₁ : cyclotomic' k K * B = HPow.hPow (α := K[X]) X k - 1
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
have left₂ : cyclotomic' k K * B = ∏ i ∈ k.divisors, cyclotomic' i K
Tactic: rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
        Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left_1 : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
left : B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
left₁ : cyclotomic' k K * B = HPow.hPow (α := K[X]) X k - 1
left₂ : cyclotomic' k K * B = ∏ i ∈ k.divisors, cyclotomic' i K
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
have left₃ : cyclotomic' k K * B = ∏ i ∈ Finset.cons k k.properDivisors sorry, cyclotomic' i K
Tactic: rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
        Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left_1 : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
left : B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
left₁ : cyclotomic' k K * B = HPow.hPow (α := K[X]) X k - 1
left₂ : cyclotomic' k K * B = ∏ i ∈ k.divisors, cyclotomic' i K
left₃ : cyclotomic' k K * B = ∏ i ∈ Finset.cons k k.properDivisors ⋯, cyclotomic' i K
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
have left₄ : cyclotomic' k K * B = HMul.hMul (α := K[X]) (cyclotomic' k K) (∏ x ∈ k.properDivisors, cyclotomic' x K)
Tactic: rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
        Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
have huniq : 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1 ∧ degree.{u_2} (R := K) 0 < B.degree
Tactic: have huniq : 0 + B * cyclotomic' k K = X ^ k - 1 ∧ (0 : K[X]).degree < B.degree := by
    constructor
    · rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
        Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
    · simpa only [degree_zero, bot_lt_iff_ne_bot, Ne, degree_eq_bot] using Bmo.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
huniq : 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1 ∧ degree.{u_2} (R := K) 0 < B.degree
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
have huniq₁ : (HPow.hPow (α := K[X]) X k - 1) /ₘ B = cyclotomic' k K ∧ (HPow.hPow (α := K[X]) X k - 1) %ₘ B = 0
Tactic: replace huniq := div_modByMonic_unique (cyclotomic' k K) (0 : K[X]) Bmo huniq
Cleared hypotheses: huniq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
huniq : (HPow.hPow (α := K[X]) X k - 1) /ₘ B = cyclotomic' k K ∧ (HPow.hPow (α := K[X]) X k - 1) %ₘ B = 0
⊢ ∃ (x : ℤ[X]),
    Eq.{u_2 + 1} (α := K[X]) ((mapRingHom (Int.castRingHom K) : (a : ℤ[X]) → K[X]) x : K[X]) (cyclotomic' k K : K[X])
have h₁ : Eq.{u_2 + 1} (α := K[X]) ((mapRingHom (Int.castRingHom K) : (a : ℤ[X]) → K[X]) Q₁ : K[X]) (cyclotomic' k K : K[X])
Tactic: use Q₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
huniq : (HPow.hPow (α := K[X]) X k - 1) /ₘ B = cyclotomic' k K ∧ (HPow.hPow (α := K[X]) X k - 1) %ₘ B = 0
⊢ Eq.{u_2 + 1} (α := K[X]) ((mapRingHom (Int.castRingHom K) : (a : ℤ[X]) → K[X]) Q₁ : K[X]) (cyclotomic' k K : K[X])
have h₁ : map (Int.castRingHom K) (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B = (HPow.hPow (α := K[X]) X k - 1) /ₘ B
Tactic: rw [coe_mapRingHom, map_divByMonic (Int.castRingHom K) hB₁mo, hB₁, ← huniq.1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ (↑n : ℕ)
⊢ ∃! P : ℤ[X], Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)
have obtain : ∀ (P : ℤ[X])
  (hP :
    Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K) ∧
      P.degree = degree (cyclotomic' (↑n : ℕ) K) ∧ P.Monic),
  ∃! P : ℤ[X], Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)
Tactic: obtain ⟨P, hP⟩ := int_coeff_of_cyclotomic' h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ (↑n : ℕ)
P : ℤ[X]
hP :
  Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K) ∧
    P.degree = degree (cyclotomic' (↑n : ℕ) K) ∧ P.Monic
⊢ ∃! P : ℤ[X], Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)
have refine : ∀ (Q : ℤ[X]) (hQ : (fun (P : ℤ[X]) ↦ Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)) Q), Q = P
Tactic: refine ⟨P, hP.1, fun Q hQ => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ (↑n : ℕ)
P : ℤ[X]
hP :
  Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K) ∧
    P.degree = degree (cyclotomic' (↑n : ℕ) K) ∧ P.Monic
Q : ℤ[X]
hQ : (fun (P : ℤ[X]) ↦ Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)) Q
⊢ Q = P
have a : Eq.{u_2 + 1} (α := K[X]) (map (Int.castRingHom K) Q) (map (Int.castRingHom K) P)
Tactic: apply map_injective (Int.castRingHom K) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ (↑n : ℕ)
P : ℤ[X]
hP :
  Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K) ∧
    P.degree = degree (cyclotomic' (↑n : ℕ) K) ∧ P.Monic
Q : ℤ[X]
hQ : (fun (P : ℤ[X]) ↦ Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)) Q
a : Eq (α := K[X]) (map (Int.castRingHom K) Q) (cyclotomic' (↑n : ℕ) K)
⊢ Eq.{u_2 + 1} (α := K[X]) (map (Int.castRingHom K) Q) (map (Int.castRingHom K) P)
have a₁ : Eq (α := K[X]) (cyclotomic' (↑n : ℕ) K) (cyclotomic' (↑n : ℕ) K)
Tactic: rw [hP.1, hQ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ cyclotomic n ℤ =
    Exists.choose (p := fun (P : ℤ[X]) ↦
      map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯
have simp : map (Int.castRingHom ℤ)
    (sorry.choose (p := fun (P : ℤ[X]) ↦
      map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic)) =
  Exists.choose (p := fun (P : ℤ[X]) ↦
    map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) sorry
Tactic: simp only [cyclotomic, h, dif_neg, not_false_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ map (Int.castRingHom ℤ)
      (⋯.choose (p := fun (P : ℤ[X]) ↦
        map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic)) =
    Exists.choose (p := fun (P : ℤ[X]) ↦
      map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) ⋯
have a : ∀ (i : ℕ),
  (map (Int.castRingHom ℤ)
          (sorry.choose (p := fun (P : ℤ[X]) ↦
            map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic))).coeff
      i =
    (Exists.choose (p := fun (P : ℤ[X]) ↦
          map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) sorry).coeff
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
⊢ Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)
have pos : ∀ (hzero : n = 0), Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)
Tactic: by_cases hzero : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
pos : ∀ (hzero : n = 0), Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)
⊢ Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)
have neg : ∀ (hzero : ¬n = 0), Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) (cyclotomic n R)
Tactic: by_cases hzero : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
have pos : ∀ (hzero : n = 0),
  map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
Tactic: by_cases hzero : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
pos :
  ∀ (hzero : n = 0),
    map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
      degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
have neg : ∀ (hzero : ¬n = 0),
  map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
Tactic: by_cases hzero : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    degree (cyclotomic n ℤ) = degree (cyclotomic' n ℂ) ∧ Monic (cyclotomic n ℤ)
have neg : map (Int.castRingHom ℂ)
      (Exists.choose (p := fun (P : ℤ[X]) ↦
        map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) sorry) =
    cyclotomic' n ℂ ∧
  (Exists.choose (p := fun (P : ℤ[X]) ↦
          map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) sorry).degree =
      degree (cyclotomic' n ℂ) ∧
    (Exists.choose (p := fun (P : ℤ[X]) ↦
        map (Int.castRingHom ℂ) P = cyclotomic' n ℂ ∧ P.degree = degree (cyclotomic' n ℂ) ∧ P.Monic) sorry).Monic
Tactic: rw [int_cyclotomic_rw hzero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ P = cyclotomic n ℤ
have a : map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
Tactic: apply map_injective (Int.castRingHom ℂ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
⊢ map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
have a : cyclotomic' n ℂ = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
Tactic: rw [h, (int_cyclotomic_spec n).1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
P : ℤ[X]
h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ
a : cyclotomic' n ℂ = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
⊢ map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
have a₁ : Eq (α := ℂ[X]) (cyclotomic' n ℂ) (cyclotomic' n ℂ)
Tactic: rw [h, (int_cyclotomic_spec n).1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
⊢ map f (cyclotomic n R) = cyclotomic n S
have rw : map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)
Tactic: rw [← map_cyclotomic_int n R, ← map_cyclotomic_int n S, map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
⊢ map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)
have this : Subsingleton.{max (u_2 + 1) 1} (ℤ →+* S)
Tactic: have : Subsingleton (ℤ →+* S) := inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
q : R
n : ℕ
inst : Ring R
inst_1 : Ring S
f : R →+* S
⊢ Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) q) (cyclotomic n S) : S)
    ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
have rw : Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) q) (map f (cyclotomic n R)) : S)
  ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
Tactic: rw [← map_cyclotomic n f, eval_map, eval₂_at_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
q : R
n : ℕ
inst : Ring R
inst_1 : Ring S
f : R →+* S
rw :
  Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) q) (map f (cyclotomic n R)) : S)
    ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
⊢ Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) q) (cyclotomic n S) : S)
    ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
have rw₁ : eval₂ f ((f : (a : R) → S) q) (cyclotomic n R) = (f : (a : R) → S) (eval q (cyclotomic n R))
Tactic: rw [← map_cyclotomic n f, eval_map, eval₂_at_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
q : R
n : ℕ
inst : Ring R
inst_1 : Ring S
f : R →+* S
rw :
  Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) q) (map f (cyclotomic n R)) : S)
    ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
rw₁ : eval₂ f ((f : (a : R) → S) q) (cyclotomic n R) = (f : (a : R) → S) (eval q (cyclotomic n R))
⊢ Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) q) (cyclotomic n S) : S)
    ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
have rw₂ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
  ((f : (a : R) → S) (eval q (cyclotomic n R)) : S)
Tactic: rw [← map_cyclotomic n f, eval_map, eval₂_at_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
⊢ cyclotomic 1 R = HSub.hSub (α := R[X]) X 1
have hspec : map (Int.castRingHom ℂ) (HSub.hSub (α := ℤ[X]) X 1) = cyclotomic' 1 ℂ
Tactic: have hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ := by
    simp only [cyclotomic'_one, map_X, Polynomial.map_one, Polynomial.map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
hspec : map (Int.castRingHom ℂ) (HSub.hSub (α := ℤ[X]) X 1) = cyclotomic' 1 ℂ
⊢ cyclotomic 1 R = HSub.hSub (α := R[X]) X 1
have symm : HSub.hSub (α := R[X]) X 1 = cyclotomic 1 R
Tactic: symm