-- Mathlib/FieldTheory/Normal/Basic.lean
theorem isSolvable_of_isScalarTower [Normal F K₁] [h1 : IsSolvable (K₁ ≃ₐ[F] K₁)]
    [h2 : IsSolvable (E ≃ₐ[K₁] E)] : IsSolvable (E ≃ₐ[F] E)

Proof state:
F : Type u_1
inst✝⁷ : Field F
K₁ : Type u_3
inst✝⁶ : Field K₁
inst✝⁵ : Algebra F K₁
E : Type u_6
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : Algebra K₁ E
inst✝¹ : IsScalarTower F K₁ E
inst✝ : Normal F K₁
h1 : IsSolvable (K₁ ≃ₐ[F] K₁)
h2 : IsSolvable (E ≃ₐ[K₁] E)
⊢ IsSolvable (E ≃ₐ[F] E)

Tactic:
let f : (E ≃ₐ[K₁] E) →* E ≃ₐ[F] E :=
  { toFun := fun ϕ =>
      AlgEquiv.ofAlgHom (ϕ.toAlgHom.restrictScalars F) (ϕ.symm.toAlgHom.restrictScalars F)
        (AlgHom.ext fun x => ϕ.apply_symm_apply x) (AlgHom.ext fun x => ϕ.symm_apply_apply x)
    map_one' := AlgEquiv.ext fun _ => rfl
    map_mul' := fun _ _ => AlgEquiv.ext fun _ => rfl }

Result:
F : Type u_1
inst✝⁷ : Field F
K₁ : Type u_3
inst✝⁶ : Field K₁
inst✝⁵ : Algebra F K₁
E : Type u_6
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : Algebra K₁ E
inst✝¹ : IsScalarTower F K₁ E
inst✝ : Normal F K₁
h1 : IsSolvable (K₁ ≃ₐ[F] K₁)
h2 : IsSolvable (E ≃ₐ[K₁] E)
f : (E ≃ₐ[K₁] E) →* E ≃ₐ[F] E :=
  { toFun := fun ϕ => AlgEquiv.ofAlgHom (AlgHom.restrictScalars F ↑ϕ) (AlgHom.restrictScalars F ↑ϕ.symm) ⋯ ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
⊢ IsSolvable (E ≃ₐ[F] E)

Proof state:
F : Type u_1
inst✝⁷ : Field F
K₁ : Type u_3
inst✝⁶ : Field K₁
inst✝⁵ : Algebra F K₁
E : Type u_6
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : Algebra K₁ E
inst✝¹ : IsScalarTower F K₁ E
inst✝ : Normal F K₁
h1 : IsSolvable (K₁ ≃ₐ[F] K₁)
h2 : IsSolvable (E ≃ₐ[K₁] E)
f : (E ≃ₐ[K₁] E) →* E ≃ₐ[F] E :=
  { toFun := fun ϕ => AlgEquiv.ofAlgHom (AlgHom.restrictScalars F ↑ϕ) (AlgHom.restrictScalars F ↑ϕ.symm) ⋯ ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
⊢ IsSolvable (E ≃ₐ[F] E)

Tactic:
refine
  solvable_of_ker_le_range f (AlgEquiv.restrictNormalHom K₁) fun ϕ hϕ =>
    ⟨{ ϕ with commutes' := fun x => ?_ }, AlgEquiv.ext fun _ => rfl⟩

Result:
F : Type u_1
inst✝⁷ : Field F
K₁ : Type u_3
inst✝⁶ : Field K₁
inst✝⁵ : Algebra F K₁
E : Type u_6
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : Algebra K₁ E
inst✝¹ : IsScalarTower F K₁ E
inst✝ : Normal F K₁
h1 : IsSolvable (K₁ ≃ₐ[F] K₁)
h2 : IsSolvable (E ≃ₐ[K₁] E)
f : (E ≃ₐ[K₁] E) →* E ≃ₐ[F] E :=
  { toFun := fun ϕ => AlgEquiv.ofAlgHom (AlgHom.restrictScalars F ↑ϕ) (AlgHom.restrictScalars F ↑ϕ.symm) ⋯ ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
ϕ : E ≃ₐ[F] E
hϕ : ϕ ∈ (AlgEquiv.restrictNormalHom K₁).ker
x : K₁
⊢ ϕ.toFun ((algebraMap K₁ E) x) = (algebraMap K₁ E) x

Proof state:
F : Type u_1
inst✝⁷ : Field F
K₁ : Type u_3
inst✝⁶ : Field K₁
inst✝⁵ : Algebra F K₁
E : Type u_6
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : Algebra K₁ E
inst✝¹ : IsScalarTower F K₁ E
inst✝ : Normal F K₁
h1 : IsSolvable (K₁ ≃ₐ[F] K₁)
h2 : IsSolvable (E ≃ₐ[K₁] E)
f : (E ≃ₐ[K₁] E) →* E ≃ₐ[F] E :=
  { toFun := fun ϕ => AlgEquiv.ofAlgHom (AlgHom.restrictScalars F ↑ϕ) (AlgHom.restrictScalars F ↑ϕ.symm) ⋯ ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
ϕ : E ≃ₐ[F] E
hϕ : ϕ ∈ (AlgEquiv.restrictNormalHom K₁).ker
x : K₁
⊢ ϕ.toFun ((algebraMap K₁ E) x) = (algebraMap K₁ E) x

Tactic:
exact Eq.trans (ϕ.restrictNormal_commutes K₁ x).symm (congr_arg _ (AlgEquiv.ext_iff.mp hϕ x))

Result:
no goals