awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Perfect
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
⊢ 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:
ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩

Premises used: Multiset.ext'
-- Module: Mathlib.FieldTheory.Perfect
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
⊢ 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:
exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩

Premises used: Multiset.ext'
-- Module: Mathlib.FieldTheory.Perfect
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
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
⊢ 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:
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'⟩

Premises used: Iff.mpr, Multiset.card_eq_zero, Nat.zero_le, Multiset.le_iff_count, Polynomial.rootMultiplicity_expand_pow, Multiset.count_eq_card_filter_eq, Polynomial.count_roots, Multiset.count_nsmul, Multiset.count_map, Multiset.ext', rfl
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
rw :
  Multiset.map (α := R) (⇑(iterateFrobenius R p 1) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f)) ≤
    p • f.roots
⊢ Multiset.map (α := R) (⇑(frobenius R p) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f)) ≤ p • f.roots

Tactic:
rw [← iterateFrobenius_one]

Premises used: iterateFrobenius_one
-- Module: Mathlib.FieldTheory.Perfect
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 (HPow.hPow (β := ℕ) p 1) : (a : R[X]) → R[X]) f)) ≤
    HPow.hPow (β := ℕ) p 1 • f.roots

Tactic:
roots_expand_pow_map_iterateFrobenius_le p 1 f

Premises used: Polynomial.roots_expand_pow_map_iterateFrobenius_le, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
h h₁ : HPow.hPow (β := ℕ) p 1 = p
⊢ Multiset.map (α := R) (⇑(iterateFrobenius R p 1) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f)) ≤
    p • f.roots

Tactic:
convert! ← roots_expand_pow_map_iterateFrobenius_le p 1 f

Premises used: Polynomial.roots_expand_pow_map_iterateFrobenius_le, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
⊢ HPow.hPow (β := ℕ) p 1 = p

Tactic:
apply pow_one

Premises used: pow_one
-- Module: Mathlib.FieldTheory.Perfect
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
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
⊢ 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

Tactic:
rw [Finset.image_toFinset, ← (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne',
    toFinset_subset]

Premises used: Polynomial.roots, Finset.image_toFinset, Multiset.toFinset_nsmul, LT.lt.ne', expChar_pow_pos, Multiset.toFinset_subset
-- Module: Mathlib.FieldTheory.Perfect
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
⊢ 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:
subset_of_le (roots_expand_pow_map_iterateFrobenius_le p n f)

Premises used: Multiset.subset_of_le, Polynomial.roots_expand_pow_map_iterateFrobenius_le
-- Module: Mathlib.FieldTheory.Perfect
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
⊢ 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:
exact subset_of_le (roots_expand_pow_map_iterateFrobenius_le p n f)

Premises used: Multiset.subset_of_le, Polynomial.roots_expand_pow_map_iterateFrobenius_le
-- Module: Mathlib.FieldTheory.Perfect
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
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
⊢ Finset.image (α := R) (⇑(frobenius R p) : (a : R) → R) (toFinset (roots ((expand R p : (a : R[X]) → R[X]) f))) ⊆
    f.roots.toFinset

Tactic:
rw [← iterateFrobenius_one]

Premises used: iterateFrobenius_one
-- Module: Mathlib.FieldTheory.Perfect
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 (HPow.hPow (β := ℕ) p 1) : (a : R[X]) → R[X]) f))) ⊆
    f.roots.toFinset

Tactic:
roots_expand_pow_image_iterateFrobenius_subset p 1 f

Premises used: Polynomial.roots_expand_pow_image_iterateFrobenius_subset, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Perfect
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
h : HPow.hPow (β := ℕ) p 1 = p
⊢ 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:
convert! ← roots_expand_pow_image_iterateFrobenius_subset p 1 f

Premises used: Polynomial.roots_expand_pow_image_iterateFrobenius_subset, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Perfect
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
⊢ HPow.hPow (β := ℕ) p 1 = p

Tactic:
apply pow_one

Premises used: pow_one
-- Module: Mathlib.FieldTheory.Perfect
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)

Tactic:
ext' fun r ↦ ?_

Premises used: Multiset.ext'
-- Module: Mathlib.FieldTheory.Perfect
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)

Tactic:
refine ext' fun r ↦ ?_

Premises used: Multiset.ext'
-- Module: Mathlib.FieldTheory.Perfect
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
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
⊢ 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:
rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
    count_eq_card_filter_eq]

Premises used: Polynomial.rootMultiplicity_expand_pow, Multiset.count_eq_card_filter_eq, Polynomial.count_roots, Multiset.count_nsmul, Multiset.count_map
-- Module: Mathlib.FieldTheory.Perfect
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
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
⊢ 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:
congr
-- Module: Mathlib.FieldTheory.Perfect
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
e_a : ∀ (x : R), r ^ p ^ n = x ↔ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x
⊢ 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:
ext
-- Module: Mathlib.FieldTheory.Perfect
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 x : R
⊢ r ^ p ^ n = x ↔ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x

Tactic:
(iterateFrobeniusEquiv R p n).eq_symm_apply.symm

Premises used: iterateFrobeniusEquiv, RingEquiv.eq_symm_apply, Iff.symm
-- Module: Mathlib.FieldTheory.Perfect
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 x : R
⊢ r ^ p ^ n = x ↔ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x

Tactic:
exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm

Premises used: iterateFrobeniusEquiv, RingEquiv.eq_symm_apply, Iff.symm
-- Module: Mathlib.FieldTheory.Perfect
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
e_a₂ : ∀ (r x : R), r ^ p ^ n = x ↔ r = (RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x
⊢ 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)

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

Premises used: iterateFrobeniusEquiv, Polynomial.rootMultiplicity_expand_pow, Multiset.count_eq_card_filter_eq, Polynomial.count_roots, Multiset.count_nsmul, Multiset.count_map, RingEquiv.eq_symm_apply, Iff.symm, Multiset.ext'
-- Module: Mathlib.FieldTheory.Perfect
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
rw :
  HSMul.hSMul (β := Multiset R) p
    (Multiset.map (⇑(HPow.hPow (α := R ≃+* R) (β := ℕ) (frobeniusEquiv R p) 1).symm : (a : R) → R) f.roots)
| roots ((expand R p : (a : R[X]) → R[X]) f)

Tactic:
rw [← pow_one p, roots_expand_pow, iterateFrobeniusEquiv_eq_pow, pow_one]

Premises used: iterateFrobeniusEquiv_eq_pow, pow_one, Polynomial.roots_expand_pow
-- Module: Mathlib.FieldTheory.Perfect
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
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)
⊢ 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)

Tactic:
conv_lhs => rw [← pow_one p, roots_expand_pow, iterateFrobeniusEquiv_eq_pow, pow_one]

Premises used: iterateFrobeniusEquiv_eq_pow, pow_one, Polynomial.roots_expand_pow
-- Module: Mathlib.FieldTheory.Perfect
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
⊢ 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:
rfl
-- Module: Mathlib.FieldTheory.Perfect
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
⊢ 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)
-- Module: Mathlib.FieldTheory.Perfect
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
m : ℕ
rw :
  m • (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (p ^ n)) ((C : (a : R) → R[X]) y : R[X])).roots =
    HSMul.hSMul (β := Multiset R) (m * p ^ n)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))
rw₁ :
  m •
      HSMul.hSMul (β := Multiset R) (p ^ n)
        (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R)) =
    HSMul.hSMul (β := Multiset R) (m * p ^ n)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))
rw₂ rw₃ :
  m •
      HSMul.hSMul (β := Multiset R) (p ^ n)
        (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R)) =
    m •
      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]) ^ m).roots =
    HSMul.hSMul (β := Multiset R) (m * p ^ n)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) y : R))

Tactic:
rw [roots_pow, roots_X_pow_char_pow_sub_C, mul_smul]

Premises used: Polynomial.roots_pow, SemigroupAction.mul_smul, Polynomial.roots_X_pow_char_pow_sub_C
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
y : R
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (HPow.hPow (β := ℕ) p 1)) ((C : (a : R) → R[X]) y : R[X])).roots =
    HSMul.hSMul (β := Multiset R) (HPow.hPow (β := ℕ) p 1)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p 1) : (a : R) → R) y : R))

Tactic:
have H := roots_X_pow_char_pow_sub_C (p := p) (n := 1) (y := y)
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
y : R
H :
  (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (HPow.hPow (β := ℕ) p 1)) ((C : (a : R) → R[X]) y : R[X])).roots =
    HSMul.hSMul (β := Multiset R) (HPow.hPow (β := ℕ) p 1)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p 1) : (a : R) → R) y : R))
rwa :
  ∀
    (H :
      (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X])).roots =
        HSMul.hSMul (β := Multiset R) p
          (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p 1) : (a : R) → R) y : R))),
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X])).roots =
      HSMul.hSMul (β := Multiset R) p (singleton (α := R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) y : R))
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (H :
      (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X])).roots =
        HSMul.hSMul (β := Multiset R) p
          (singleton (α := R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) y : R))),
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X])).roots =
      HSMul.hSMul (β := Multiset R) p (singleton (α := R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) y : R))
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X])).roots =
    HSMul.hSMul (β := Multiset R) p (singleton (α := R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) y : R))

Tactic:
rwa [pow_one, iterateFrobeniusEquiv_one] at H

Premises used: iterateFrobeniusEquiv_one, pow_one
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
y : R
m : ℕ
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (HPow.hPow (β := ℕ) p 1)) ((C : (a : R) → R[X]) y : R[X]) ^ m).roots =
    HSMul.hSMul (β := Multiset R) (m * HPow.hPow (β := ℕ) p 1)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p 1) : (a : R) → R) y : R))

Tactic:
have H := roots_X_pow_char_pow_sub_C_pow (p := p) (n := 1) (y := y) (m := m)
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
y : R
m : ℕ
H :
  (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (HPow.hPow (β := ℕ) p 1)) ((C : (a : R) → R[X]) y : R[X]) ^ m).roots =
    HSMul.hSMul (β := Multiset R) (m * HPow.hPow (β := ℕ) p 1)
      (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p 1) : (a : R) → R) y : R))
rwa :
  ∀
    (H :
      (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X]) ^ m).roots =
        HSMul.hSMul (β := Multiset R) (m * p)
          (singleton (α := R) ((RingEquiv.symm (iterateFrobeniusEquiv R p 1) : (a : R) → R) y : R))),
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X]) ^ m).roots =
      HSMul.hSMul (β := Multiset R) (m * p)
        (singleton (α := R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) y : R))
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (H :
      (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X]) ^ m).roots =
        HSMul.hSMul (β := Multiset R) (m * p)
          (singleton (α := R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) y : R))),
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X]) ^ m).roots =
      HSMul.hSMul (β := Multiset R) (m * p)
        (singleton (α := R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) y : R))
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X p) ((C : (a : R) → R[X]) y : R[X]) ^ m).roots =
    HSMul.hSMul (β := Multiset R) (m * p)
      (singleton (α := R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) y : R))

Tactic:
rwa [pow_one, iterateFrobeniusEquiv_one] at H

Premises used: iterateFrobeniusEquiv_one, pow_one
-- Module: Mathlib.FieldTheory.Perfect
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
simp_rw :
  Multiset.map (fun (x : R) ↦ (iterateFrobeniusEquiv R p n : (a : R) → R) x)
      (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) =
    p ^ n • f.roots
simp_rw₁ :
  Multiset.map (fun (x : R) ↦ (iterateFrobeniusEquiv R p n : (a : R) → R) x)
      (HSMul.hSMul (β := Multiset R) (p ^ n)
        (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots)) =
    p ^ n • f.roots
simp_rw₂ :
  HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map (fun (x : R) ↦ (iterateFrobeniusEquiv R p n : (a : R) → R) x)
        (Multiset.map (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R) f.roots)) =
    p ^ n • f.roots
simp_rw₃ :
  HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map
        ((fun (x : R) ↦ (iterateFrobeniusEquiv R p n : (a : R) → R) x) ∘
          (⇑(RingEquiv.symm (iterateFrobeniusEquiv R p n)) : (a : R) → R))
        f.roots) =
    p ^ n • f.roots
simp_rw₄ :
  HSMul.hSMul (β := Multiset R) (p ^ n)
      (Multiset.map
        (fun (x : R) ↦
          (iterateFrobeniusEquiv R p n : (a : R) → R)
            ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R))
        f.roots) =
    p ^ n • f.roots
simp_rw₅ : HSMul.hSMul (β := Multiset R) (p ^ n) (Multiset.map (fun (x : R) ↦ x) f.roots) = 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

Tactic:
simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']

Premises used: RingEquiv.apply_symm_apply, Multiset.map_map, Multiset.map_id', Function.comp_apply, Polynomial.roots_expand_pow, coe_iterateFrobeniusEquiv, Multiset.map_nsmul
-- Module: Mathlib.FieldTheory.Perfect
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
⊢ Multiset.map (α := R) (⇑(frobenius R p) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f)) = p • f.roots

Tactic:
simp [roots_expand, Multiset.map_nsmul]

Premises used: Polynomial.roots_expand, Multiset.map_nsmul