-- 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 × 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)
neg :
  ∀
    (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
neg₁ :
  ∀
    (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
neg₂ :
  ∀
    (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)
⊢ f = g
have neg₃ : ∀
  (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)
Tactic: classical
  simp only [restrictProd, restrictDvd_def] at hfg
  simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk_inj] at hfg
  ext (x hx)
  rw [rootSet_def, aroots_mul hpq] at hx
  rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h
  · 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))⟩
    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
    rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
    exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)
  · 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))⟩
    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
    rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
    exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)
Cleared hypotheses: hfg