-- 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))
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))
⊢ (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)) ((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