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