awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
r : R
h : ∃ (s : R), r = s ^ p ^ n
⊢ count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
have pos : ∀ (s : R),
  count (s ^ p ^ n)
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count (s ^ p ^ n) (p ^ n • f.roots)
Tactic: obtain ⟨s, rfl⟩ := h
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
s : R
⊢ count (s ^ p ^ n)
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count (s ^ p ^ n) (p ^ n • f.roots)
have pos : card.{u_1} (α := R)
    (filter (fun (a : R) ↦ s ^ p ^ n = (iterateFrobenius R p n : (a : R) → R) a)
      (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
  card.{u_1} (α := R) (filter (fun (x : R) ↦ s = x) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))
Tactic: simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
r : R
h : ¬∃ (s : R), r = s ^ p ^ n
⊢ count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
have h₁ : count r
    (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
      (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
  0
Tactic: convert! Nat.zero_le _
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
r : R
h : ¬∃ (s : R), r = s ^ p ^ n
⊢ count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
    0
have h₁ : Eq.{u_1 + 1} (α := Multiset R)
  (filter (fun (a : R) ↦ r = (iterateFrobenius R p n : (a : R) → R) a)
    (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))
  0
Tactic: simp_rw [count_map, card_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
⊢ Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) ≤
    p ^ n • f.roots
have refine : ∀ (r : R),
  count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
Tactic: classical
  refine le_iff_count.2 fun r ↦ ?_
  by_cases h : ∃ s, r = s ^ p ^ n
  · obtain ⟨s, rfl⟩ := h
    simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]
    exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
  convert! Nat.zero_le _
  simp_rw [count_map, card_eq_zero]
  exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
refine :
  ∀ (r : R),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
⊢ Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) ≤
    p ^ n • f.roots
have pos : ∀ (r : R) (h : ∃ (s : R), r = s ^ p ^ n),
  count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
Tactic: classical
  refine le_iff_count.2 fun r ↦ ?_
  by_cases h : ∃ s, r = s ^ p ^ n
  · obtain ⟨s, rfl⟩ := h
    simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]
    exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
  convert! Nat.zero_le _
  simp_rw [count_map, card_eq_zero]
  exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
refine :
  ∀ (r : R),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
pos :
  ∀ (r : R) (h : ∃ (s : R), r = s ^ p ^ n),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
⊢ Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) ≤
    p ^ n • f.roots
have neg : ∀ (r : R) (h : ¬∃ (s : R), r = s ^ p ^ n),
  count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
Tactic: classical
  refine le_iff_count.2 fun r ↦ ?_
  by_cases h : ∃ s, r = s ^ p ^ n
  · obtain ⟨s, rfl⟩ := h
    simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]
    exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
  convert! Nat.zero_le _
  simp_rw [count_map, card_eq_zero]
  exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
refine :
  ∀ (r : R),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
pos :
  ∀ (r : R) (h : ∃ (s : R), r = s ^ p ^ n),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
neg neg₁ :
  ∀ (r : R) (h : ¬∃ (s : R), r = s ^ p ^ n),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
⊢ Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) ≤
    p ^ n • f.roots
have h : ∀ (r : R) (h : ¬∃ (s : R), r = s ^ p ^ n),
  count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
    0
Tactic: classical
  refine le_iff_count.2 fun r ↦ ?_
  by_cases h : ∃ s, r = s ^ p ^ n
  · obtain ⟨s, rfl⟩ := h
    simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]
    exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
  convert! Nat.zero_le _
  simp_rw [count_map, card_eq_zero]
  exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
refine :
  ∀ (r : R),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
pos :
  ∀ (r : R) (h : ∃ (s : R), r = s ^ p ^ n),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
neg neg₁ :
  ∀ (r : R) (h : ¬∃ (s : R), r = s ^ p ^ n),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
h :
  ∀ (r : R) (h : ¬∃ (s : R), r = s ^ p ^ n),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
      0
⊢ Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) ≤
    p ^ n • f.roots
have h₁ : ∀ (r : R) (h : ¬∃ (s : R), r = s ^ p ^ n),
  Eq.{u_1 + 1} (α := Multiset R)
    (filter (fun (a : R) ↦ r = (iterateFrobenius R p n : (a : R) → R) a)
      (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))
    0
Tactic: classical
  refine le_iff_count.2 fun r ↦ ?_
  by_cases h : ∃ s, r = s ^ p ^ n
  · obtain ⟨s, rfl⟩ := h
    simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]
    exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
  convert! Nat.zero_le _
  simp_rw [count_map, card_eq_zero]
  exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
⊢ Multiset.map (α := R) (⇑(frobenius R p) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f)) ≤ p • f.roots
have rw : Multiset.map (α := R) (⇑(iterateFrobenius R p 1) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f)) ≤
  p • f.roots
Tactic: rw [← iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
⊢ Multiset.map (α := R) (⇑(iterateFrobenius R p 1) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f)) ≤
    p • f.roots
have h : HPow.hPow (β := ℕ) p 1 = p
Tactic: convert! ← roots_expand_pow_map_iterateFrobenius_le p 1 f
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : DecidableEq R
⊢ Finset.image (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
      (toFinset (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ⊆
    f.roots.toFinset
have rw : Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) ⊆
  p ^ n • f.roots
Tactic: rw [Finset.image_toFinset, ← (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne',
    toFinset_subset]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : DecidableEq R
⊢ Finset.image (α := R) (⇑(frobenius R p) : (a : R) → R) (toFinset (roots ((expand R p : (a : R[X]) → R[X]) f))) ⊆
    f.roots.toFinset
have rw : Finset.image (α := R) (⇑(iterateFrobenius R p 1) : (a : R) → R)
    (toFinset (roots ((expand R p : (a : R[X]) → R[X]) f))) ⊆
  f.roots.toFinset
Tactic: rw [← iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : DecidableEq R
⊢ Finset.image (α := R) (⇑(iterateFrobenius R p 1) : (a : R) → R)
      (toFinset (roots ((expand R p : (a : R[X]) → R[X]) f))) ⊆
    f.roots.toFinset
have h : HPow.hPow (β := ℕ) p 1 = p
Tactic: convert! ← roots_expand_pow_image_iterateFrobenius_subset p 1 f
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
⊢ roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f) =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots)
have refine : ∀ (r : R),
  count r (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) =
    count r
      (HSMul.hSMul (β := Multiset R) (p ^ n)
        (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots))
Tactic: refine ext' fun r ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
r : R
⊢ count r (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) =
    count r
      (HSMul.hSMul (β := Multiset R) (p ^ n)
        (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots))
have rw : p ^ n * (filter (fun (x : R) ↦ r ^ p ^ n = x) f.roots).card =
  p ^ n * (filter (fun (a : R) ↦ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) a) f.roots).card
Tactic: rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
    count_eq_card_filter_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
r : R
⊢ p ^ n * (filter (fun (x : R) ↦ r ^ p ^ n = x) f.roots).card =
    p ^ n * (filter (fun (a : R) ↦ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) a) f.roots).card
have e_a : Eq.{u_1 + 1} (α := R → Prop) (fun (x : R) ↦ r ^ p ^ n = x) fun (a : R) ↦
  r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) a
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
r : R
⊢ Eq.{u_1 + 1} (α := R → Prop) (fun (x : R) ↦ r ^ p ^ n = x) fun (a : R) ↦
    r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) a
have e_a : ∀ (x : R), r ^ p ^ n = x ↔ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
⊢ roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f) =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots)
have refine : ∀ (r : R),
  count r (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) =
    count r
      (HSMul.hSMul (β := Multiset R) (p ^ n)
        (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots))
Tactic: classical
  refine ext' fun r ↦ ?_
  rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
    count_eq_card_filter_eq]; congr; ext
  exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
refine :
  ∀ (r : R),
    count r (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) =
      count r
        (HSMul.hSMul (β := Multiset R) (p ^ n)
          (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots))
⊢ roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f) =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots)
have refine₁ : ∀ (r : R),
  p ^ n * (filter (fun (x : R) ↦ r ^ p ^ n = x) f.roots).card =
    p ^ n * (filter (fun (a : R) ↦ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) a) f.roots).card
Tactic: classical
  refine ext' fun r ↦ ?_
  rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
    count_eq_card_filter_eq]; congr; ext
  exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
refine :
  ∀ (r : R),
    count r (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) =
      count r
        (HSMul.hSMul (β := Multiset R) (p ^ n)
          (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots))
refine₁ refine₂ :
  ∀ (r : R),
    p ^ n * (filter (fun (x : R) ↦ r ^ p ^ n = x) f.roots).card =
      p ^ n * (filter (fun (a : R) ↦ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) a) f.roots).card
⊢ roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f) =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots)
have e_a : ∀ (r : R),
  Eq.{u_1 + 1} (α := R → Prop) (fun (x : R) ↦ r ^ p ^ n = x) fun (a : R) ↦
    r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) a
Tactic: classical
  refine ext' fun r ↦ ?_
  rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
    count_eq_card_filter_eq]; congr; ext
  exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
refine :
  ∀ (r : R),
    count r (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) =
      count r
        (HSMul.hSMul (β := Multiset R) (p ^ n)
          (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots))
refine₁ refine₂ :
  ∀ (r : R),
    p ^ n * (filter (fun (x : R) ↦ r ^ p ^ n = x) f.roots).card =
      p ^ n * (filter (fun (a : R) ↦ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) a) f.roots).card
e_a e_a₁ :
  ∀ (r : R),
    Eq.{u_1 + 1} (α := R → Prop) (fun (x : R) ↦ r ^ p ^ n = x) fun (a : R) ↦
      r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) a
⊢ roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f) =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots)
have e_a₂ : ∀ (r x : R), r ^ p ^ n = x ↔ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x
Tactic: classical
  refine ext' fun r ↦ ?_
  rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
    count_eq_card_filter_eq]; congr; ext
  exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
| roots ((expand R p : (a : R[X]) → R[X]) f)
have rw : HSMul.hSMul (β := Multiset R) p
  (Multiset.map (⇑(HPow.hPow (α := R ≃+* R) (β := ℕ) (frobeniusEquiv R p) 1).symm : (a : R) → R) f.roots)
Tactic: rw [← pow_one p, roots_expand_pow, iterateFrobeniusEquiv_eq_pow, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
⊢ roots ((expand R p : (a : R[X]) → R[X]) f) =
    HSMul.hSMul (β := Multiset R) p (Multiset.map (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) f.roots)
have conv_lhs : HSMul.hSMul (β := Multiset R) p
    (Multiset.map (⇑(HPow.hPow (α := R ≃+* R) (β := ℕ) (frobeniusEquiv R p) 1).symm : (a : R) → R) f.roots) =
  HSMul.hSMul (β := Multiset R) p (Multiset.map (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) f.roots)
Tactic: conv_lhs => rw [← pow_one p, roots_expand_pow, iterateFrobeniusEquiv_eq_pow, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
y : R
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (p ^ n)) ((C : (a : R) → R[X]) y : R[X])).roots =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))
have H : roots ((expand R (p ^ n) : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X]))) =
  HSMul.hSMul (β := Multiset R) (p ^ n)
    (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])).roots)
Tactic: have H := roots_expand_pow (p := p) (n := n) (f := X - C y)
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
y : R
H :
  roots ((expand R (p ^ n) : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X]))) =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])).roots)
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (p ^ n)) ((C : (a : R) → R[X]) y : R[X])).roots =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))
have rwa : ∀
  (H :
    roots
        ((expand R (p ^ n) : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X]))) =
      HSMul.hSMul (β := Multiset R) (p ^ n)
        (Multiset.map (α := R) (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) {y})),
  (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (p ^ n)) ((C : (a : R) → R[X]) y : R[X])).roots =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))
Tactic: rwa [roots_X_sub_C, Multiset.map_singleton, map_sub, expand_X, expand_C] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
y : R
H :
  roots ((expand R (p ^ n) : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X]))) =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])).roots)
rwa :
  ∀
    (H :
      roots
          ((expand R (p ^ n) : (a : R[X]) → R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X]))) =
        HSMul.hSMul (β := Multiset R) (p ^ n)
          (Multiset.map (α := R) (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) {y})),
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (p ^ n)) ((C : (a : R) → R[X]) y : R[X])).roots =
      HSMul.hSMul (β := Multiset R) (p ^ n)
        (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (p ^ n)) ((C : (a : R) → R[X]) y : R[X])).roots =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))
have rwa₁ : ∀
  (H :
    roots
        ((expand R (p ^ n) : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X]))) =
      HSMul.hSMul (β := Multiset R) (p ^ n)
        (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))),
  (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (p ^ n)) ((C : (a : R) → R[X]) y : R[X])).roots =
    HSMul.hSMul (β := Multiset R) (p ^ n)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))
Tactic: rwa [roots_X_sub_C, Multiset.map_singleton, map_sub, expand_X, expand_C] at H
Cleared hypotheses: H