awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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
⊢ Eq (α := p.SplittingField) ((ϕ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
    ((1 : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
have key : Eq.{u_2 + 1} (α := (↑(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)) :
        (a : (↑(p.rootSet E) : Type u_2)) → (↑(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))
  ((1 : (a : (↑(p.rootSet E) : Type u_2)) → (↑(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: have key := Equiv.Perm.ext_iff.mp hϕ (rootsEquivRoots p E ⟨x, hx⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
⊢ Function.Surjective (α := q.Gal) (β := p.Gal) (⇑(restrictDvd hpq) : (a : q.Gal) → p.Gal)
have this : 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)
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
⊢ Function.Surjective (α := q.Gal) (β := p.Gal) (⇑(restrictDvd hpq) : (a : q.Gal) → p.Gal)
have 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)
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 _ _
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
⊢ Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)
have 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)
Tactic: by_cases hpq : p * q = 0
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
⊢ Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)
have 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)
Tactic: by_cases hpq : p * q = 0
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p * q = 0
⊢ Unique (p * q).Gal
have rw : Unique (Gal (F := F) 0)
Tactic: rw [hpq]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : p * q = 0
⊢ Function.Injective (α := (p * q).Gal) (β := p.Gal × q.Gal) (⇑(restrictProd p q) : (a : (p * q).Gal) → p.Gal × q.Gal)
have 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)
Tactic: have : Unique (p * q).Gal := by rw [hpq]; infer_instance
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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)
⊢ f = g
have 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)
Tactic: simp only [restrictProd, restrictDvd_def] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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)
⊢ f = g
have 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)
Tactic: simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk_inj] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
⊢ f = g
have 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)
Tactic: ext (x hx)
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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
⊢ 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)
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
⊢ 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)
have 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)
Tactic: rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
⊢ 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)
have 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)
Tactic: rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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
⊢ 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)
have this : 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))⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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))
⊢ 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)
have 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 sorry)) :
      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
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
    ((f : (a : (p * q).SplittingField) → (p * q).SplittingField) x : (p * q).SplittingField)
    ((g : (a : (p * q).SplittingField) → (p * q).SplittingField) x : (p * q).SplittingField)
have 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 sorry)) :
          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 sorry)) :
          p.SplittingField)) :
    (p * q).SplittingField)
Tactic: rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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
⊢ 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)
have this : 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))⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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))
⊢ 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)
have 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 sorry)) :
      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
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
    ((f : (a : (p * q).SplittingField) → (p * q).SplittingField) x : (p * q).SplittingField)
    ((g : (a : (p * q).SplittingField) → (p * q).SplittingField) x : (p * q).SplittingField)
have 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 sorry)) :
          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 sorry)) :
          q.SplittingField)) :
    (p * q).SplittingField)
Tactic: rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]