-- 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))
ϕ : Gal(E/F)
x : (↑(p.rootSet E) : Type u_2)
ψ : AlgEquiv.{u_1, u_1, u_2} F p.SplittingField
  ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E)) :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
rw :
  Eq (α := E)
    ((↑(((↑((↑ϕ : E →ₐ[F] E).restrictNormalAux p.SplittingField) :
                ↥(IsScalarTower.toAlgHom F p.SplittingField E).range →+*
                  ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) :
              (a : ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) →
                ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
            ((((↑(↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)) :
                        p.SplittingField →ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) :
                    RingHom.{u_1, u_2} p.SplittingField
                      ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E))) :
                  RingHom.{u_1, u_2} p.SplittingField
                    ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E))) :
                (a : p.SplittingField) → ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
              (↑(((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))
                    x) :
                p.SplittingField))) :
        E) :
      E)
    ((ϕ : (a : E) → E) (↑x : E) : E)
⊢ Eq (α := E)
    ((↑((ψ : (a : p.SplittingField) → ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
            ((ψ.symm : (a : ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) → p.SplittingField)
              (((↑((↑ϕ : E →ₐ[F] E).restrictNormalAux p.SplittingField) :
                    ↥(IsScalarTower.toAlgHom F p.SplittingField E).range →+*
                      ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) :
                  (a : ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) →
                    ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
                ((((↑(↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)) :
                            p.SplittingField →ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) :
                        RingHom.{u_1, u_2} p.SplittingField
                          ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E))) :
                      RingHom.{u_1, u_2} p.SplittingField
                        ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E))) :
                    (a : p.SplittingField) → ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
                  (↑(((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))
                        x) :
                    p.SplittingField))))) :
        E) :
      E)
    ((ϕ : (a : E) → E) (↑x : E) : E)

Tactic:
rw [AlgEquiv.apply_symm_apply ψ]

Premises used: AlgEquiv.apply_symm_apply