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

Tactic:
change
    rootsEquivRoots p E (ϕ • (rootsEquivRoots p E).symm (rootsEquivRoots p E ⟨x, hx⟩)) =
      rootsEquivRoots p E ⟨x, hx⟩
    at key

Premises used: Polynomial.Gal.rootsEquivRoots, Subtype.mk, HSMul.hSMul, Equiv.symm, DFunLike.coe