-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (Subfield.subtype (subfield G F)) x f = 0
y : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G x)
g : G
rw :
  Polynomial.IsRoot (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f)
    (ofQuotientStabilizer G x (↑g : G ⧸ stabilizer G x))
rw₁ :
  Polynomial.eval (ofQuotientStabilizer G x (↑g : G ⧸ stabilizer G x))
      (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f) =
    0
rw₂ : Polynomial.eval (g • x) (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f) = 0
rw₃ :
  g •
      Polynomial.eval x
        (HSMul.hSMul (β := Polynomial F) g⁻¹ (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f)) =
    0
rw₄ :
  g •
      Polynomial.eval x
        (HSMul.hSMul (β := Polynomial F) g⁻¹
          (Polynomial.map
            (↑(IsInvariantSubring.subtypeHom G (Subfield.toSubring (subfield G F))) : ↥(subfield G F).toSubring →+* F)
            f)) =
    0
rw₅ :
  g •
      Polynomial.eval x
        (HSMul.hSMul (β := Polynomial F) g⁻¹
          ((MulSemiringActionHom.polynomial (IsInvariantSubring.subtypeHom G (Subfield.toSubring (subfield G F))) :
                (a : Polynomial ↥(subfield G F)) → Polynomial F)
              f :
            Polynomial F)) =
    0
rw₆ :
  g •
      Polynomial.eval x
        ((MulSemiringActionHom.polynomial (IsInvariantSubring.subtypeHom G (Subfield.toSubring (subfield G F))) :
            (a : Polynomial ↥(subfield G F)) → Polynomial F)
          (g⁻¹ • f)) =
    0
rw₇ :
  g •
      Polynomial.eval x
        ((MulSemiringActionHom.polynomial (IsInvariantSubring.subtypeHom G (Subfield.toSubring (subfield G F))) :
            (a : Polynomial ↥(subfield G F)) → Polynomial F)
          f) =
    0
rw₈ :
  g •
      Polynomial.eval x
        (Polynomial.map (↑(IsInvariantSubring.subtypeHom G (Subfield.toSubring (subfield G F))) : ↥(subfield G F) →+* F)
          f) =
    0
rw₉ : g • Polynomial.eval x (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f) = 0
rw₁₀ : g • Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0
rw₁₁ : g • Polynomial.eval₂ (Subfield.subtype (subfield G F)) x f = 0
rw₁₂ : HSMul.hSMul (β := F) g 0 = 0
rw₁₃ rw₁₄ : Eq.{v + 1} (α := F) 0 0
⊢ HSub.hSub (α := Polynomial F) (β := Polynomial F) Polynomial.X
      ((Polynomial.C : (a : F) → Polynomial F) (ofQuotientStabilizer G x (↑g : G ⧸ stabilizer G x)) : Polynomial F) ∣
    Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f

Tactic:
rw [Polynomial.dvd_iff_isRoot, Polynomial.IsRoot.def, MulAction.ofQuotientStabilizer_mk,
    Polynomial.eval_smul',
    ← IsInvariantSubring.coe_subtypeHom' G (FixedPoints.subfield G F).toSubring,
    ← MulSemiringActionHom.coe_polynomial, ← map_smul, smul_polynomial,
    MulSemiringActionHom.coe_polynomial, IsInvariantSubring.coe_subtypeHom',
    Polynomial.eval_map, Subfield.toSubring_subtype_eq_subtype, hf, smul_zero]

Premises used: Polynomial.eval_map, smul_zero, Polynomial.IsRoot.def, IsInvariantSubring.coe_subtypeHom', MulSemiringActionHom.coe_polynomial, FixedPoints.smul_polynomial, MulAction.ofQuotientStabilizer_mk, Subfield.toSubring_subtype_eq_subtype, FixedPoints.subfield, Polynomial.dvd_iff_isRoot, Polynomial.eval_smul', Subfield.toSubring, map_smul