-- Mathlib/FieldTheory/AbelRuffini.lean
theorem isSolvable' {α : E} {q : F[X]} (q_irred : Irreducible q) (q_aeval : aeval α q = 0)
    (hα : IsSolvableByRad F α) : IsSolvable q.Gal

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
this : IsSolvable (q * C q.leadingCoeff⁻¹).Gal
⊢ ¬q = 0 ∧ ¬q.leadingCoeff = 0

Tactic:
exact ⟨q_irred.ne_zero, leadingCoeff_ne_zero.mpr q_irred.ne_zero⟩

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
⊢ IsSolvable (minpoly F ⟨α, hα⟩).Gal

Tactic:
exact isSolvable ⟨α, hα⟩

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
⊢ IsSolvable (q * C q.leadingCoeff⁻¹).Gal

Tactic:
rw [minpoly.eq_of_irreducible q_irred q_aeval, ←
  show minpoly F (⟨α, hα⟩ : solvableByRad F E) = minpoly F α from
    (minpoly.algebraMap_eq (RingHom.injective _) _).symm]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
⊢ IsSolvable (minpoly F ⟨α, hα⟩).Gal

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
⊢ IsSolvable q.Gal

Tactic:
have : _root_.IsSolvable (q * C q.leadingCoeff⁻¹).Gal := by
  rw [minpoly.eq_of_irreducible q_irred q_aeval, ←
    show minpoly F (⟨α, hα⟩ : solvableByRad F E) = minpoly F α from
      (minpoly.algebraMap_eq (RingHom.injective _) _).symm]
  exact isSolvable ⟨α, hα⟩

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
this : IsSolvable (q * C q.leadingCoeff⁻¹).Gal
⊢ IsSolvable q.Gal

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
this : IsSolvable (q * C q.leadingCoeff⁻¹).Gal
⊢ IsSolvable q.Gal

Tactic:
refine solvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ ?_)

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
this : IsSolvable (q * C q.leadingCoeff⁻¹).Gal
⊢ q * C q.leadingCoeff⁻¹ ≠ 0

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
this : IsSolvable (q * C q.leadingCoeff⁻¹).Gal
⊢ q * C q.leadingCoeff⁻¹ ≠ 0

Tactic:
rw [mul_ne_zero_iff, Ne, Ne, C_eq_zero, inv_eq_zero]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval α) q = 0
hα : IsSolvableByRad F α
this : IsSolvable (q * C q.leadingCoeff⁻¹).Gal
⊢ ¬q = 0 ∧ ¬q.leadingCoeff = 0