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
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 : Polynomial.map (R := ↥(subfield G F)) (Subfield.subtype (subfield G F)) (minpoly G F x) ∣
  Polynomial.map (Subfield.subtype (subfield G F)) 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]
-- 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
rw :
  Polynomial.map (R := ↥(subfield G F)) (Subfield.subtype (subfield G F)) (minpoly G F x) ∣
    Polynomial.map (Subfield.subtype (subfield G F)) f
⊢ minpoly G F x ∣ f
have rw₁ : Polynomial.map (R := ↥(subfield G F)) (Subfield.subtype (subfield G F))
    (Polynomial.toSubring (prodXSubSMul G F x) (Subfield.toSubring (subfield G F)) sorry) ∣
  Polynomial.map (Subfield.subtype (subfield G F)) 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]
-- 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
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
⊢ minpoly G F x ∣ f
have 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)) sorry))
  (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) 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]
-- 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
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)
⊢ minpoly G F x ∣ f
have rw₃ : Dvd.dvd (α := Polynomial F) (prodXSubSMul G F x)
  (Polynomial.map (Subring.subtype (Subfield.toSubring (subfield G F))) 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]
-- 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
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)
⊢ 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: 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]
-- 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
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)
⊢ minpoly G F x ∣ f
have 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
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]
-- 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 g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
⊢ f ∣ minpoly G F x
have rw : f ∣ f * g
Tactic: rw [← hfg]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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 = 1 ∨ g = 1
have hf2 : f ∣ minpoly G F x
Tactic: have hf2 : f ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_right _ _
-- 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 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
have rw : g ∣ f * g
Tactic: rw [← hfg]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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
⊢ f = 1 ∨ g = 1
have hg2 : g ∣ minpoly G F x
Tactic: have hg2 : g ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_left _ _
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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
⊢ f = 1 ∨ g = 1
have this : 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
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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
this :
  Polynomial.eval₂ (R := ↥(Subfield.toSubring (subfield G F))) (Subring.subtype (Subfield.toSubring (subfield G F))) x
      (minpoly G F x) =
    0
⊢ f = 1 ∨ g = 1
have this₁ : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0 ∨
  Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
Tactic: rw [← hfg, Polynomial.eval₂_mul, mul_eq_zero] 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 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
this :
  Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0 ∨
    Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
⊢ f = 1 ∨ g = 1
have inl : ∀ (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0), f = 1 ∨ g = 1
Tactic: rcases this with this | 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 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
this :
  Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0 ∨
    Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
inl : ∀ (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0), f = 1 ∨ g = 1
⊢ f = 1 ∨ g = 1
have inr : ∀ (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0), f = 1 ∨ g = 1
Tactic: rcases this with this | 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 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0
⊢ f = 1 ∨ g = 1
have inl : g = 1
Tactic: right
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0
⊢ g = 1
have hf3 : f = minpoly G F x
Tactic: have hf3 : f = minpoly G F x :=
      Polynomial.eq_of_monic_of_associated hf (monic G F x)
        (associated_of_dvd_dvd hf2 <| @of_eval₂ G _ F _ _ _ x f 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 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0
hf3 : f = minpoly G F x
⊢ g = 1
have inl : ∀ (hfg : f * g = HMul.hMul (α := Polynomial ↥(subfield G F)) (minpoly G F x) 1) (hf2 : f ∣ minpoly G F x)
  (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0)
  (hf3 : f = minpoly G F x), g = 1
Tactic: rwa [← mul_one (minpoly G F x), hf3, mul_right_inj' (monic G F x).ne_zero] at hfg
Cleared hypotheses: hfg, hf2, hg2, this, hf3
-- 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 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0
hf3 : f = minpoly G F x
inl :
  ∀ (hfg : f * g = HMul.hMul (α := Polynomial ↥(subfield G F)) (minpoly G F x) 1) (hf2 : f ∣ minpoly G F x)
    (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0)
    (hf3 : f = minpoly G F x), g = 1
⊢ g = 1
have inl₁ : ∀ (hfg : minpoly G F x * g = HMul.hMul (α := Polynomial ↥(subfield G F)) (minpoly G F x) 1) (hf2 : f ∣ minpoly G F x)
  (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0)
  (hf3 : f = minpoly G F x), g = 1
Tactic: rwa [← mul_one (minpoly G F x), hf3, mul_right_inj' (monic G F x).ne_zero] at hfg
Cleared hypotheses: hfg, hf2, hg2, this, hf3
-- 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 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0
hf3 : f = minpoly G F x
inl :
  ∀ (hfg : f * g = HMul.hMul (α := Polynomial ↥(subfield G F)) (minpoly G F x) 1) (hf2 : f ∣ minpoly G F x)
    (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0)
    (hf3 : f = minpoly G F x), g = 1
inl₁ :
  ∀ (hfg : minpoly G F x * g = HMul.hMul (α := Polynomial ↥(subfield G F)) (minpoly G F x) 1) (hf2 : f ∣ minpoly G F x)
    (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0)
    (hf3 : f = minpoly G F x), g = 1
⊢ g = 1
have inl₂ : ∀ (hfg : g = 1) (hf2 : f ∣ minpoly G F x) (hg2 : g ∣ minpoly G F x)
  (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0) (hf3 : f = minpoly G F x),
  g = 1
Tactic: rwa [← mul_one (minpoly G F x), hf3, mul_right_inj' (monic G F x).ne_zero] at hfg
Cleared hypotheses: hfg, hf2, hg2, this, hf3
-- 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 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
⊢ f = 1 ∨ g = 1
have inr : f = 1
Tactic: left
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
⊢ f = 1
have hg3 : g = minpoly G F x
Tactic: have hg3 : g = minpoly G F x :=
      Polynomial.eq_of_monic_of_associated hg (monic G F x)
        (associated_of_dvd_dvd hg2 <| @of_eval₂ G _ F _ _ _ x g 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 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
hg3 : g = minpoly G F x
⊢ f = 1
have inr : ∀ (hfg : f * g = HMul.hMul (α := Polynomial ↥(subfield G F)) 1 (minpoly G F x)) (hf2 : f ∣ minpoly G F x)
  (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0)
  (hg3 : g = minpoly G F x), f = 1
Tactic: rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg
Cleared hypotheses: hfg, hf2, hg2, this, hg3
-- 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 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
hg3 : g = minpoly G F x
inr :
  ∀ (hfg : f * g = HMul.hMul (α := Polynomial ↥(subfield G F)) 1 (minpoly G F x)) (hf2 : f ∣ minpoly G F x)
    (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0)
    (hg3 : g = minpoly G F x), f = 1
⊢ f = 1
have inr₁ : ∀ (hfg : f * minpoly G F x = HMul.hMul (α := Polynomial ↥(subfield G F)) 1 (minpoly G F x)) (hf2 : f ∣ minpoly G F x)
  (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0)
  (hg3 : g = minpoly G F x), f = 1
Tactic: rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg
Cleared hypotheses: hfg, hf2, hg2, this, hg3
-- 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 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
hg3 : g = minpoly G F x
inr :
  ∀ (hfg : f * g = HMul.hMul (α := Polynomial ↥(subfield G F)) 1 (minpoly G F x)) (hf2 : f ∣ minpoly G F x)
    (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0)
    (hg3 : g = minpoly G F x), f = 1
inr₁ :
  ∀ (hfg : f * minpoly G F x = HMul.hMul (α := Polynomial ↥(subfield G F)) 1 (minpoly G F x)) (hf2 : f ∣ minpoly G F x)
    (hg2 : g ∣ minpoly G F x) (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0)
    (hg3 : g = minpoly G F x), f = 1
⊢ f = 1
have inr₂ : ∀ (hfg : f = 1) (hf2 : f ∣ minpoly G F x) (hg2 : g ∣ minpoly G F x)
  (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0) (hg3 : g = minpoly G F x),
  f = 1
Tactic: rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg
Cleared hypotheses: hfg, hf2, hg2, this, hg3
-- 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 : Finite G
x : F
⊢ IsIntegral (↥(subfield G F)) x
have intro : ∀ (val : Fintype G), IsIntegral (↥(subfield G F)) x
Tactic: cases nonempty_fintype G