-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
⊢ 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)
have 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)
Tactic: rw [AlgEquiv.apply_symm_apply ψ]