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
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
⊢ 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

Premises used: mul_eq_zero, Polynomial.eval₂_mul
-- 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
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
inr : ∀ (this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0), f = 1 ∨ g = 1
⊢ f = 1 ∨ g = 1

Tactic:
rcases this with this | this
-- 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0
inl : g = 1
⊢ f = 1 ∨ g = 1

Tactic:
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
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x f = 0
⊢ 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)
-- 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
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
inl₂ inl₃ inl₄ 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
⊢ g = 1

Tactic:
rwa [← mul_one (minpoly G F x), hf3, mul_right_inj' (monic G F x).ne_zero] at hfg

Premises used: FixedPoints.minpoly.monic, FixedPoints.minpoly, mul_right_inj', mul_one, Polynomial.Monic.ne_zero
-- 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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
inr : f = 1
⊢ f = 1 ∨ g = 1

Tactic:
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
this : Polynomial.eval₂ (Subring.subtype (Subfield.toSubring (subfield G F))) x g = 0
⊢ 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)
-- 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
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
inr₂ inr₃ inr₄ 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
⊢ f = 1

Tactic:
rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg

Premises used: FixedPoints.minpoly.monic, FixedPoints.minpoly, mul_left_inj', one_mul, Polynomial.Monic.ne_zero
-- 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
⊢ Irreducible (M := Polynomial ↥(subfield G F)) (minpoly G F x)

Tactic:
(Polynomial.irreducible_of_monic (monic G F x) (ne_one G F x)).2 (irreducible_aux G F x)

Premises used: Iff.mpr, FixedPoints.minpoly.monic, Polynomial.irreducible_of_monic, FixedPoints.minpoly.irreducible_aux, FixedPoints.minpoly.ne_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 : Finite G
x : F
intro : ∀ (val : Fintype G), IsIntegral (↥(subfield G F)) x
⊢ IsIntegral (↥(subfield G F)) x

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- 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 : Finite G
x : F
val : Fintype G
⊢ IsIntegral (↥(subfield G F)) x

Tactic:
⟨minpoly G F x, minpoly.monic G F x, minpoly.eval₂ G F x⟩

Premises used: FixedPoints.minpoly.monic, FixedPoints.minpoly, RingHom.IsIntegralElem, IsIntegral, And.intro, Exists.intro, 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 : Finite G
x : F
val : Fintype G
⊢ IsIntegral (↥(subfield G F)) x

Tactic:
exact ⟨minpoly G F x, minpoly.monic G F x, minpoly.eval₂ G F x⟩
-- 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
⊢ Eq (α := Polynomial ↥(subfield G F)) (minpoly G F x) (_root_.minpoly (↥(subfield G F)) x)

Tactic:
minpoly.eq_of_irreducible_of_monic (minpoly.irreducible G F x) (minpoly.eval₂ G F x)
    (minpoly.monic G F x)

Premises used: FixedPoints.minpoly.monic, FixedPoints.minpoly.irreducible, minpoly.eq_of_irreducible_of_monic, 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
s : Finset F
hs : LinearIndependent ↥(subfield G F) (M := F) fun (i : ↥s) ↦ (↑i : F)
⊢ #s ≤ Fintype.card G

Tactic:
simpa only [rank_fun', Cardinal.mk_coe_finset, Finset.coe_sort_coe, Cardinal.lift_natCast,
      Nat.cast_le] using
      (linearIndependent_smul_of_linearIndependent G F hs).cardinal_lift_le_rank

Premises used: Finset.coe_sort_coe, LinearIndependent.cardinal_lift_le_rank, Cardinal.mk_coe_finset, Cardinal.lift_natCast, FixedPoints.linearIndependent_smul_of_linearIndependent, Nat.cast_le, rank_fun'
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
intro :
  ∀ (val : Fintype G),
    Polynomial.Splits
      (Polynomial.map (R := ↥(subfield G F)) (algebraMap (↥(subfield G F)) F) (_root_.minpoly (↥(subfield G F)) x))
⊢ Polynomial.Splits
    (Polynomial.map (R := ↥(subfield G F)) (algebraMap (↥(subfield G F)) F) (_root_.minpoly (↥(subfield G F)) x))

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
val : Fintype G
intro :
  Polynomial.Splits.{v} (R := 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.Splits
    (Polynomial.map (R := ↥(subfield G F)) (algebraMap (↥(subfield G F)) F) (_root_.minpoly (↥(subfield G F)) x))

Tactic:
rw [← minpoly_eq_minpoly, minpoly, coe_algebraMap, ← Subfield.toSubring_subtype_eq_subtype,
      Polynomial.map_toSubring _ (subfield G F).toSubring, prodXSubSMul]

Premises used: FixedPoints.minpoly, Subfield.toSubring_subtype_eq_subtype, FixedPoints.subfield, FixedPoints.minpoly_eq_minpoly, Polynomial.map_toSubring, FixedPoints.coe_algebraMap, Subfield.toSubring, prodXSubSMul
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
val : Fintype G
⊢ Polynomial.Splits.{v} (R := 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))

Tactic:
Polynomial.Splits.prod fun _ _ => Polynomial.Splits.X_sub_C _

Premises used: MulAction.ofQuotientStabilizer, Polynomial.Splits.X_sub_C, Polynomial.Splits.prod
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
val : Fintype G
⊢ Polynomial.Splits.{v} (R := 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))

Tactic:
exact Polynomial.Splits.prod fun _ _ => Polynomial.Splits.X_sub_C _

Premises used: Polynomial.Splits.prod
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
intro : ∀ (val : Fintype G), IsSeparable (↥(subfield G F)) x
⊢ IsSeparable (↥(subfield G F)) x

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
val : Fintype G
intro : Polynomial.Separable (prodXSubSMul G F x)
⊢ IsSeparable (↥(subfield G F)) x

Tactic:
rw [IsSeparable, ← minpoly_eq_minpoly,
      ← Polynomial.separable_map (FixedPoints.subfield G F).subtype, minpoly,
      ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ (subfield G F).toSubring]

Premises used: Subfield.subtype, FixedPoints.minpoly, Subfield.toSubring_subtype_eq_subtype, FixedPoints.subfield, FixedPoints.minpoly_eq_minpoly, Polynomial.map_toSubring, IsSeparable, Subfield.toSubring, Polynomial.separable_map
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
val : Fintype G
⊢ Polynomial.Separable (prodXSubSMul G F x)

Tactic:
Polynomial.separable_prod_X_sub_C_iff.2 (injective_ofQuotientStabilizer G x)

Premises used: Iff.mpr, Polynomial.separable_prod_X_sub_C_iff, MulAction.injective_ofQuotientStabilizer, prodXSubSMul
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
val : Fintype G
⊢ Polynomial.Separable (prodXSubSMul G F x)

Tactic:
exact Polynomial.separable_prod_X_sub_C_iff.2 (injective_ofQuotientStabilizer G x)

Premises used: Iff.mpr, Polynomial.separable_prod_X_sub_C_iff, MulAction.injective_ofQuotientStabilizer
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
⊢ Algebra.IsSeparable (↥(subfield G F)) F

Tactic:
exact ⟨fun x => by
    cases nonempty_fintype G
    rw [IsSeparable, ← minpoly_eq_minpoly,
      ← Polynomial.separable_map (FixedPoints.subfield G F).subtype, minpoly,
      ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ (subfield G F).toSubring]
    exact Polynomial.separable_prod_X_sub_C_iff.2 (injective_ofQuotientStabilizer G x)⟩
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
⊢ Algebra.IsSeparable (↥(subfield G F)) F

Tactic:
classical
  exact ⟨fun x => by
    cases nonempty_fintype G
    rw [IsSeparable, ← minpoly_eq_minpoly,
      ← Polynomial.separable_map (FixedPoints.subfield G F).subtype, minpoly,
      ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ (subfield G F).toSubring]
    exact Polynomial.separable_prod_X_sub_C_iff.2 (injective_ofQuotientStabilizer G x)⟩
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
intro : ∀ (val : Fintype G), FiniteDimensional (↥(subfield G F)) F
⊢ FiniteDimensional (↥(subfield G F)) F

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
val : Fintype G
⊢ FiniteDimensional (↥(subfield G F)) F

Tactic:
IsNoetherian.iff_fg.1
    (IsNoetherian.iff_rank_lt_aleph0.2 <| (rank_le_card G F).trans_lt Cardinal.natCast_lt_aleph0)

Premises used: Iff.mpr, IsNoetherian.iff_rank_lt_aleph0, FixedPoints.rank_le_card, Cardinal.natCast_lt_aleph0, IsNoetherian.iff_fg, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
val : Fintype G
⊢ FiniteDimensional (↥(subfield G F)) F

Tactic:
exact IsNoetherian.iff_fg.1
    (IsNoetherian.iff_rank_lt_aleph0.2 <| (rank_le_card G F).trans_lt Cardinal.natCast_lt_aleph0)

Premises used: Iff.mpr, IsNoetherian.iff_rank_lt_aleph0, FixedPoints.rank_le_card, Cardinal.natCast_lt_aleph0, IsNoetherian.iff_fg, Iff.mp, LE.le.trans_lt
-- 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
rw : Module.rank (↥(subfield G F)) F ≤ (↑(Fintype.card G) : Cardinal.{v})
⊢ finrank (↥(subfield G F)) F ≤ Fintype.card G

Tactic:
rw [← @Nat.cast_le Cardinal, finrank_eq_rank]

Premises used: Module.finrank_eq_rank, Nat.cast_le
-- 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
⊢ Module.rank (↥(subfield G F)) F ≤ (↑(Fintype.card G) : Cardinal.{v})

Tactic:
apply rank_le_card

Premises used: FixedPoints.rank_le_card
-- Module: Mathlib.FieldTheory.Fixed
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : IsDomain B
inst_5 : Algebra R B
⊢ LinearIndependent (ι := A →ₐ[R] B) B AlgHom.toLinearMap

Tactic:
have : LinearIndependent B (LinearMap.ltoFun R A B B ∘ AlgHom.toLinearMap) :=
    ((linearIndependent_monoidHom A B).comp ((↑) : (A →ₐ[R] B) → A →* B) fun _ _ hfg =>
        AlgHom.ext fun _ => DFunLike.ext_iff.1 hfg _ :
      _)
  this.of_comp _

Premises used: LinearMap.ltoFun, linearIndependent_monoidHom, MonoidHomClass.toMonoidHom, DFunLike.ext_iff, AlgHom.ext, LinearIndependent.of_comp, Iff.mp, LinearIndependent.comp
-- Module: Mathlib.FieldTheory.Fixed
Goal:
K : Type u
V : Type v
W : Type w
inst : Field K
inst_1 : Ring V
inst_2 : Algebra K V
inst_3 : FiniteDimensional K V
inst_4 : Field W
inst_5 : Algebra K W
⊢ Cardinal.mk (V →ₐ[K] W) ≤ (↑(finrank W (V →ₗ[K] W)) : Cardinal.{max w v})

Tactic:
(linearIndependent_toLinearMap K V W).cardinalMk_le_finrank

Premises used: linearIndependent_toLinearMap, LinearIndependent.cardinalMk_le_finrank
-- Module: Mathlib.FieldTheory.Fixed
Goal:
K : Type u
V : Type v
inst : Field K
inst_1 : Field V
inst_2 : Algebra K V
inst_3 : FiniteDimensional K V
⊢ Fintype.card.{v} (V →ₐ[K] V) ≤ finrank V (V →ₗ[K] V)

Tactic:
(linearIndependent_toLinearMap K V V).fintype_card_le_finrank

Premises used: linearIndependent_toLinearMap, LinearIndependent.fintype_card_le_finrank
-- Module: Mathlib.FieldTheory.Fixed
Goal:
F : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : FiniteDimensional F K
⊢ Fintype.card.{u_3} (K →ₐ[F] K) ≤ finrank F K

Tactic:
Module.finrank_linearMap_self F K K ▸ finrank_algHom F K

Premises used: finrank_algHom, Eq.rec, Module.finrank_linearMap_self
-- Module: Mathlib.FieldTheory.Fixed
Goal:
F : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : FiniteDimensional F K
⊢ Fintype.card.{u_3} Gal(K/F) ≤ finrank F K

Tactic:
Fintype.ofEquiv_card (algEquivEquivAlgHom F K).toEquiv.symm ▸ AlgHom.card_le

Premises used: AlgEquiv.toAlgHom, AlgEquiv.ofBijective, Eq.rec, MulEquiv.toEquiv, Fintype.ofEquiv_card, algEquivEquivAlgHom, AlgHom.card_le, Equiv.symm, Eq.symm, EquivLike.toEquiv
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Fintype G
inst_4 : FaithfulSMul G F
⊢ finrank (↥(subfield G F)) F = Fintype.card G

Tactic:
le_antisymm (FixedPoints.finrank_le_card G F) <|
    calc
      Fintype.card G ≤ Fintype.card (F →ₐ[FixedPoints.subfield G F] F) :=
        Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)
      _ ≤ finrank F (F →ₗ[FixedPoints.subfield G F] F) := finrank_algHom (subfield G F) F
      _ = finrank (FixedPoints.subfield G F) F := finrank_linearMap_self _ _ _

Premises used: Fintype.card_le_of_injective, Trans.trans, finrank_algHom, FixedPoints.finrank_le_card, Membership.mem, Subtype, le_antisymm, FixedPoints.subfield, Module.finrank_linearMap_self, MulSemiringAction.toAlgHom_injective
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
intro :
  ∀ (val : Fintype G),
    Function.Bijective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
      (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
intro :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
      (MulSemiringAction.toAlgHom (↥(subfield G F)) F) ∧
    Fintype.card G = Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

Tactic:
rw [Fintype.bijective_iff_injective_and_card]

Premises used: Fintype.bijective_iff_injective_and_card
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
intro :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
intro₁ : Fintype.card G = Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
      (MulSemiringAction.toAlgHom (↥(subfield G F)) F) ∧
    Fintype.card G = Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

Tactic:
MulSemiringAction.toAlgHom_injective _ F

Premises used: MulSemiringAction.toAlgHom_injective
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

Tactic:
exact MulSemiringAction.toAlgHom_injective _ F

Premises used: MulSemiringAction.toAlgHom_injective
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
intro : Fintype.card G ≤ Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
intro₁ : Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card G
⊢ Fintype.card G = Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)

Tactic:
apply le_antisymm

Premises used: le_antisymm