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

Proof state:
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 (p.comp (X ^ n)).Gal

Tactic:
refine gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_

Result:
case hq.refine_1
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
⊢ Splits (algebraMap F (p.comp (X ^ n)).SplittingField) p

case hq.refine_2
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 (Polynomial.map (algebraMap F p.SplittingField) (p.comp (X ^ n))).Gal

Proof state:
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

Tactic:
exact minpoly.ne_zero (isIntegral (α ^ n)) h'

Result:
no goals

Proof state:
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 α))

Tactic:
exact ⟨splits_of_splits_of_dvd _ hp (SplittingField.splits (p.comp (X ^ n)))
  (minpoly.dvd F α (by rw [aeval_comp, aeval_X_pow, minpoly.aeval]))⟩

Result:
no goals

Proof state:
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

Tactic:
exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])

Result:
no goals

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
q : p.SplittingField[X]
hq : ∃ a ∈ Multiset.map (fun a => X - C a) s, a.comp (X ^ n) = q
⊢ IsSolvable q.Gal

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

Result:
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 : q ∈ Multiset.map (fun a => X - C a) s
⊢ IsSolvable (q.comp (X ^ n)).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 : q ∈ Multiset.map (fun a => X - C a) s
⊢ IsSolvable (q.comp (X ^ n)).Gal

Tactic:
rw [Multiset.mem_map] at hq

Result:
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

Proof state:
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

Tactic:
rw [sub_comp, X_comp, C_comp]

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 ^ n - C q).Gal

Proof state:
case hq.refine_2
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 (Polynomial.map (algebraMap F p.SplittingField) (p.comp (X ^ n))).Gal

Tactic:
obtain ⟨s, hs⟩ := (splits_iff_exists_multiset _).1 (SplittingField.splits p)

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 (Polynomial.map (algebraMap F p.SplittingField) (p.comp (X ^ n))).Gal

Proof state:
case hq.refine_1
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
⊢ Splits (algebraMap F (p.comp (X ^ n)).SplittingField) p

Tactic:
exact Gal.splits_in_splittingField_of_comp _ _ (by rwa [natDegree_X_pow])

Result:
no goals

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 (Polynomial.map (algebraMap F p.SplittingField) (p.comp (X ^ n))).Gal

Tactic:
rw [map_comp, Polynomial.map_pow, map_X, hs, mul_comp, C_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
    (C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod.comp (X ^ n)).Gal