awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ 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'
have h₃ : (g * (g⁻¹ * g')) • a = g' • a
Tactic: rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ 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'
have h₄ : g' • a = g' • a
Tactic: rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s : Finset F
⊢ LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
have have : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
Tactic: classical
  have : IsEmpty ((∅ : Finset F) : Set F) := by simp
  refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
  rw [coe_insert] at hs ⊢
  rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
  rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
  rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
  rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
  suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
    replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
    simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
    refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
    change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
    exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa
  intro i his g
  refine
    eq_of_sub_eq_zero
      (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) ?_ ⟨i, his⟩
          (mem_attach _ _) :
        _)
  refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
  ext g'; dsimp only
  conv_lhs =>
    rw [sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
  rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
  conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
  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'
  rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]
  rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s : Finset F
have : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
⊢ LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
have have₁ : ∀ (this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)),
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
Tactic: classical
  have : IsEmpty ((∅ : Finset F) : Set F) := by simp
  refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
  rw [coe_insert] at hs ⊢
  rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
  rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
  rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
  rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
  suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
    replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
    simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
    refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
    change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
    exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa
  intro i his g
  refine
    eq_of_sub_eq_zero
      (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) ?_ ⟨i, his⟩
          (mem_attach _ _) :
        _)
  refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
  ext g'; dsimp only
  conv_lhs =>
    rw [sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
  rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
  conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
  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'
  rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]
  rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s : Finset F
have : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
have₁ :
  ∀ (this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)),
    LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
      LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
have₂ : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
have₃ have₄ :
  ∀ (this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)),
    LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
      LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
⊢ LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
have have₅ : ∀ (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 (↑(insert a s) : Set F)),
  LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑(insert a s) : Set F)
Tactic: classical
  have : IsEmpty ((∅ : Finset F) : Set F) := by simp
  refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
  rw [coe_insert] at hs ⊢
  rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
  rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
  rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
  rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
  suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
    replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
    simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
    refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
    change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
    exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa
  intro i his g
  refine
    eq_of_sub_eq_zero
      (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) ?_ ⟨i, his⟩
          (mem_attach _ _) :
        _)
  refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
  ext g'; dsimp only
  conv_lhs =>
    rw [sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
  rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
  conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
  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'
  rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]
  rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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 (R := ↥(subfield G F))
    (Polynomial.toSubring (prodXSubSMul G F x) (Subfield.toSubring (subfield G F)) ⋯)
have rw : Polynomial.Monic (prodXSubSMul G F x)
Tactic: rw [Polynomial.monic_toSubring]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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.toSubring (subfield G F))) (Subring.subtype (Subfield.toSubring (subfield G F))) x
      (minpoly G F x) =
    0
have 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)
Tactic: rw [← prodXSubSMul.eval G F x, Polynomial.eval₂_eq_eval_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ Eq.{v + 1} (α := F) 1 0
have 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
Tactic: rwa [H, Polynomial.eval₂_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ Eq.{v + 1} (α := F) 1 0
have rwa₁ : ∀ (this : Eq.{v + 1} (α := F) 1 0), Eq.{v + 1} (α := F) 1 0
Tactic: rwa [H, Polynomial.eval₂_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ minpoly G F x ∣ f
have 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)
Tactic: rw [← Polynomial.map_dvd_map' (Subfield.subtype <| FixedPoints.subfield G F), minpoly,
    ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ _, prodXSubSMul]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
have 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
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 => ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ 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
have rw : Polynomial.IsRoot (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f)
  (ofQuotientStabilizer G x (↑g : G ⧸ stabilizer G x))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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))
⊢ 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
have rw₁ : Polynomial.eval (ofQuotientStabilizer G x (↑g : G ⧸ stabilizer G x))
    (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f) =
  0
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ 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
have rw₂ : Polynomial.eval (g • x) (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f) = 0
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ 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
have rw₃ : g •
    Polynomial.eval x
      (HSMul.hSMul (β := Polynomial F) g⁻¹ (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) f)) =
  0
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ 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
have 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
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]