-- 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
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 (α := 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))
  (((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
Cleared hypotheses: key