-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand_pow_map_iterateFrobenius_le :
    (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) ≤ p ^ n • f.roots

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h : ¬∃ s, r = s ^ p ^ n
⊢ count r (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤ count r (p ^ n • f.roots)

Tactic:
convert Nat.zero_le _

Result:
case h.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h : ¬∃ s, r = s ^ p ^ n
⊢ count r (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ count r (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤ count r (p ^ n • f.roots)

Tactic:
by_cases h : ∃ s, r = s ^ p ^ n

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h : ∃ s, r = s ^ p ^ n
⊢ count r (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤ count r (p ^ n • f.roots)

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h : ¬∃ s, r = s ^ p ^ n
⊢ count r (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤ count r (p ^ n • f.roots)

Proof state:
case h.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h : ¬∃ s, r = s ^ p ^ n
⊢ filter (fun a => r = (iterateFrobenius R p n) a) ((expand R (p ^ n)) f).roots = 0

Tactic:
exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots ≤ p ^ n • f.roots

Tactic:
refine le_iff_count.2 fun r ↦ ?_

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ count r (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤ count r (p ^ n • f.roots)

Proof state:
case pos.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
s : R
⊢ (filter (fun a => s ^ p ^ n = (iterateFrobenius R p n) a) ((expand R (p ^ n)) f).roots).card ≤
    (filter (fun x => s = x) ((expand R (p ^ n)) f).roots).card

Tactic:
exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h : ¬∃ s, r = s ^ p ^ n
⊢ count r (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) = 0

Tactic:
simp_rw [count_map, card_eq_zero]

Result:
case h.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h : ¬∃ s, r = s ^ p ^ n
⊢ filter (fun a => r = (iterateFrobenius R p n) a) ((expand R (p ^ n)) f).roots = 0

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h : ∃ s, r = s ^ p ^ n
⊢ count r (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤ count r (p ^ n • f.roots)

Tactic:
obtain ⟨s, rfl⟩ := h

Result:
case pos.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
s : R
⊢ count (s ^ p ^ n) (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤
    count (s ^ p ^ n) (p ^ n • f.roots)

Proof state:
case pos.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
s : R
⊢ count (s ^ p ^ n) (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤
    count (s ^ p ^ n) (p ^ n • f.roots)

Tactic:
simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
  count_eq_card_filter_eq]

Result:
case pos.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
s : R
⊢ (filter (fun a => s ^ p ^ n = (iterateFrobenius R p n) a) ((expand R (p ^ n)) f).roots).card ≤
    (filter (fun x => s = x) ((expand R (p ^ n)) f).roots).card