awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
x : F
f : g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F)
| HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)

Tactic:
rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]

Premises used: MulAction.toFun_apply, mul_inv_cancel_left, SemigroupAction.mul_smul, smul_mul'
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
f :
  ∀ (x : F), g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F)
| fun (x : F) ↦
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)

Tactic:
ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]

Premises used: MulAction.toFun_apply, mul_inv_cancel_left, SemigroupAction.mul_smul, smul_mul'
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
f :
  ∀ (x : F),
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)
f₁ :
  ∀ (x : F), g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F)
| fun (x : F) ↦
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)

Tactic:
· ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]

Premises used: MulAction.toFun_apply, mul_inv_cancel_left, SemigroupAction.mul_smul, smul_mul'
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
s₁ : s
f f₁ :
  fun (x : F) ↦
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)
| ∑ x ∈ s,
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)

Tactic:
congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]

Premises used: MulAction.toFun_apply, mul_inv_cancel_left, SemigroupAction.mul_smul, smul_mul'
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
h :
  Eq (α := F)
    (∑ x ∈ s,
      g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F))
    (∑ x ∈ s, HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F))
⊢ Eq (α := F)
    (∑ x ∈ s,
      HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F))
    (∑ x ∈ s, HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F))

Tactic:
conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]

Premises used: MulAction.toFun_apply, mul_inv_cancel_left, SemigroupAction.mul_smul, smul_mul'
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
h :
  Eq (α := F)
    (∑ x ∈ s,
      HSMul.hSMul (β := F) g
        ((fun (y : F) ↦
            HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) y : F) ((toFun G F : (a : F) → G → F) y : G → F))
          x (g⁻¹ * g')))
    (∑ x ∈ s,
      (fun (y : F) ↦
          HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) y : F) ((toFun G F : (a : F) → G → F) y : G → F))
        x g')
⊢ Eq (α := F)
    (∑ x ∈ s,
      g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F))
    (∑ x ∈ s, HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F))

Tactic:
change
    (∑ x ∈ s, g • (fun y => l y • MulAction.toFun G F y) x (g⁻¹ * g')) =
      ∑ x ∈ s, (fun y => l y • MulAction.toFun G F y) x g'

Premises used: HMul.hMul, Inv.inv, HSMul.hSMul, MulAction.toFun, DFunLike.coe, Finset.sum
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
h :
  HSMul.hSMul (β := F) g
      ((∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F))
        (g⁻¹ * g')) =
    (∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F)) g'
⊢ Eq (α := F)
    (∑ x ∈ s,
      HSMul.hSMul (β := F) g
        ((fun (y : F) ↦
            HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) y : F) ((toFun G F : (a : F) → G → F) y : G → F))
          x (g⁻¹ * g')))
    (∑ x ∈ s,
      (fun (y : F) ↦
          HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) y : F) ((toFun G F : (a : F) → G → F) y : G → F))
        x g')

Tactic:
rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]

Premises used: Finset.sum_apply, Finset.smul_sum, HSMul.hSMul, MulAction.toFun, DFunLike.coe
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
h : HSMul.hSMul (β := F) g ((toFun G F : (a : F) → G → F) a (g⁻¹ * g') : F) = (toFun G F : (a : F) → G → F) a g'
h₁ : g • (g⁻¹ * g') • a = (toFun G F : (a : F) → G → F) a g'
h₂ : g • (g⁻¹ * g') • a = g' • a
h₃ : (g * (g⁻¹ * g')) • a = g' • a
h₄ h₅ : g' • a = g' • a
⊢ HSMul.hSMul (β := F) g
      ((∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F))
        (g⁻¹ * g')) =
    (∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F)) g'

Tactic:
rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]

Premises used: MulAction.toFun_apply, smul_smul, mul_inv_cancel_left
-- 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
rw : Polynomial.Monic (prodXSubSMul G F x)
⊢ Polynomial.Monic (R := ↥(subfield G F))
    (Polynomial.toSubring (prodXSubSMul G F x) (Subfield.toSubring (subfield G F)) ⋯)

Tactic:
rw [Polynomial.monic_toSubring]

Premises used: Polynomial.monic_toSubring
-- 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
⊢ Polynomial.Monic (prodXSubSMul G F x)

Tactic:
prodXSubSMul.monic G F x

Premises used: prodXSubSMul.monic
-- 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
⊢ Polynomial.Monic (prodXSubSMul G F x)

Tactic:
exact prodXSubSMul.monic G F x

Premises used: prodXSubSMul.monic
-- 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
rw :
  Polynomial.eval x
      (Polynomial.map (R := ↥(Subfield.toSubring (subfield G F))) (Subring.subtype (Subfield.toSubring (subfield G F)))
        (minpoly G F x)) =
    Polynomial.eval x (prodXSubSMul G F x)
⊢ Polynomial.eval₂ (R := ↥(Subfield.toSubring (subfield G F))) (Subring.subtype (Subfield.toSubring (subfield G F))) x
      (minpoly G F x) =
    0

Tactic:
rw [← prodXSubSMul.eval G F x, Polynomial.eval₂_eq_eval_map]

Premises used: Polynomial.eval₂_eq_eval_map, prodXSubSMul.eval
-- 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
⊢ Polynomial.eval x
      (Polynomial.map (R := ↥(Subfield.toSubring (subfield G F))) (Subring.subtype (Subfield.toSubring (subfield G F)))
        (minpoly G F x)) =
    Polynomial.eval x (prodXSubSMul G F x)

Tactic:
simp only [minpoly, Polynomial.map_toSubring]

Premises used: FixedPoints.minpoly, Polynomial.map_toSubring
-- 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
⊢ Polynomial.eval₂ (R := ↥(subfield G F)) (Subfield.subtype (subfield G F)) x (minpoly G F x) = 0

Tactic:
eval₂ G F x

Premises used: Subfield.subtype, Set.Mem, Subring.subtype, Subfield.copy, FixedPoints.subfield, FixedPoints.minpoly.eval₂
-- 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
H : Eq (α := Polynomial ↥(subfield G F)) (minpoly G F x) 1
this :
  Polynomial.eval₂ (R := ↥(Subfield.toSubring (subfield G F))) (Subring.subtype (Subfield.toSubring (subfield G F))) x
      (minpoly G F x) =
    0
rwa :
  ∀
    (this :
      Polynomial.eval₂ (R := ↥(Subfield.toSubring (subfield G F))) (Subring.subtype (Subfield.toSubring (subfield G F)))
          x 1 =
        0),
    Eq.{v + 1} (α := F) 1 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : Eq.{v + 1} (α := F) 1 0), Eq.{v + 1} (α := F) 1 0
⊢ Eq.{v + 1} (α := F) 1 0

Tactic:
rwa [H, Polynomial.eval₂_one] at this

Premises used: Polynomial.eval₂_one
-- 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
rw :
  Dvd.dvd (α := Polynomial F)
    (∏ g : G ⧸ stabilizer G x,
      HSub.hSub (α := Polynomial F) (β := Polynomial F) Polynomial.X
        ((Polynomial.C : (a : F) → Polynomial F) (ofQuotientStabilizer G x g) : Polynomial F))
    (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f)
⊢ 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]

Premises used: Subfield.subtype, FixedPoints.minpoly, Subfield.toSubring_subtype_eq_subtype, FixedPoints.subfield, Polynomial.map_toSubring, Polynomial.map_dvd_map', prodXSubSMul
-- 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
⊢ Dvd.dvd (α := Polynomial F)
    (∏ g : G ⧸ stabilizer G x,
      HSub.hSub (α := Polynomial F) (β := Polynomial F) Polynomial.X
        ((Polynomial.C : (a : F) → Polynomial F) (ofQuotientStabilizer G x g) : Polynomial F))
    (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f)

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

Premises used: MulAction.injective_ofQuotientStabilizer, QuotientGroup.induction_on, Fintype.prod_dvd_of_coprime, Polynomial.pairwise_coprime_X_sub_C
-- 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
G₁ :
  ∀ (y : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G x)) (g : G),
    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
⊢ Dvd.dvd (α := Polynomial F)
    (∏ g : G ⧸ stabilizer G x,
      HSub.hSub (α := Polynomial F) (β := Polynomial F) Polynomial.X
        ((Polynomial.C : (a : F) → Polynomial F) (ofQuotientStabilizer G x g) : Polynomial F))
    (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) 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 => ?_

Premises used: MulAction.injective_ofQuotientStabilizer, QuotientGroup.induction_on, Fintype.prod_dvd_of_coprime, Polynomial.pairwise_coprime_X_sub_C
-- 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
rw :
  Polynomial.map (R := ↥(subfield G F)) (Subfield.subtype (subfield G F)) (minpoly G F x) ∣
    Polynomial.map (Subfield.subtype (subfield G F)) f
rw₁ :
  Polynomial.map (R := ↥(subfield G F)) (Subfield.subtype (subfield G F))
      (Polynomial.toSubring (prodXSubSMul G F x) (Subfield.toSubring (subfield G F)) ⋯) ∣
    Polynomial.map (Subfield.subtype (subfield G F)) f
rw₂ :
  Dvd.dvd (α := Polynomial F)
    (Polynomial.map (R := ↥(subfield G F)) (Subring.subtype (Subfield.toSubring (subfield G F)))
      (Polynomial.toSubring (prodXSubSMul G F x) (Subfield.toSubring (subfield G F)) ⋯))
    (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f)
rw₃ :
  Dvd.dvd (α := Polynomial F) (prodXSubSMul G F x)
    (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f)
rw₄ rw₅ rw₆ :
  Dvd.dvd (α := Polynomial F)
    (∏ g : G ⧸ stabilizer G x,
      HSub.hSub (α := Polynomial F) (β := Polynomial F) Polynomial.X
        ((Polynomial.C : (a : F) → Polynomial F) (ofQuotientStabilizer G x g) : Polynomial F))
    (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f)
rw₇ :
  ∀ (y : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G x)) (g : G),
    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
⊢ 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, ← map_smul, smul_polynomial,
    MulSemiringActionHom.coe_polynomial, IsInvariantSubring.coe_subtypeHom',
    Polynomial.eval_map, Subfield.toSubring_subtype_eq_subtype, hf, smul_zero]

Premises used: Subfield.subtype, Polynomial.eval_map, FixedPoints.minpoly, 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.map_toSubring, Polynomial.dvd_iff_isRoot, Polynomial.map_dvd_map', Polynomial.eval_smul', Subfield.toSubring, map_smul, prodXSubSMul
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
rw : f ∣ f * g
⊢ f ∣ minpoly G F x

Tactic:
rw [← hfg]
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
⊢ f ∣ f * g

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
⊢ f ∣ f * g

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
⊢ f ∣ minpoly G F x

Tactic:
have hf2 : f ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_right _ _
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
rw : g ∣ f * g
⊢ g ∣ minpoly G F x

Tactic:
rw [← hfg]
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ g ∣ f * g

Tactic:
dvd_mul_left _ _

Premises used: dvd_mul_left
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ g ∣ f * g

Tactic:
exact dvd_mul_left _ _

Premises used: dvd_mul_left
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ g ∣ minpoly G F x

Tactic:
have hg2 : g ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_left _ _
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
⊢ Polynomial.eval₂ (R := ↥(Subfield.toSubring (subfield G F))) (Subring.subtype (Subfield.toSubring (subfield G F))) x
      (minpoly G F x) =
    0

Tactic:
have := eval₂ G F x