-- Mathlib/FieldTheory/Fixed.lean
theorem of_eval₂ (f : Polynomial (FixedPoints.subfield G F))
    (hf : Polynomial.eval₂ (Subfield.subtype <| FixedPoints.subfield G F) x f = 0) :
    minpoly G F x ∣ f

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ minpoly G F x ∣ f

Tactic:
rw [← Polynomial.map_dvd_map' (Subfield.subtype <| FixedPoints.subfield G F), minpoly,
  ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ _, prodXSubSMul]

Result:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ ∏ g : G ⧸ stabilizer G x, (Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g)) ∣
    Polynomial.map (subfield G F).subtype f

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ ∏ g : G ⧸ stabilizer G x, (Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g)) ∣
    Polynomial.map (subfield G F).subtype f

Tactic:
refine
  Fintype.prod_dvd_of_coprime
    (Polynomial.pairwise_coprime_X_sub_C <| MulAction.injective_ofQuotientStabilizer G x) fun y =>
    QuotientGroup.induction_on y fun g => ?_

Result:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
y : G ⧸ stabilizer G x
g : G
⊢ Polynomial.X - Polynomial.C (ofQuotientStabilizer G x ↑g) ∣ Polynomial.map (subfield G F).subtype f

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ minpoly G F x ∣ f

Tactic:
classical
rw [← Polynomial.map_dvd_map' (Subfield.subtype <| FixedPoints.subfield G F), minpoly,
  ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ _, prodXSubSMul]
refine
  Fintype.prod_dvd_of_coprime
    (Polynomial.pairwise_coprime_X_sub_C <| MulAction.injective_ofQuotientStabilizer G x) fun y =>
    QuotientGroup.induction_on y fun g => ?_
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, ← MulSemiringActionHom.map_smul, smul_polynomial,
  MulSemiringActionHom.coe_polynomial, IsInvariantSubring.coe_subtypeHom',
  Polynomial.eval_map, Subfield.toSubring_subtype_eq_subtype, hf, smul_zero]

Result:
no goals

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
y : G ⧸ stabilizer G x
g : G
⊢ Polynomial.X - Polynomial.C (ofQuotientStabilizer G x ↑g) ∣ Polynomial.map (subfield G F).subtype 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, ← MulSemiringActionHom.map_smul, smul_polynomial,
  MulSemiringActionHom.coe_polynomial, IsInvariantSubring.coe_subtypeHom',
  Polynomial.eval_map, Subfield.toSubring_subtype_eq_subtype, hf, smul_zero]

Result:
no goals