-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem restrict_smul [Fact (p.Splits (algebraMap F E))] (ϕ : E ≃ₐ[F] E) (x : rootSet p E) :
    ↑(restrict p E ϕ • x) = ϕ x

Proof state:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ↑(ψ
        (ψ.symm
          (↑((↑ϕ).restrictNormalAux p.SplittingField)
            (↑↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E))
              ↑((rootsEquivRoots p E).symm x))))) =
    ϕ ↑x

Tactic:
rw [AlgEquiv.apply_symm_apply ψ]

Result:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ↑(↑((↑ϕ).restrictNormalAux p.SplittingField)
        (↑↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)) ↑((rootsEquivRoots p E).symm x))) =
    ϕ ↑x

Proof state:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ϕ ↑((rootsEquivRoots p E) ((rootsEquivRoots p E).symm x)) = ϕ ↑x

Tactic:
rw [Equiv.apply_symm_apply (rootsEquivRoots p E)]

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ↑(↑((↑ϕ).restrictNormalAux p.SplittingField)
        (↑↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)) ↑((rootsEquivRoots p E).symm x))) =
    ϕ ↑x

Tactic:
change ϕ (rootsEquivRoots p E ((rootsEquivRoots p E).symm x)) = ϕ x

Result:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ϕ ↑((rootsEquivRoots p E) ((rootsEquivRoots p E).symm x)) = ϕ ↑x

Proof state:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ↑((restrict p E) ϕ • x) = ϕ ↑x

Tactic:
change ↑(ψ (ψ.symm _)) = ϕ x

Result:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ↑(ψ
        (ψ.symm
          (↑((↑ϕ).restrictNormalAux p.SplittingField)
            (↑↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E))
              ↑((rootsEquivRoots p E).symm x))))) =
    ϕ ↑x

Proof state:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(p.rootSet E)
⊢ ↑((restrict p E) ϕ • x) = ϕ ↑x

Tactic:
let ψ := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)

Result:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ↑((restrict p E) ϕ • x) = ϕ ↑x