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
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))
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))
⊢ (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 :
    (HSub.hSub (α := R[X]) (β := R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) X : R[X])
          ((expand R (p ^ n) : (a : R[X]) → R[X]) ((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))
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))
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))
rwa₂ :
  ∀
    (H :
      (HSub.hSub (α := R[X]) (β := R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) X : R[X])
            ((expand R (p ^ n) : (a : R[X]) → R[X]) ((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))
⊢ (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 :
    (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X (p ^ n))
          ((expand R (p ^ n) : (a : R[X]) → R[X]) ((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))
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
m : ℕ
⊢ (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))
have 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))
Tactic: rw [roots_pow, roots_X_pow_char_pow_sub_C, mul_smul]
-- 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
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))
⊢ (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))
have 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))
Tactic: rw [roots_pow, roots_X_pow_char_pow_sub_C, mul_smul]
-- 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
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))
⊢ (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))
have 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))
Tactic: rw [roots_pow, roots_X_pow_char_pow_sub_C, mul_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (hypothesis)
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 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))
have 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))
Tactic: have H := roots_X_pow_char_pow_sub_C (p := p) (n := 1) (y := y)
-- 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
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))
⊢ (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))
have 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))
Tactic: rwa [pow_one, iterateFrobeniusEquiv_one] 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 : ℕ
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))
⊢ (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))
have 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))
Tactic: rwa [pow_one, iterateFrobeniusEquiv_one] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (hypothesis)
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 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))
have 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))
Tactic: have H := roots_X_pow_char_pow_sub_C_pow (p := p) (n := 1) (y := y) (m := m)
-- 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
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))
⊢ (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))
have 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))
Tactic: rwa [pow_one, iterateFrobeniusEquiv_one] 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 : ℕ
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))
⊢ (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))
have 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))
Tactic: rwa [pow_one, iterateFrobeniusEquiv_one] 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
f : R[X]
inst_3 : PerfectRing R p
⊢ 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 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
Tactic: simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']
-- 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
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
⊢ 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 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
Tactic: simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']
-- 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
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
⊢ 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 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
Tactic: simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']
-- 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
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
⊢ 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 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
Tactic: simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']
-- 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
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
⊢ 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 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
Tactic: simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']
-- 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
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
⊢ 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 simp_rw₅ : HSMul.hSMul (β := Multiset R) (p ^ n) (Multiset.map (fun (x : R) ↦ x) f.roots) = 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']
-- 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
inst_4 : 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 : toFinset
    (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
      (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
  f.roots.toFinset
Tactic: rw [Finset.image_toFinset, roots_expand_pow_map_iterateFrobenius,
    (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne']