-- Mathlib/FieldTheory/AbelRuffini.lean
theorem isSolvable (α : solvableByRad F E) : IsSolvable (minpoly F α).Gal

Proof state:
case mul
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α β : ↥(solvableByRad F E)),
    IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F β).Gal → IsSolvable (minpoly F (α * β)).Gal

Tactic:
exact fun α β => induction2 (mul_mem (subset_adjoin F _ (Set.mem_insert α _))
  (subset_adjoin F _ (Set.mem_insert_of_mem α (Set.mem_singleton β))))

Result:
no goals

Proof state:
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : F), IsSolvable (minpoly F ((algebraMap F ↥(solvableByRad F E)) α)).Gal

Tactic:
exact fun α => by rw [minpoly.eq_X_sub_C (solvableByRad F E)]; exact gal_X_sub_C_isSolvable α

Result:
no goals

Proof state:
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F α⁻¹).Gal

Tactic:
exact fun α => induction1 (inv_mem (mem_adjoin_simple_self F α))

Result:
no goals

Proof state:
case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → IsSolvable (minpoly F (α ^ n)).Gal → IsSolvable (minpoly F α).Gal

Tactic:
exact fun α n => induction3

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
⊢ IsSolvable (minpoly F α).Gal

Tactic:
revert α

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal

Proof state:
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F (-α)).Gal

Tactic:
exact fun α => induction1 (neg_mem (mem_adjoin_simple_self F α))

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : F
⊢ IsSolvable (X - C α).Gal

Tactic:
exact gal_X_sub_C_isSolvable α

Result:
no goals

Proof state:
case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α β : ↥(solvableByRad F E)),
    IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F β).Gal → IsSolvable (minpoly F (α + β)).Gal

Tactic:
exact fun α β => induction2 (add_mem (subset_adjoin F _ (Set.mem_insert α _))
  (subset_adjoin F _ (Set.mem_insert_of_mem α (Set.mem_singleton β))))

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : F
⊢ IsSolvable (minpoly F ((algebraMap F ↥(solvableByRad F E)) α)).Gal

Tactic:
rw [minpoly.eq_X_sub_C (solvableByRad F E)]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : F
⊢ IsSolvable (X - C α).Gal

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal

Tactic:
apply solvableByRad.induction

Result:
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : F), IsSolvable (minpoly F ((algebraMap F ↥(solvableByRad F E)) α)).Gal

case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α β : ↥(solvableByRad F E)),
    IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F β).Gal → IsSolvable (minpoly F (α + β)).Gal

case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F (-α)).Gal

case mul
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α β : ↥(solvableByRad F E)),
    IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F β).Gal → IsSolvable (minpoly F (α * β)).Gal

case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F α⁻¹).Gal

case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → IsSolvable (minpoly F (α ^ n)).Gal → IsSolvable (minpoly F α).Gal