-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_isSolvable_tower (p q : F[X]) (hpq : p.Splits (algebraMap F q.SplittingField))
    (hp : IsSolvable p.Gal) (hq : IsSolvable (q.map (algebraMap F p.SplittingField)).Gal) :
    IsSolvable q.Gal

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
⊢ IsSolvable q.Gal

Tactic:
let K := p.SplittingField

Result:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
⊢ IsSolvable q.Gal

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
⊢ IsSolvable q.Gal

Tactic:
let L := q.SplittingField

Result:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
⊢ IsSolvable q.Gal

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this✝ : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal :=
  (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr
ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom
this : IsSolvable (K ≃ₐ[F] K)
⊢ IsSolvable q.Gal

Tactic:
haveI : IsSolvable (L ≃ₐ[K] L) := solvable_of_solvable_injective ϕ_inj

Result:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this✝¹ : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal :=
  (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr
ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom
this✝ : IsSolvable (K ≃ₐ[F] K)
this : IsSolvable (L ≃ₐ[K] L)
⊢ IsSolvable q.Gal

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal :=
  (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr
ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom
⊢ IsSolvable q.Gal

Tactic:
haveI : IsSolvable (K ≃ₐ[F] K) := hp

Result:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this✝ : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal :=
  (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr
ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom
this : IsSolvable (K ≃ₐ[F] K)
⊢ IsSolvable q.Gal

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this✝¹ : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal :=
  (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr
ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom
this✝ : IsSolvable (K ≃ₐ[F] K)
this : IsSolvable (L ≃ₐ[K] L)
⊢ IsSolvable q.Gal

Tactic:
exact isSolvable_of_isScalarTower F p.SplittingField q.SplittingField

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
⊢ IsSolvable q.Gal

Tactic:
haveI : Fact (p.Splits (algebraMap F L)) := ⟨hpq⟩

Result:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (Splits (algebraMap F L) p)
⊢ IsSolvable q.Gal

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal :=
  (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr
⊢ IsSolvable q.Gal

Tactic:
have ϕ_inj : Function.Injective ϕ.toMonoidHom := ϕ.injective

Result:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal :=
  (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr
ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom
⊢ IsSolvable q.Gal

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (Splits (algebraMap F L) p)
⊢ IsSolvable q.Gal

Tactic:
let ϕ : (L ≃ₐ[K] L) ≃* (q.map (algebraMap F K)).Gal :=
  (IsSplittingField.algEquiv L (q.map (algebraMap F K))).autCongr

Result:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : Splits (algebraMap F q.SplittingField) p
hp : IsSolvable p.Gal
hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal :=
  (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr
⊢ IsSolvable q.Gal