awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  Eq (α := p.Gal) ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) f : p.Gal)
      ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) g : p.Gal) ∧
    Eq (α := q.Gal) ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) f : q.Gal)
      ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) g : q.Gal)
x : (p * q).SplittingField
hx :
  x ∈
    (↑(HAdd.hAdd (α := Multiset (p * q).SplittingField) (p.aroots (p * q).SplittingField)
            (q.aroots (p * q).SplittingField)).toFinset :
      Set (p * q).SplittingField)
h : Membership.mem (γ := Multiset (p * q).SplittingField) (p.aroots (p * q).SplittingField) x
this : Fact (Splits (R := (p * q).SplittingField) (map (algebraMap F (p * q).SplittingField) p))
key :
  x =
    (algebraMap p.SplittingField (p * q).SplittingField : (a : p.SplittingField) → (p * q).SplittingField)
      (↑(Equiv.invFun (rootsEquivRoots p (p * q).SplittingField)
            (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
              Membership.mem (γ := Set (p * q).SplittingField) (p.rootSet (p * q).SplittingField) x) x ⋯)) :
        p.SplittingField)
⊢ Eq (α := (p * q).SplittingField)
    ((algebraMap p.SplittingField (p * q).SplittingField : (a : p.SplittingField) → (p * q).SplittingField)
        ((AlgEquiv.restrictNormal f p.SplittingField : (a : p.SplittingField) → p.SplittingField)
          (↑(Equiv.invFun (rootsEquivRoots p (p * q).SplittingField)
                (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
                  Membership.mem (γ := Set (p * q).SplittingField) (p.rootSet (p * q).SplittingField) x) x ⋯)) :
            p.SplittingField)) :
      (p * q).SplittingField)
    ((algebraMap p.SplittingField (p * q).SplittingField : (a : p.SplittingField) → (p * q).SplittingField)
        ((AlgEquiv.restrictNormal g p.SplittingField : (a : p.SplittingField) → p.SplittingField)
          (↑(Equiv.invFun (rootsEquivRoots p (p * q).SplittingField)
                (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
                  Membership.mem (γ := Set (p * q).SplittingField) (p.rootSet (p * q).SplittingField) x) x ⋯)) :
            p.SplittingField)) :
      (p * q).SplittingField)

Tactic:
exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)

Premises used: AlgEquiv.ext_iff, congr_arg, And.left, Iff.mp
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  Eq (α := p.Gal) ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) f : p.Gal)
      ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) g : p.Gal) ∧
    Eq (α := q.Gal) ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) f : q.Gal)
      ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) g : q.Gal)
x : (p * q).SplittingField
hx :
  x ∈
    (↑(HAdd.hAdd (α := Multiset (p * q).SplittingField) (p.aroots (p * q).SplittingField)
            (q.aroots (p * q).SplittingField)).toFinset :
      Set (p * q).SplittingField)
h : Membership.mem (γ := Multiset (p * q).SplittingField) (q.aroots (p * q).SplittingField) x
⊢ Fact (Splits (R := (p * q).SplittingField) (map (algebraMap F (p * q).SplittingField) q))

Tactic:
haveI : Fact ((q.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_left q p))⟩
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  Eq (α := p.Gal) ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) f : p.Gal)
      ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) g : p.Gal) ∧
    Eq (α := q.Gal) ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) f : q.Gal)
      ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) g : q.Gal)
x : (p * q).SplittingField
hx :
  x ∈
    (↑(HAdd.hAdd (α := Multiset (p * q).SplittingField) (p.aroots (p * q).SplittingField)
            (q.aroots (p * q).SplittingField)).toFinset :
      Set (p * q).SplittingField)
h : Membership.mem (γ := Multiset (p * q).SplittingField) (q.aroots (p * q).SplittingField) x
this : Fact (Splits (R := (p * q).SplittingField) (map (algebraMap F (p * q).SplittingField) q))
⊢ x =
    (algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
      (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
            (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
              Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
        q.SplittingField)

Tactic:
have key :
      x =
        algebraMap q.SplittingField (p * q).SplittingField
          ((rootsEquivRoots q _).invFun
            ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
      Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots q _) ⟨x, _⟩).symm
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  Eq (α := p.Gal) ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) f : p.Gal)
      ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) g : p.Gal) ∧
    Eq (α := q.Gal) ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) f : q.Gal)
      ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) g : q.Gal)
x : (p * q).SplittingField
hx :
  x ∈
    (↑(HAdd.hAdd (α := Multiset (p * q).SplittingField) (p.aroots (p * q).SplittingField)
            (q.aroots (p * q).SplittingField)).toFinset :
      Set (p * q).SplittingField)
h : Membership.mem (γ := Multiset (p * q).SplittingField) (q.aroots (p * q).SplittingField) x
this : Fact (Splits (R := (p * q).SplittingField) (map (algebraMap F (p * q).SplittingField) q))
key :
  x =
    (algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
      (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
            (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
              Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
        q.SplittingField)
neg :
  Eq (α := (p * q).SplittingField)
    ((algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
        ((AlgEquiv.restrictNormal f q.SplittingField : (a : q.SplittingField) → q.SplittingField)
          (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
                (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
                  Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
            q.SplittingField)) :
      (p * q).SplittingField)
    ((algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
        ((AlgEquiv.restrictNormal g q.SplittingField : (a : q.SplittingField) → q.SplittingField)
          (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
                (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
                  Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
            q.SplittingField)) :
      (p * q).SplittingField)
⊢ Eq (α := (p * q).SplittingField)
    ((f : (a : (p * q).SplittingField) → (p * q).SplittingField) x : (p * q).SplittingField)
    ((g : (a : (p * q).SplittingField) → (p * q).SplittingField) x : (p * q).SplittingField)

Tactic:
rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]

Premises used: AlgEquiv.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  Eq (α := p.Gal) ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) f : p.Gal)
      ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) g : p.Gal) ∧
    Eq (α := q.Gal) ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) f : q.Gal)
      ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) g : q.Gal)
x : (p * q).SplittingField
hx :
  x ∈
    (↑(HAdd.hAdd (α := Multiset (p * q).SplittingField) (p.aroots (p * q).SplittingField)
            (q.aroots (p * q).SplittingField)).toFinset :
      Set (p * q).SplittingField)
h : Membership.mem (γ := Multiset (p * q).SplittingField) (q.aroots (p * q).SplittingField) x
this : Fact (Splits (R := (p * q).SplittingField) (map (algebraMap F (p * q).SplittingField) q))
key :
  x =
    (algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
      (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
            (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
              Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
        q.SplittingField)
⊢ Eq (α := (p * q).SplittingField)
    ((algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
        ((AlgEquiv.restrictNormal f q.SplittingField : (a : q.SplittingField) → q.SplittingField)
          (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
                (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
                  Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
            q.SplittingField)) :
      (p * q).SplittingField)
    ((algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
        ((AlgEquiv.restrictNormal g q.SplittingField : (a : q.SplittingField) → q.SplittingField)
          (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
                (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
                  Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
            q.SplittingField)) :
      (p * q).SplittingField)

Tactic:
congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)

Premises used: AlgEquiv.ext_iff, congr_arg, And.right, Iff.mp
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  Eq (α := p.Gal) ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) f : p.Gal)
      ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) g : p.Gal) ∧
    Eq (α := q.Gal) ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) f : q.Gal)
      ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) g : q.Gal)
x : (p * q).SplittingField
hx :
  x ∈
    (↑(HAdd.hAdd (α := Multiset (p * q).SplittingField) (p.aroots (p * q).SplittingField)
            (q.aroots (p * q).SplittingField)).toFinset :
      Set (p * q).SplittingField)
h : Membership.mem (γ := Multiset (p * q).SplittingField) (q.aroots (p * q).SplittingField) x
this : Fact (Splits (R := (p * q).SplittingField) (map (algebraMap F (p * q).SplittingField) q))
key :
  x =
    (algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
      (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
            (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
              Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
        q.SplittingField)
⊢ Eq (α := (p * q).SplittingField)
    ((algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
        ((AlgEquiv.restrictNormal f q.SplittingField : (a : q.SplittingField) → q.SplittingField)
          (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
                (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
                  Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
            q.SplittingField)) :
      (p * q).SplittingField)
    ((algebraMap q.SplittingField (p * q).SplittingField : (a : q.SplittingField) → (p * q).SplittingField)
        ((AlgEquiv.restrictNormal g q.SplittingField : (a : q.SplittingField) → q.SplittingField)
          (↑(Equiv.invFun (rootsEquivRoots q (p * q).SplittingField)
                (Subtype.mk (p := fun (x : (p * q).SplittingField) ↦
                  Membership.mem (γ := Set (p * q).SplittingField) (q.rootSet (p * q).SplittingField) x) x ⋯)) :
            q.SplittingField)) :
      (p * q).SplittingField)

Tactic:
exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)

Premises used: AlgEquiv.ext_iff, congr_arg, And.right, Iff.mp
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
rw :
  (HMul.hMul (α := (q₁ * q₂).SplittingField[X]) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)
      (map (algebraMap F (q₁ * q₂).SplittingField) p₂)).Splits
⊢ Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) (p₁ * p₂))

Tactic:
rw [Polynomial.map_mul]

Premises used: Polynomial.map_mul
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
hf : Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)
hg : Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) p₂)
⊢ (HMul.hMul (α := (q₁ * q₂).SplittingField[X]) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)
      (map (algebraMap F (q₁ * q₂).SplittingField) p₂)).Splits

Tactic:
apply Splits.mul

Premises used: Polynomial.Splits.mul
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
hf :
  Splits
    (map (↑(SplittingField.lift q₁ ⋯) : q₁.SplittingField →+* (q₁ * q₂).SplittingField)
      (map (algebraMap F q₁.SplittingField) p₁))
⊢ Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)

Tactic:
rw [←
      (SplittingField.lift q₁
          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
             ((map_dvd_map' _).mpr (dvd_mul_right q₁ q₂)))).comp_algebraMap, ← map_map]

Premises used: Iff.mpr, AlgHom.comp_algebraMap, Polynomial.SplittingField.lift, Polynomial.SplittingField.splits, Polynomial.Splits.of_dvd, dvd_mul_right, Polynomial.map_ne_zero, mul_ne_zero, Polynomial.map_map, Polynomial.map_dvd_map'
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
⊢ Splits
    (map (↑(SplittingField.lift q₁ ⋯) : q₁.SplittingField →+* (q₁ * q₂).SplittingField)
      (map (algebraMap F q₁.SplittingField) p₁))

Tactic:
h₁.map _

Premises used: Polynomial.Splits.map
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
⊢ Splits
    (map (↑(SplittingField.lift q₁ ⋯) : q₁.SplittingField →+* (q₁ * q₂).SplittingField)
      (map (algebraMap F q₁.SplittingField) p₁))

Tactic:
exact h₁.map _

Premises used: Polynomial.Splits.map
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
hg :
  Splits
    (map (↑(SplittingField.lift q₂ ⋯) : q₂.SplittingField →+* (q₁ * q₂).SplittingField)
      (map (algebraMap F q₂.SplittingField) p₂))
⊢ Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) p₂)

Tactic:
rw [←
      (SplittingField.lift q₂
          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
             ((map_dvd_map' _).mpr (dvd_mul_left q₂ q₁)))).comp_algebraMap, ← map_map]

Premises used: Iff.mpr, AlgHom.comp_algebraMap, Polynomial.SplittingField.lift, Polynomial.SplittingField.splits, dvd_mul_left, Polynomial.Splits.of_dvd, Polynomial.map_ne_zero, mul_ne_zero, Polynomial.map_map, Polynomial.map_dvd_map'
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
⊢ Splits
    (map (↑(SplittingField.lift q₂ ⋯) : q₂.SplittingField →+* (q₁ * q₂).SplittingField)
      (map (algebraMap F q₂.SplittingField) p₂))

Tactic:
h₂.map _

Premises used: Polynomial.Splits.map
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
⊢ Splits
    (map (↑(SplittingField.lift q₂ ⋯) : q₂.SplittingField →+* (q₁ * q₂).SplittingField)
      (map (algebraMap F q₂.SplittingField) p₂))

Tactic:
exact h₂.map _

Premises used: Polynomial.Splits.map
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hq : q.natDegree ≠ 0
⊢ Fact (Splits (R := (p.comp q).SplittingField) (map (algebraMap F (p.comp q).SplittingField) p))

Tactic:
haveI : Fact (Splits (p.map (algebraMap F (SplittingField (comp p q))))) :=
    ⟨splits_in_splittingField_of_comp p q hq⟩
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hq : q.natDegree ≠ 0
this : Fact (Splits (R := (p.comp q).SplittingField) (map (algebraMap F (p.comp q).SplittingField) p))
⊢ Function.Surjective (α := (p.comp q).Gal) (β := p.Gal) (⇑(restrictComp p q hq) : (a : (p.comp q).Gal) → p.Gal)

Tactic:
simpa only [restrictComp] using restrict_surjective _ _

Premises used: Polynomial.Gal.restrictComp, Polynomial.Gal.restrict_surjective
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
hp : p.Separable
⊢ Nat.card.{u_1} p.Gal = finrank F p.SplittingField

Tactic:
haveI : IsGalois F p.SplittingField := IsGalois.of_separable_splitting_field hp
  IsGalois.card_aut_eq_finrank F p.SplittingField

Premises used: IsGalois.card_aut_eq_finrank, Polynomial.Gal, Polynomial.SplittingField
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
rw : p.natDegree ∣ finrank F p.SplittingField
⊢ p.natDegree ∣ Nat.card.{u_1} p.Gal

Tactic:
rw [Gal.card_of_separable p_irr.separable]

Premises used: Irreducible.separable, Polynomial.Gal.card_of_separable
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.degree ≠ 0

Tactic:
have hp : p.degree ≠ 0 := fun h =>
    Nat.Prime.ne_zero p_deg (natDegree_eq_zero_iff_degree_le_zero.mpr (le_of_eq h))
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
rwa rwa₁ rwa₂ rwa₃ : p.degree ≠ 0
⊢ degree (R := p.SplittingField) (map (algebraMap F p.SplittingField) p) ≠ 0

Tactic:
rwa [degree_map]

Premises used: Polynomial.degree_map
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
⊢ IsIntegral F α

Tactic:
have hα : IsIntegral F α := .of_finite F α
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
h : finrank F p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
⊢ p.natDegree ∣ finrank F p.SplittingField

Tactic:
use Module.finrank F⟮α⟯ p.SplittingField

Premises used: Polynomial.SplittingField, Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton, Module.finrank
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : natDegree (minpoly F α) = p.natDegree
x : AddCommGroup ↥F⟮α⟯ := Ring.toAddCommGroup
rw :
  finrank F ↥F⟮α⟯ * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField =
    p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
rw₁ :
  natDegree (minpoly F α) * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField =
    p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
rw₂ rw₃ :
  p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
⊢ finrank F p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField

Tactic:
rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
      IntermediateField.adjoin.finrank hα, this]

Premises used: IntermediateField.adjoin.finrank, Polynomial.SplittingField, Membership.mem, Subtype, Module.finrank_mul_finrank, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
h : natDegree (minpoly F α) = p.natDegree
⊢ finrank F p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField

Tactic:
suffices (minpoly F α).natDegree = p.natDegree by
    letI _ : AddCommGroup F⟮α⟯ := Ring.toAddCommGroup
    rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
      IntermediateField.adjoin.finrank hα, this]
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
a : natDegree (minpoly F α) ≤ p.natDegree
a₁ : p.natDegree ≤ natDegree (minpoly F α)
⊢ natDegree (minpoly F α) = p.natDegree

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ natDegree (minpoly F α) ≤ p.natDegree

Tactic:
natDegree_le_of_dvd this p_irr.ne_zero

Premises used: Polynomial.natDegree_le_of_dvd, Irreducible.ne_zero
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ natDegree (minpoly F α) ≤ p.natDegree

Tactic:
exact natDegree_le_of_dvd this p_irr.ne_zero

Premises used: Polynomial.natDegree_le_of_dvd, Irreducible.ne_zero