awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : p.Gal
hϕ :
  Eq.{u_2 + 1} (α := Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (((galActionHom p E : MonoidHom.{u_1, u_2} p.Gal (Equiv.Perm (↑(p.rootSet E) : Type u_2))) :
          (a : p.Gal) → Equiv.Perm (↑(p.rootSet E) : Type u_2))
        ϕ :
      Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (1 : Equiv.Perm (↑(p.rootSet E) : Type u_2))
x : p.SplittingField
hx : Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x
key :
  Eq.{u_2 + 1} (α := (↑(p.rootSet E) : Type u_2))
    (((rootsEquivRoots p E :
            Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
          (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
        (HSMul.hSMul (β := (↑(p.rootSet p.SplittingField) : Type u_1)) ϕ
          (((Equiv.symm (rootsEquivRoots p E) :
                  Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
                (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
              (((rootsEquivRoots p E :
                    Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
                  (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
                (Subtype.mk (p := fun (x : p.SplittingField) ↦
                  Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx)) :
            (↑(p.rootSet p.SplittingField) : Type u_1))) :
      (↑(p.rootSet E) : Type u_2))
    (((rootsEquivRoots p E :
            Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
          (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
        (Subtype.mk (p := fun (x : p.SplittingField) ↦
          Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx) :
      (↑(p.rootSet E) : Type u_2))
⊢ Eq.{u_2 + 1} (α := (↑(p.rootSet E) : Type u_2))
    (((rootsEquivRoots p E :
            Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
          (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
        (ϕ •
          Subtype.mk (p := fun (x : p.SplittingField) ↦
            Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx) :
      (↑(p.rootSet E) : Type u_2))
    (((rootsEquivRoots p E :
            Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
          (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
        (Subtype.mk (p := fun (x : p.SplittingField) ↦
          Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx) :
      (↑(p.rootSet E) : Type u_2))

Tactic:
rw [Equiv.symm_apply_apply] at key

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : p.Gal
hϕ :
  Eq.{u_2 + 1} (α := Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (((galActionHom p E : MonoidHom.{u_1, u_2} p.Gal (Equiv.Perm (↑(p.rootSet E) : Type u_2))) :
          (a : p.Gal) → Equiv.Perm (↑(p.rootSet E) : Type u_2))
        ϕ :
      Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (1 : Equiv.Perm (↑(p.rootSet E) : Type u_2))
x : p.SplittingField
hx : Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x
key :
  Eq.{u_2 + 1} (α := (↑(p.rootSet E) : Type u_2))
    (((rootsEquivRoots p E :
            Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
          (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
        (ϕ •
          Subtype.mk (p := fun (x : p.SplittingField) ↦
            Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx) :
      (↑(p.rootSet E) : Type u_2))
    (((rootsEquivRoots p E :
            Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
          (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
        (Subtype.mk (p := fun (x : p.SplittingField) ↦
          Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx) :
      (↑(p.rootSet E) : Type u_2))
⊢ Eq (α := p.SplittingField) ((ϕ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
    ((1 : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)

Tactic:
Subtype.ext_iff.mp (Equiv.injective (rootsEquivRoots p E) key)

Premises used: Polynomial.Gal.rootsEquivRoots, Subtype.ext_iff, Iff.mp, Equiv.injective
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : p.Gal
hϕ :
  Eq.{u_2 + 1} (α := Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (((galActionHom p E : MonoidHom.{u_1, u_2} p.Gal (Equiv.Perm (↑(p.rootSet E) : Type u_2))) :
          (a : p.Gal) → Equiv.Perm (↑(p.rootSet E) : Type u_2))
        ϕ :
      Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (1 : Equiv.Perm (↑(p.rootSet E) : Type u_2))
x : p.SplittingField
hx : Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x
key :
  Eq.{u_2 + 1} (α := (↑(p.rootSet E) : Type u_2))
    (((rootsEquivRoots p E :
            Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
          (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
        (ϕ •
          Subtype.mk (p := fun (x : p.SplittingField) ↦
            Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx) :
      (↑(p.rootSet E) : Type u_2))
    (((rootsEquivRoots p E :
            Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
          (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
        (Subtype.mk (p := fun (x : p.SplittingField) ↦
          Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx) :
      (↑(p.rootSet E) : Type u_2))
⊢ Eq (α := p.SplittingField) ((ϕ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
    ((1 : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)

Tactic:
exact Subtype.ext_iff.mp (Equiv.injective (rootsEquivRoots p E) key)

Premises used: Polynomial.Gal.rootsEquivRoots, Subtype.ext_iff, Iff.mp, Equiv.injective
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
inst_1 : Decidable (q = 0)
hpq : p ∣ q
⊢ Eq.{u_1 + 1} (α := q.Gal →* p.Gal) (if hq : q = 0 then 1 else restrict p q.SplittingField)
    (if hq : q = 0 then 1 else restrict p q.SplittingField)

Tactic:
congr
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
⊢ Fact (Splits (R := q.SplittingField) (map (algebraMap F q.SplittingField) p))

Tactic:
haveI := Fact.mk <|
    (SplittingField.splits q).of_dvd (map_ne_zero hq) ((map_dvd_map' _).mpr hpq)
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
this : Fact (Splits (R := q.SplittingField) (map (algebraMap F q.SplittingField) p))
⊢ Function.Surjective (α := q.Gal) (β := p.Gal) (⇑(restrictDvd hpq) : (a : q.Gal) → p.Gal)

Tactic:
simpa only [restrictDvd_def, dif_neg hq] using restrict_surjective _ _

Premises used: Polynomial.Gal.restrictDvd_def, dif_neg, Polynomial.Gal.restrict_surjective
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
haveI haveI₁ haveI₂ :
  ∀ (this : Fact (Splits (R := q.SplittingField) (map (algebraMap F q.SplittingField) p))),
    Function.Surjective (α := q.Gal) (β := p.Gal) (⇑(restrictDvd hpq) : (a : q.Gal) → p.Gal)
⊢ Function.Surjective (α := q.Gal) (β := p.Gal) (⇑(restrictDvd hpq) : (a : q.Gal) → p.Gal)

Tactic:
classical
  haveI := Fact.mk <|
    (SplittingField.splits q).of_dvd (map_ne_zero hq) ((map_dvd_map' _).mpr hpq)
  simpa only [restrictDvd_def, dif_neg hq] using restrict_surjective _ _

Premises used: Polynomial.Gal.restrictDvd_def, dif_neg
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
pos :
  ∀ (hpq : p * q = 0),
    Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)
neg :
  ∀ (hpq : ¬p * q = 0),
    Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)
⊢ Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)

Tactic:
by_cases hpq : p * q = 0
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p * q = 0
rw : Unique (Gal (F := F) 0)
⊢ Unique (p * q).Gal

Tactic:
rw [hpq]
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p * q = 0
⊢ Unique (Gal (F := F) 0)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p * q = 0
pos :
  ∀ (this : Unique (p * q).Gal),
    Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)
⊢ Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)

Tactic:
have : Unique (p * q).Gal := by rw [hpq]; infer_instance
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p * q = 0
this : Unique (p * q).Gal
⊢ Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)

Tactic:
fun f g _ => Eq.trans (Unique.eq_default f) (Unique.eq_default g).symm

Premises used: Unique.eq_default, Function.Injective, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p * q = 0
this : Unique (p * q).Gal
⊢ Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)

Tactic:
exact fun f g _ => Eq.trans (Unique.eq_default f) (Unique.eq_default g).symm

Premises used: Unique.eq_default, Eq.symm, Eq.trans
-- 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 × q.Gal) ((restrictProd p q : (a : (p * q).Gal) → p.Gal × q.Gal) f : p.Gal × q.Gal)
    ((restrictProd p q : (a : (p * q).Gal) → p.Gal × q.Gal) g : p.Gal × q.Gal)
⊢ Eq (α := p.Gal × q.Gal)
    ((MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField)
            (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField) :
          (a : (p * q).Gal) → p.Gal × q.Gal)
        f :
      p.Gal × q.Gal)
    ((MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField)
            (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField) :
          (a : (p * q).Gal) → p.Gal × q.Gal)
        g :
      p.Gal × q.Gal)

Tactic:
simp only [restrictProd, restrictDvd_def] at hfg

Premises used: Polynomial.Gal.restrictDvd_def, Polynomial.Gal.restrictProd
-- 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 × q.Gal)
    ((MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField)
            (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField) :
          (a : (p * q).Gal) → p.Gal × q.Gal)
        f :
      p.Gal × q.Gal)
    ((MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField)
            (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField) :
          (a : (p * q).Gal) → p.Gal × q.Gal)
        g :
      p.Gal × q.Gal)
⊢ 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)

Tactic:
simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk_inj] at hfg

Premises used: Prod.mk_inj, dif_neg, MonoidHom.prod_apply
-- 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)
neg :
  ∀ (x : (p * q).SplittingField)
    (hx : Membership.mem (γ := Set (p * q).SplittingField) ((p * q).rootSet (p * q).SplittingField) x),
    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)
⊢ f = g

Tactic:
ext (x hx)
-- 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 : Membership.mem (γ := Set (p * q).SplittingField) ((p * q).rootSet (p * q).SplittingField) x
⊢ x ∈
    (↑(HAdd.hAdd (α := Multiset (p * q).SplittingField) (p.aroots (p * q).SplittingField)
            (q.aroots (p * q).SplittingField)).toFinset :
      Set (p * q).SplittingField)

Tactic:
rw [rootSet_def, aroots_mul hpq] at hx

Premises used: Polynomial.rootSet_def, Polynomial.aroots_mul
-- 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)
neg :
  ∀ (h : Membership.mem (γ := Multiset (p * q).SplittingField) (p.aroots (p * q).SplittingField) x),
    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)
neg₁ :
  ∀ (h : Membership.mem (γ := Multiset (p * q).SplittingField) (q.aroots (p * q).SplittingField) x),
    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)
⊢ 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:
rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h

Premises used: Multiset.mem_add, Iff.mp, Multiset.mem_toFinset
-- 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
⊢ Fact (Splits (R := (p * q).SplittingField) (map (algebraMap F (p * q).SplittingField) p))

Tactic:
haveI : Fact ((p.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_right p q))⟩
-- 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))
⊢ 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)

Tactic:
have key :
      x =
        algebraMap p.SplittingField (p * q).SplittingField
          ((rootsEquivRoots p _).invFun
            ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
      Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots p _) ⟨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) (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)
neg :
  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)
⊢ 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) (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:
congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)

Premises used: AlgEquiv.ext_iff, congr_arg, And.left, Iff.mp