-- Mathlib/FieldTheory/AbelRuffini.lean
theorem induction3 {α : solvableByRad F E} {n : ℕ} (hn : n ≠ 0) (hα : P (α ^ n)) : P α

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ (aeval α) (p.comp (X ^ n)) = 0

Tactic:
rw [aeval_comp, aeval_X_pow, minpoly.aeval]

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)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ P α

Tactic:
apply gal_isSolvable_of_splits

Result:
case x
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ Fact (Splits (algebraMap F (SplittingField ?q)) (minpoly F α))

case hq
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ IsSolvable (Gal ?q)

case q
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ F[X]

Proof state:
case hq.refine_2.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ IsSolvable ((Multiset.map (fun a => X - C a) s).prod.comp (X ^ n)).Gal

Tactic:
rw [multiset_prod_comp]

Result:
case hq.refine_2.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ IsSolvable (Multiset.map (fun p_1 => p_1.comp (X ^ n)) (Multiset.map (fun a => X - C a) s)).prod.Gal

Proof state:
case hq.refine_2.intro.hs.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
q : p.SplittingField[X]
hq : ∃ a ∈ s, X - C a = q
⊢ IsSolvable (q.comp (X ^ n)).Gal

Tactic:
obtain ⟨q, _, rfl⟩ := hq

Result:
case hq.refine_2.intro.hs.intro.intro.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
q : p.SplittingField
left✝ : q ∈ s
⊢ IsSolvable ((X - C q).comp (X ^ n)).Gal

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
⊢ P α

Tactic:
let p := minpoly F (α ^ n)

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
⊢ P α

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ (X ^ n).natDegree ≠ 0

Tactic:
rwa [natDegree_X_pow]

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)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
⊢ p.comp (X ^ n) ≠ 0

Tactic:
intro h

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
h : p.comp (X ^ n) = 0
⊢ False

Proof state:
case hq.refine_2.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ IsSolvable
    (C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod.comp (X ^ n)).Gal

Tactic:
apply gal_mul_isSolvable (gal_C_isSolvable _)

Result:
case hq.refine_2.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ IsSolvable ((Multiset.map (fun a => X - C a) s).prod.comp (X ^ n)).Gal

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
h : p.comp (X ^ n) = 0
h' : eval ((X ^ n).coeff 0) p = 0 ∧ X ^ n = C ((X ^ n).coeff 0)
⊢ n = 0

Tactic:
rw [← @natDegree_C F, ← h'.2, natDegree_X_pow]

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)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
h : p.comp (X ^ n) = 0
⊢ False

Tactic:
rcases comp_eq_zero_iff.mp h with h' | h'

Result:
case inl
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
h : p.comp (X ^ n) = 0
h' : p = 0
⊢ False

case inr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
h : p.comp (X ^ n) = 0
h' : eval ((X ^ n).coeff 0) p = 0 ∧ X ^ n = C ((X ^ n).coeff 0)
⊢ False

Proof state:
case hq.refine_2.intro.hs
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ ∀ p_1 ∈ Multiset.map (fun p_2 => p_2.comp (X ^ n)) (Multiset.map (fun a => X - C a) s), IsSolvable p_1.Gal

Tactic:
intro q hq

Result:
case hq.refine_2.intro.hs
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
q : p.SplittingField[X]
hq : q ∈ Multiset.map (fun p_1 => p_1.comp (X ^ n)) (Multiset.map (fun a => X - C a) s)
⊢ IsSolvable q.Gal