[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsSolvable (Gal 0)
[PROOFSTEP]
infer_instance
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsSolvable (Gal 1)
[PROOFSTEP]
infer_instance
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : F
⊢ IsSolvable (Gal (↑C x))
[PROOFSTEP]
infer_instance
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsSolvable (Gal X)
[PROOFSTEP]
infer_instance
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : F
⊢ IsSolvable (Gal (X - ↑C x))
[PROOFSTEP]
infer_instance
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
⊢ IsSolvable (Gal (X ^ n))
[PROOFSTEP]
infer_instance
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Multiset F[X]
hs : ∀ (p : F[X]), p ∈ s → IsSolvable (Gal p)
⊢ IsSolvable (Gal (Multiset.prod s))
[PROOFSTEP]
apply Multiset.induction_on' s
[GOAL]
case h₁
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Multiset F[X]
hs : ∀ (p : F[X]), p ∈ s → IsSolvable (Gal p)
⊢ IsSolvable (Gal (Multiset.prod 0))
[PROOFSTEP]
exact gal_one_isSolvable
[GOAL]
case h₂
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Multiset F[X]
hs : ∀ (p : F[X]), p ∈ s → IsSolvable (Gal p)
⊢ ∀ {a : F[X]} {s_1 : Multiset F[X]},
    a ∈ s → s_1 ⊆ s → IsSolvable (Gal (Multiset.prod s_1)) → IsSolvable (Gal (Multiset.prod (insert a s_1)))
[PROOFSTEP]
intro p t hps _ ht
[GOAL]
case h₂
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Multiset F[X]
hs : ∀ (p : F[X]), p ∈ s → IsSolvable (Gal p)
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
ht : IsSolvable (Gal (Multiset.prod t))
⊢ IsSolvable (Gal (Multiset.prod (insert p t)))
[PROOFSTEP]
rw [Multiset.insert_eq_cons, Multiset.prod_cons]
[GOAL]
case h₂
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Multiset F[X]
hs : ∀ (p : F[X]), p ∈ s → IsSolvable (Gal p)
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
ht : IsSolvable (Gal (Multiset.prod t))
⊢ IsSolvable (Gal (p * Multiset.prod t))
[PROOFSTEP]
exact gal_mul_isSolvable (hs p hps) ht
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p q : F[X]
hpq : Splits (algebraMap F (SplittingField q)) p
hp : IsSolvable (Gal p)
hq : IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) q))
⊢ IsSolvable (Gal q)
[PROOFSTEP]
let K := p.SplittingField
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p q : F[X]
hpq : Splits (algebraMap F (SplittingField q)) p
hp : IsSolvable (Gal p)
hq : IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) q))
K : Type u_1 := SplittingField p
⊢ IsSolvable (Gal q)
[PROOFSTEP]
let L := q.SplittingField
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p q : F[X]
hpq : Splits (algebraMap F (SplittingField q)) p
hp : IsSolvable (Gal p)
hq : IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) q))
K : Type u_1 := SplittingField p
L : Type u_1 := SplittingField q
⊢ IsSolvable (Gal q)
[PROOFSTEP]
haveI : Fact (p.Splits (algebraMap F L)) := ⟨hpq⟩
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p q : F[X]
hpq : Splits (algebraMap F (SplittingField q)) p
hp : IsSolvable (Gal p)
hq : IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) q))
K : Type u_1 := SplittingField p
L : Type u_1 := SplittingField q
this : Fact (Splits (algebraMap F L) p)
⊢ IsSolvable (Gal q)
[PROOFSTEP]
let ϕ : (L ≃ₐ[K] L) ≃* (q.map (algebraMap F K)).Gal := (IsSplittingField.algEquiv L (q.map (algebraMap F K))).autCongr
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p q : F[X]
hpq : Splits (algebraMap F (SplittingField q)) p
hp : IsSolvable (Gal p)
hq : IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) q))
K : Type u_1 := SplittingField p
L : Type u_1 := SplittingField q
this : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* Gal (Polynomial.map (algebraMap F K) q) :=
  AlgEquiv.autCongr (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q))
⊢ IsSolvable (Gal q)
[PROOFSTEP]
have ϕ_inj : Function.Injective ϕ.toMonoidHom := ϕ.injective
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p q : F[X]
hpq : Splits (algebraMap F (SplittingField q)) p
hp : IsSolvable (Gal p)
hq : IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) q))
K : Type u_1 := SplittingField p
L : Type u_1 := SplittingField q
this : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* Gal (Polynomial.map (algebraMap F K) q) :=
  AlgEquiv.autCongr (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q))
ϕ_inj : Function.Injective ↑(MulEquiv.toMonoidHom ϕ)
⊢ IsSolvable (Gal q)
[PROOFSTEP]
haveI : IsSolvable (K ≃ₐ[F] K) := hp
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p q : F[X]
hpq : Splits (algebraMap F (SplittingField q)) p
hp : IsSolvable (Gal p)
hq : IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) q))
K : Type u_1 := SplittingField p
L : Type u_1 := SplittingField q
this✝ : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* Gal (Polynomial.map (algebraMap F K) q) :=
  AlgEquiv.autCongr (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q))
ϕ_inj : Function.Injective ↑(MulEquiv.toMonoidHom ϕ)
this : IsSolvable (K ≃ₐ[F] K)
⊢ IsSolvable (Gal q)
[PROOFSTEP]
haveI : IsSolvable (L ≃ₐ[K] L) := solvable_of_solvable_injective ϕ_inj
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p q : F[X]
hpq : Splits (algebraMap F (SplittingField q)) p
hp : IsSolvable (Gal p)
hq : IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) q))
K : Type u_1 := SplittingField p
L : Type u_1 := SplittingField q
this✝¹ : Fact (Splits (algebraMap F L) p)
ϕ : (L ≃ₐ[K] L) ≃* Gal (Polynomial.map (algebraMap F K) q) :=
  AlgEquiv.autCongr (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q))
ϕ_inj : Function.Injective ↑(MulEquiv.toMonoidHom ϕ)
this✝ : IsSolvable (K ≃ₐ[F] K)
this : IsSolvable (L ≃ₐ[K] L)
⊢ IsSolvable (Gal q)
[PROOFSTEP]
exact isSolvable_of_isScalarTower F p.SplittingField q.SplittingField
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
⊢ IsSolvable (Gal (X ^ n - 1))
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : n = 0
⊢ IsSolvable (Gal (X ^ n - 1))
[PROOFSTEP]
rw [hn, pow_zero, sub_self]
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : n = 0
⊢ IsSolvable (Gal 0)
[PROOFSTEP]
exact gal_zero_isSolvable
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
⊢ IsSolvable (Gal (X ^ n - 1))
[PROOFSTEP]
have hn' : 0 < n := pos_iff_ne_zero.mpr hn
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ IsSolvable (Gal (X ^ n - 1))
[PROOFSTEP]
have hn'' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
⊢ IsSolvable (Gal (X ^ n - 1))
[PROOFSTEP]
apply isSolvable_of_comm
[GOAL]
case neg.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
⊢ ∀ (a b : Gal (X ^ n - 1)), a * b = b * a
[PROOFSTEP]
intro σ τ
[GOAL]
case neg.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : Gal (X ^ n - 1)
⊢ σ * τ = τ * σ
[PROOFSTEP]
ext a ha
[GOAL]
case neg.h.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : Gal (X ^ n - 1)
a : SplittingField (X ^ n - 1)
ha : a ∈ rootSet (X ^ n - 1) (SplittingField (X ^ n - 1))
⊢ ↑(σ * τ) a = ↑(τ * σ) a
[PROOFSTEP]
simp only [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_one, sub_eq_zero] at ha 
[GOAL]
case neg.h.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : Gal (X ^ n - 1)
a : SplittingField (X ^ n - 1)
ha : a ^ n = 1
⊢ ↑(σ * τ) a = ↑(τ * σ) a
[PROOFSTEP]
have key : ∀ σ : (X ^ n - 1 : F[X]).Gal, ∃ m : ℕ, σ a = a ^ m :=
  by
  intro σ
  lift n to ℕ+ using hn'
  exact map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : Gal (X ^ n - 1)
a : SplittingField (X ^ n - 1)
ha : a ^ n = 1
⊢ ∀ (σ : Gal (X ^ n - 1)), ∃ m, ↑σ a = a ^ m
[PROOFSTEP]
intro σ
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ✝ τ : Gal (X ^ n - 1)
a : SplittingField (X ^ n - 1)
ha : a ^ n = 1
σ : Gal (X ^ n - 1)
⊢ ∃ m, ↑σ a = a ^ m
[PROOFSTEP]
lift n to ℕ+ using hn'
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ+
hn : ¬↑n = 0
hn'' : X ^ ↑n - 1 ≠ 0
σ✝ τ : Gal (X ^ ↑n - 1)
a : SplittingField (X ^ ↑n - 1)
ha : a ^ ↑n = 1
σ : Gal (X ^ ↑n - 1)
⊢ ∃ m, ↑σ a = a ^ m
[PROOFSTEP]
exact map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)
[GOAL]
case neg.h.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : Gal (X ^ n - 1)
a : SplittingField (X ^ n - 1)
ha : a ^ n = 1
key : ∀ (σ : Gal (X ^ n - 1)), ∃ m, ↑σ a = a ^ m
⊢ ↑(σ * τ) a = ↑(τ * σ) a
[PROOFSTEP]
obtain ⟨c, hc⟩ := key σ
[GOAL]
case neg.h.h.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : Gal (X ^ n - 1)
a : SplittingField (X ^ n - 1)
ha : a ^ n = 1
key : ∀ (σ : Gal (X ^ n - 1)), ∃ m, ↑σ a = a ^ m
c : ℕ
hc : ↑σ a = a ^ c
⊢ ↑(σ * τ) a = ↑(τ * σ) a
[PROOFSTEP]
obtain ⟨d, hd⟩ := key τ
[GOAL]
case neg.h.h.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : Gal (X ^ n - 1)
a : SplittingField (X ^ n - 1)
ha : a ^ n = 1
key : ∀ (σ : Gal (X ^ n - 1)), ∃ m, ↑σ a = a ^ m
c : ℕ
hc : ↑σ a = a ^ c
d : ℕ
hd : ↑τ a = a ^ d
⊢ ↑(σ * τ) a = ↑(τ * σ) a
[PROOFSTEP]
rw [σ.mul_apply, τ.mul_apply, hc, τ.map_pow, hd, σ.map_pow, hc, ← pow_mul, pow_mul']
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : a = 0
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
rw [ha, C_0, sub_zero]
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : a = 0
⊢ IsSolvable (Gal (X ^ n))
[PROOFSTEP]
exact gal_X_pow_isSolvable n
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
have ha' : algebraMap F (X ^ n - C a).SplittingField a ≠ 0 :=
  mt ((injective_iff_map_eq_zero _).mp (RingHom.injective _) a) ha
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : n = 0
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
rw [hn, pow_zero, ← C_1, ← C_sub]
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : n = 0
⊢ IsSolvable (Gal (↑C (1 - a)))
[PROOFSTEP]
exact gal_C_isSolvable (1 - a)
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
have hn' : 0 < n := pos_iff_ne_zero.mpr hn
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
have hn'' : X ^ n - C a ≠ 0 := X_pow_sub_C_ne_zero hn' a
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
have hn''' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
have mem_range :
  ∀ {c : (X ^ n - C a).SplittingField}, (c ^ n = 1 → (∃ d, algebraMap F (X ^ n - C a).SplittingField d = c)) :=
  fun {c} hc =>
  RingHom.mem_range.mp
    (minpoly.mem_range_of_degree_eq_one F c
      (h.def.resolve_left hn''' (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c))
        (minpoly.dvd F c (by rwa [map_id, AlgHom.map_sub, sub_eq_zero, aeval_X_pow, aeval_one]))))
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
c : SplittingField (X ^ n - ↑C a)
hc : c ^ n = 1
⊢ ↑(aeval c) (Polynomial.map (RingHom.id F) (X ^ n - 1)) = 0
[PROOFSTEP]
rwa [map_id, AlgHom.map_sub, sub_eq_zero, aeval_X_pow, aeval_one]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
⊢ IsSolvable (Gal (X ^ n - ↑C a))
[PROOFSTEP]
apply isSolvable_of_comm
[GOAL]
case neg.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
⊢ ∀ (a_1 b : Gal (X ^ n - ↑C a)), a_1 * b = b * a_1
[PROOFSTEP]
intro σ τ
[GOAL]
case neg.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
⊢ σ * τ = τ * σ
[PROOFSTEP]
ext b hb
[GOAL]
case neg.h.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ∈ rootSet (X ^ n - ↑C a) (SplittingField (X ^ n - ↑C a))
⊢ ↑(σ * τ) b = ↑(τ * σ) b
[PROOFSTEP]
rw [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hb 
[GOAL]
case neg.h.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
⊢ ↑(σ * τ) b = ↑(τ * σ) b
[PROOFSTEP]
have hb' : b ≠ 0 := by
  intro hb'
  rw [hb', zero_pow hn'] at hb 
  exact ha' hb.symm
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
⊢ b ≠ 0
[PROOFSTEP]
intro hb'
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b = 0
⊢ False
[PROOFSTEP]
rw [hb', zero_pow hn'] at hb 
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : 0 = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b = 0
⊢ False
[PROOFSTEP]
exact ha' hb.symm
[GOAL]
case neg.h.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
⊢ ↑(σ * τ) b = ↑(τ * σ) b
[PROOFSTEP]
have key : ∀ σ : (X ^ n - C a).Gal, ∃ c, σ b = b * algebraMap F _ c :=
  by
  intro σ
  have key : (σ b / b) ^ n = 1 := by rw [div_pow, ← σ.map_pow, hb, σ.commutes, div_self ha']
  obtain ⟨c, hc⟩ := mem_range key
  use c
  rw [hc, mul_div_cancel' (σ b) hb']
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
⊢ ∀ (σ : Gal (X ^ n - ↑C a)), ∃ c, ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
[PROOFSTEP]
intro σ
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ✝ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
σ : Gal (X ^ n - ↑C a)
⊢ ∃ c, ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
[PROOFSTEP]
have key : (σ b / b) ^ n = 1 := by rw [div_pow, ← σ.map_pow, hb, σ.commutes, div_self ha']
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ✝ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
σ : Gal (X ^ n - ↑C a)
⊢ (↑σ b / b) ^ n = 1
[PROOFSTEP]
rw [div_pow, ← σ.map_pow, hb, σ.commutes, div_self ha']
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ✝ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
σ : Gal (X ^ n - ↑C a)
key : (↑σ b / b) ^ n = 1
⊢ ∃ c, ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
[PROOFSTEP]
obtain ⟨c, hc⟩ := mem_range key
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ✝ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
σ : Gal (X ^ n - ↑C a)
key : (↑σ b / b) ^ n = 1
c : F
hc : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c = ↑σ b / b
⊢ ∃ c, ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
[PROOFSTEP]
use c
[GOAL]
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ✝ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
σ : Gal (X ^ n - ↑C a)
key : (↑σ b / b) ^ n = 1
c : F
hc : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c = ↑σ b / b
⊢ ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
[PROOFSTEP]
rw [hc, mul_div_cancel' (σ b) hb']
[GOAL]
case neg.h.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
key : ∀ (σ : Gal (X ^ n - ↑C a)), ∃ c, ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
⊢ ↑(σ * τ) b = ↑(τ * σ) b
[PROOFSTEP]
obtain ⟨c, hc⟩ := key σ
[GOAL]
case neg.h.h.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
key : ∀ (σ : Gal (X ^ n - ↑C a)), ∃ c, ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
c : F
hc : ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
⊢ ↑(σ * τ) b = ↑(τ * σ) b
[PROOFSTEP]
obtain ⟨d, hd⟩ := key τ
[GOAL]
case neg.h.h.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - ↑C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range :
  ∀ {c : SplittingField (X ^ n - ↑C a)}, c ^ n = 1 → ∃ d, ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d = c
σ τ : Gal (X ^ n - ↑C a)
b : SplittingField (X ^ n - ↑C a)
hb : b ^ n = ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) a
hb' : b ≠ 0
key : ∀ (σ : Gal (X ^ n - ↑C a)), ∃ c, ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
c : F
hc : ↑σ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) c
d : F
hd : ↑τ b = b * ↑(algebraMap F (SplittingField (X ^ n - ↑C a))) d
⊢ ↑(σ * τ) b = ↑(τ * σ) b
[PROOFSTEP]
rw [σ.mul_apply, τ.mul_apply, hc, τ.map_mul, τ.commutes, hd, σ.map_mul, σ.commutes, hc, mul_assoc, mul_assoc,
  mul_right_inj' hb', mul_comm]
[GOAL]
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
have ha' : i a ≠ 0 := mt ((injective_iff_map_eq_zero i).mp i.injective a) ha
[GOAL]
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : n = 0
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
rw [hn, pow_zero, sub_self]
[GOAL]
case pos
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : n = 0
⊢ Splits i 0
[PROOFSTEP]
exact splits_zero i
[GOAL]
case neg
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
have hn' : 0 < n := pos_iff_ne_zero.mpr hn
[GOAL]
case neg
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
have hn'' : (X ^ n - C a).degree ≠ 0 := ne_of_eq_of_ne (degree_X_pow_sub_C hn' a) (mt WithBot.coe_eq_coe.mp hn)
[GOAL]
case neg
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
obtain ⟨b, hb⟩ := exists_root_of_splits i h hn''
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : eval₂ i b (X ^ n - ↑C a) = 0
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
rw [eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] at hb 
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
have hb' : b ≠ 0 := by
  intro hb'
  rw [hb', zero_pow hn'] at hb 
  exact ha' hb.symm
[GOAL]
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
⊢ b ≠ 0
[PROOFSTEP]
intro hb'
[GOAL]
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b = 0
⊢ False
[PROOFSTEP]
rw [hb', zero_pow hn'] at hb 
[GOAL]
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : 0 = ↑i a
hb' : b = 0
⊢ False
[PROOFSTEP]
exact ha' hb.symm
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
let s := ((X ^ n - C a).map i).roots
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
have hs : _ = _ * (s.map _).prod := eq_prod_roots_of_splits h
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs :
  Polynomial.map i (X ^ n - ↑C a) =
    ↑C (↑i (leadingCoeff (X ^ n - ↑C a))) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
rw [leadingCoeff_X_pow_sub_C hn', RingHom.map_one, C_1, one_mul] at hs 
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
have hs' : Multiset.card s = n := (natDegree_eq_card_roots h).symm.trans natDegree_X_pow_sub_C
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
⊢ Splits i (X ^ n - 1)
[PROOFSTEP]
apply @splits_of_exists_multiset F E _ _ i (X ^ n - 1) (s.map fun c : E => c / b)
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
⊢ Polynomial.map i (X ^ n - 1) =
    ↑C (↑i (leadingCoeff (X ^ n - 1))) *
      Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.map (fun c => c / b) s))
[PROOFSTEP]
rw [leadingCoeff_X_pow_sub_one hn', RingHom.map_one, C_1, one_mul, Multiset.map_map]
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
⊢ Polynomial.map i (X ^ n - 1) = Multiset.prod (Multiset.map ((fun a => X - ↑C a) ∘ fun c => c / b) s)
[PROOFSTEP]
have C_mul_C : C (i a⁻¹) * C (i a) = 1 := by rw [← C_mul, ← i.map_mul, inv_mul_cancel ha, i.map_one, C_1]
[GOAL]
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
⊢ ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
[PROOFSTEP]
rw [← C_mul, ← i.map_mul, inv_mul_cancel ha, i.map_one, C_1]
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
C_mul_C : ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
⊢ Polynomial.map i (X ^ n - 1) = Multiset.prod (Multiset.map ((fun a => X - ↑C a) ∘ fun c => c / b) s)
[PROOFSTEP]
have key1 : (X ^ n - 1 : F[X]).map i = C (i a⁻¹) * ((X ^ n - C a).map i).comp (C b * X) := by
  rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, Polynomial.map_one, sub_comp, pow_comp,
    X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ← mul_assoc, C_mul_C, one_mul]
[GOAL]
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
C_mul_C : ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
⊢ Polynomial.map i (X ^ n - 1) = ↑C (↑i a⁻¹) * comp (Polynomial.map i (X ^ n - ↑C a)) (↑C b * X)
[PROOFSTEP]
rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, Polynomial.map_one, sub_comp, pow_comp,
  X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ← mul_assoc, C_mul_C, one_mul]
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
C_mul_C : ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = ↑C (↑i a⁻¹) * comp (Polynomial.map i (X ^ n - ↑C a)) (↑C b * X)
⊢ Polynomial.map i (X ^ n - 1) = Multiset.prod (Multiset.map ((fun a => X - ↑C a) ∘ fun c => c / b) s)
[PROOFSTEP]
have key2 : ((fun q : E[X] => q.comp (C b * X)) ∘ fun c : E => X - C c) = fun c : E => C b * (X - C (c / b)) :=
  by
  ext1 c
  dsimp only [Function.comp_apply]
  rw [sub_comp, X_comp, C_comp, mul_sub, ← C_mul, mul_div_cancel' c hb']
[GOAL]
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
C_mul_C : ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = ↑C (↑i a⁻¹) * comp (Polynomial.map i (X ^ n - ↑C a)) (↑C b * X)
⊢ ((fun q => comp q (↑C b * X)) ∘ fun c => X - ↑C c) = fun c => ↑C b * (X - ↑C (c / b))
[PROOFSTEP]
ext1 c
[GOAL]
case h
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
C_mul_C : ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = ↑C (↑i a⁻¹) * comp (Polynomial.map i (X ^ n - ↑C a)) (↑C b * X)
c : E
⊢ ((fun q => comp q (↑C b * X)) ∘ fun c => X - ↑C c) c = ↑C b * (X - ↑C (c / b))
[PROOFSTEP]
dsimp only [Function.comp_apply]
[GOAL]
case h
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
C_mul_C : ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = ↑C (↑i a⁻¹) * comp (Polynomial.map i (X ^ n - ↑C a)) (↑C b * X)
c : E
⊢ comp (X - ↑C c) (↑C b * X) = ↑C b * (X - ↑C (c / b))
[PROOFSTEP]
rw [sub_comp, X_comp, C_comp, mul_sub, ← C_mul, mul_div_cancel' c hb']
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
C_mul_C : ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = ↑C (↑i a⁻¹) * comp (Polynomial.map i (X ^ n - ↑C a)) (↑C b * X)
key2 : ((fun q => comp q (↑C b * X)) ∘ fun c => X - ↑C c) = fun c => ↑C b * (X - ↑C (c / b))
⊢ Polynomial.map i (X ^ n - 1) = Multiset.prod (Multiset.map ((fun a => X - ↑C a) ∘ fun c => c / b) s)
[PROOFSTEP]
rw [key1, hs, multiset_prod_comp, Multiset.map_map, key2, Multiset.prod_map_mul,
  -- Porting note: needed for `Multiset.map_const` to workshow (fun (_ : E) => C b) = Function.const E (C b) by rfl,
  Multiset.map_const, Multiset.prod_replicate, hs', ← C_pow, hb, ← mul_assoc, C_mul_C, one_mul]
[GOAL]
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
C_mul_C : ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = ↑C (↑i a⁻¹) * comp (Polynomial.map i (X ^ n - ↑C a)) (↑C b * X)
key2 : ((fun q => comp q (↑C b * X)) ∘ fun c => X - ↑C c) = fun c => ↑C b * (X - ↑C (c / b))
⊢ (fun x => ↑C b) = Function.const E (↑C b)
[PROOFSTEP]
rfl
[GOAL]
case neg.intro
F✝ : Type u_1
inst✝⁴ : Field F✝
E✝ : Type u_2
inst✝³ : Field E✝
inst✝² : Algebra F✝ E✝
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - ↑C a)
ha' : ↑i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : degree (X ^ n - ↑C a) ≠ 0
b : E
hb : b ^ n = ↑i a
hb' : b ≠ 0
s : Multiset E := roots (Polynomial.map i (X ^ n - ↑C a))
hs : Polynomial.map i (X ^ n - ↑C a) = Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hs' : ↑Multiset.card s = n
C_mul_C : ↑C (↑i a⁻¹) * ↑C (↑i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = ↑C (↑i a⁻¹) * comp (Polynomial.map i (X ^ n - ↑C a)) (↑C b * X)
key2 : ((fun q => comp q (↑C b * X)) ∘ fun c => X - ↑C c) = fun c => ↑C b * (X - ↑C (c / b))
⊢ Multiset.prod (Multiset.map (fun c => X - ↑C (c / b)) s) =
    Multiset.prod (Multiset.map ((fun a => X - ↑C a) ∘ fun c => c / b) s)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
⊢ IsSolvable (Gal (X ^ n - ↑C x))
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
hx : x = 0
⊢ IsSolvable (Gal (X ^ n - ↑C x))
[PROOFSTEP]
rw [hx, C_0, sub_zero]
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
hx : x = 0
⊢ IsSolvable (Gal (X ^ n))
[PROOFSTEP]
exact gal_X_pow_isSolvable n
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (Gal (X ^ n - ↑C x))
[PROOFSTEP]
apply gal_isSolvable_tower (X ^ n - 1) (X ^ n - C x)
[GOAL]
case neg.hpq
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
hx : ¬x = 0
⊢ Splits (algebraMap F (SplittingField (X ^ n - ↑C x))) (X ^ n - 1)
[PROOFSTEP]
exact splits_X_pow_sub_one_of_X_pow_sub_C _ n hx (SplittingField.splits _)
[GOAL]
case neg.hp
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (Gal (X ^ n - 1))
[PROOFSTEP]
exact gal_X_pow_sub_one_isSolvable n
[GOAL]
case neg.hq
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField (X ^ n - 1))) (X ^ n - ↑C x)))
[PROOFSTEP]
rw [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C]
[GOAL]
case neg.hq
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (Gal (X ^ n - ↑C (↑(algebraMap F (SplittingField (X ^ n - 1))) x)))
[PROOFSTEP]
apply gal_X_pow_sub_C_isSolvable_aux
[GOAL]
case neg.hq.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
hx : ¬x = 0
⊢ Splits (RingHom.id (SplittingField (X ^ n - 1))) (X ^ n - 1)
[PROOFSTEP]
have key := SplittingField.splits (X ^ n - 1 : F[X])
[GOAL]
case neg.hq.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℕ
x : F
hx : ¬x = 0
key : Splits (algebraMap F (SplittingField (X ^ n - 1))) (X ^ n - 1)
⊢ Splits (RingHom.id (SplittingField (X ^ n - 1))) (X ^ n - 1)
[PROOFSTEP]
rwa [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_pow, map_X, Polynomial.map_one] at key 
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ {a b : E}, a ∈ IsSolvableByRad F → b ∈ IsSolvableByRad F → a * b ∈ IsSolvableByRad F
[PROOFSTEP]
apply IsSolvableByRad.mul
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ 1 ∈
    { carrier := IsSolvableByRad F,
        mul_mem' := (_ : ∀ (α β : E), IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)) }.carrier
[PROOFSTEP]
change IsSolvableByRad F 1
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsSolvableByRad F 1
[PROOFSTEP]
convert IsSolvableByRad.base (E := E) (1 : F)
[GOAL]
case h.e'_6
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ 1 = ↑(algebraMap F E) 1
[PROOFSTEP]
rw [RingHom.map_one]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ {a b : E},
    a ∈
        {
              toSubsemigroup :=
                { carrier := IsSolvableByRad F,
                  mul_mem' :=
                    (_ : ∀ (α β : E), IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)) },
              one_mem' := (_ : IsSolvableByRad F 1) }.toSubsemigroup.carrier →
      b ∈
          {
                toSubsemigroup :=
                  { carrier := IsSolvableByRad F,
                    mul_mem' :=
                      (_ : ∀ (α β : E), IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)) },
                one_mem' := (_ : IsSolvableByRad F 1) }.toSubsemigroup.carrier →
        a + b ∈
          {
                toSubsemigroup :=
                  { carrier := IsSolvableByRad F,
                    mul_mem' :=
                      (_ : ∀ (α β : E), IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)) },
                one_mem' := (_ : IsSolvableByRad F 1) }.toSubsemigroup.carrier
[PROOFSTEP]
apply IsSolvableByRad.add
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ 0 ∈
    {
          toSubsemigroup :=
            { carrier := IsSolvableByRad F,
              mul_mem' := (_ : ∀ (α β : E), IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)) },
          one_mem' := (_ : IsSolvableByRad F 1) }.toSubsemigroup.carrier
[PROOFSTEP]
change IsSolvableByRad F 0
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsSolvableByRad F 0
[PROOFSTEP]
convert IsSolvableByRad.base (E := E) (0 : F)
[GOAL]
case h.e'_6
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ 0 = ↑(algebraMap F E) 0
[PROOFSTEP]
rw [RingHom.map_zero]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : { x // x ∈ solvableByRad F E }
⊢ P α
[PROOFSTEP]
revert α
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : { x // x ∈ solvableByRad F E }), P α
[PROOFSTEP]
suffices ∀ α : E, IsSolvableByRad F α → ∃ β : solvableByRad F E, ↑β = α ∧ P β
  by
  intro α
  obtain ⟨α₀, hα₀, Pα⟩ := this α (Subtype.mem α)
  convert Pα
  exact Subtype.ext hα₀.symm
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
this : ∀ (α : E), IsSolvableByRad F α → ∃ β, ↑β = α ∧ P β
⊢ ∀ (α : { x // x ∈ solvableByRad F E }), P α
[PROOFSTEP]
intro α
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
this : ∀ (α : E), IsSolvableByRad F α → ∃ β, ↑β = α ∧ P β
α : { x // x ∈ solvableByRad F E }
⊢ P α
[PROOFSTEP]
obtain ⟨α₀, hα₀, Pα⟩ := this α (Subtype.mem α)
[GOAL]
case intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
this : ∀ (α : E), IsSolvableByRad F α → ∃ β, ↑β = α ∧ P β
α α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = ↑α
Pα : P α₀
⊢ P α
[PROOFSTEP]
convert Pα
[GOAL]
case h.e'_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
this : ∀ (α : E), IsSolvableByRad F α → ∃ β, ↑β = α ∧ P β
α α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = ↑α
Pα : P α₀
⊢ α = α₀
[PROOFSTEP]
exact Subtype.ext hα₀.symm
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : E), IsSolvableByRad F α → ∃ β, ↑β = α ∧ P β
[PROOFSTEP]
apply IsSolvableByRad.rec
[GOAL]
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : F), ∃ β, ↑β = ↑(algebraMap F E) α ∧ P β
[PROOFSTEP]
exact fun α => ⟨algebraMap F (solvableByRad F E) α, rfl, base α⟩
[GOAL]
case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α β : E),
    IsSolvableByRad F α →
      IsSolvableByRad F β → (∃ β, ↑β = α ∧ P β) → (∃ β_1, ↑β_1 = β ∧ P β_1) → ∃ β_1, ↑β_1 = α + β ∧ P β_1
[PROOFSTEP]
intro α β _ _ Pα Pβ
[GOAL]
case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α β : E
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
Pα : ∃ β, ↑β = α ∧ P β
Pβ : ∃ β_1, ↑β_1 = β ∧ P β_1
⊢ ∃ β_1, ↑β_1 = α + β ∧ P β_1
[PROOFSTEP]
obtain ⟨⟨α₀, hα₀, Pα⟩, β₀, hβ₀, Pβ⟩ := Pα, Pβ
[GOAL]
case add.intro.intro.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α β : E
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : { x // x ∈ solvableByRad F E }
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ∃ β_1, ↑β_1 = α + β ∧ P β_1
[PROOFSTEP]
exact ⟨α₀ + β₀, by rw [← hα₀, ← hβ₀]; rfl, add α₀ β₀ Pα Pβ⟩
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α β : E
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : { x // x ∈ solvableByRad F E }
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ↑(α₀ + β₀) = α + β
[PROOFSTEP]
rw [← hα₀, ← hβ₀]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α β : E
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : { x // x ∈ solvableByRad F E }
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ↑(α₀ + β₀) = ↑α₀ + ↑β₀
[PROOFSTEP]
rfl
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : E), IsSolvableByRad F α → (∃ β, ↑β = α ∧ P β) → ∃ β, ↑β = -α ∧ P β
[PROOFSTEP]
intro α _ Pα
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
Pα : ∃ β, ↑β = α ∧ P β
⊢ ∃ β, ↑β = -α ∧ P β
[PROOFSTEP]
obtain ⟨α₀, hα₀, Pα⟩ := Pα
[GOAL]
case neg.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
⊢ ∃ β, ↑β = -α ∧ P β
[PROOFSTEP]
exact ⟨-α₀, by rw [← hα₀]; rfl, neg α₀ Pα⟩
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
⊢ ↑(-α₀) = -α
[PROOFSTEP]
rw [← hα₀]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
⊢ ↑(-α₀) = -↑α₀
[PROOFSTEP]
rfl
[GOAL]
case mul
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α β : E),
    IsSolvableByRad F α →
      IsSolvableByRad F β → (∃ β, ↑β = α ∧ P β) → (∃ β_1, ↑β_1 = β ∧ P β_1) → ∃ β_1, ↑β_1 = α * β ∧ P β_1
[PROOFSTEP]
intro α β _ _ Pα Pβ
[GOAL]
case mul
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α β : E
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
Pα : ∃ β, ↑β = α ∧ P β
Pβ : ∃ β_1, ↑β_1 = β ∧ P β_1
⊢ ∃ β_1, ↑β_1 = α * β ∧ P β_1
[PROOFSTEP]
obtain ⟨⟨α₀, hα₀, Pα⟩, β₀, hβ₀, Pβ⟩ := Pα, Pβ
[GOAL]
case mul.intro.intro.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α β : E
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : { x // x ∈ solvableByRad F E }
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ∃ β_1, ↑β_1 = α * β ∧ P β_1
[PROOFSTEP]
exact ⟨α₀ * β₀, by rw [← hα₀, ← hβ₀]; rfl, mul α₀ β₀ Pα Pβ⟩
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α β : E
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : { x // x ∈ solvableByRad F E }
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ↑(α₀ * β₀) = α * β
[PROOFSTEP]
rw [← hα₀, ← hβ₀]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α β : E
a✝¹ : IsSolvableByRad F α
a✝ : IsSolvableByRad F β
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
β₀ : { x // x ∈ solvableByRad F E }
hβ₀ : ↑β₀ = β
Pβ : P β₀
⊢ ↑(α₀ * β₀) = ↑α₀ * ↑β₀
[PROOFSTEP]
rfl
[GOAL]
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : E), IsSolvableByRad F α → (∃ β, ↑β = α ∧ P β) → ∃ β, ↑β = α⁻¹ ∧ P β
[PROOFSTEP]
intro α _ Pα
[GOAL]
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
Pα : ∃ β, ↑β = α ∧ P β
⊢ ∃ β, ↑β = α⁻¹ ∧ P β
[PROOFSTEP]
obtain ⟨α₀, hα₀, Pα⟩ := Pα
[GOAL]
case inv.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
⊢ ∃ β, ↑β = α⁻¹ ∧ P β
[PROOFSTEP]
exact ⟨α₀⁻¹, by rw [← hα₀]; rfl, inv α₀ Pα⟩
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
⊢ ↑α₀⁻¹ = α⁻¹
[PROOFSTEP]
rw [← hα₀]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
a✝ : IsSolvableByRad F α
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α
Pα : P α₀
⊢ ↑α₀⁻¹ = (↑α₀)⁻¹
[PROOFSTEP]
rfl
[GOAL]
case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
⊢ ∀ (α : E) (n : ℕ), n ≠ 0 → IsSolvableByRad F (α ^ n) → (∃ β, ↑β = α ^ n ∧ P β) → ∃ β, ↑β = α ∧ P β
[PROOFSTEP]
intro α n hn hα Pα
[GOAL]
case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
n : ℕ
hn : n ≠ 0
hα : IsSolvableByRad F (α ^ n)
Pα : ∃ β, ↑β = α ^ n ∧ P β
⊢ ∃ β, ↑β = α ∧ P β
[PROOFSTEP]
obtain ⟨α₀, hα₀, Pα⟩ := Pα
[GOAL]
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
n : ℕ
hn : n ≠ 0
hα : IsSolvableByRad F (α ^ n)
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α ^ n
Pα : P α₀
⊢ ∃ β, ↑β = α ∧ P β
[PROOFSTEP]
refine' ⟨⟨α, IsSolvableByRad.rad α n hn hα⟩, rfl, rad _ n hn _⟩
[GOAL]
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
n : ℕ
hn : n ≠ 0
hα : IsSolvableByRad F (α ^ n)
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α ^ n
Pα : P α₀
⊢ P ({ val := α, property := (_ : IsSolvableByRad F α) } ^ n)
[PROOFSTEP]
convert Pα
[GOAL]
case h.e'_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
P : { x // x ∈ solvableByRad F E } → Prop
base : ∀ (α : F), P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
add : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α + β)
neg : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P (-α)
mul : ∀ (α β : { x // x ∈ solvableByRad F E }), P α → P β → P (α * β)
inv : ∀ (α : { x // x ∈ solvableByRad F E }), P α → P α⁻¹
rad : ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → P (α ^ n) → P α
α : E
n : ℕ
hn : n ≠ 0
hα : IsSolvableByRad F (α ^ n)
α₀ : { x // x ∈ solvableByRad F E }
hα₀ : ↑α₀ = α ^ n
Pα : P α₀
⊢ { val := α, property := (_ : IsSolvableByRad F α) } ^ n = α₀
[PROOFSTEP]
exact Subtype.ext (Eq.trans ((solvableByRad F E).coe_pow _ n) hα₀.symm)
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
⊢ IsIntegral F α
[PROOFSTEP]
revert α
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : { x // x ∈ solvableByRad F E }), IsIntegral F α
[PROOFSTEP]
apply solvableByRad.induction
[GOAL]
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : F), IsIntegral F (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)
[PROOFSTEP]
exact fun _ => isIntegral_algebraMap
[GOAL]
case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α β : { x // x ∈ solvableByRad F E }), IsIntegral F α → IsIntegral F β → IsIntegral F (α + β)
[PROOFSTEP]
exact fun _ _ => isIntegral_add
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : { x // x ∈ solvableByRad F E }), IsIntegral F α → IsIntegral F (-α)
[PROOFSTEP]
exact fun _ => isIntegral_neg
[GOAL]
case mul
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α β : { x // x ∈ solvableByRad F E }), IsIntegral F α → IsIntegral F β → IsIntegral F (α * β)
[PROOFSTEP]
exact fun _ _ => isIntegral_mul
[GOAL]
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : { x // x ∈ solvableByRad F E }), IsIntegral F α → IsIntegral F α⁻¹
[PROOFSTEP]
intro α hα
[GOAL]
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
hα : IsIntegral F α
⊢ IsIntegral F α⁻¹
[PROOFSTEP]
exact
  Subalgebra.inv_mem_of_algebraic (integralClosure F (solvableByRad F E))
    (show IsAlgebraic F ↑(⟨α, hα⟩ : integralClosure F (solvableByRad F E)) from isAlgebraic_iff_isIntegral.mpr hα)
[GOAL]
case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ), n ≠ 0 → IsIntegral F (α ^ n) → IsIntegral F α
[PROOFSTEP]
intro α n hn hα
[GOAL]
case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
⊢ IsIntegral F α
[PROOFSTEP]
obtain ⟨p, h1, h2⟩ := isAlgebraic_iff_isIntegral.mpr hα
[GOAL]
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : ↑(aeval (α ^ n)) p = 0
⊢ IsIntegral F α
[PROOFSTEP]
refine'
  isAlgebraic_iff_isIntegral.mp
    ⟨p.comp (X ^ n), ⟨fun h => h1 (leadingCoeff_eq_zero.mp _), by rw [aeval_comp, aeval_X_pow, h2]⟩⟩
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : ↑(aeval (α ^ n)) p = 0
⊢ ↑(aeval α) (comp p (X ^ n)) = 0
[PROOFSTEP]
rw [aeval_comp, aeval_X_pow, h2]
[GOAL]
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : ↑(aeval (α ^ n)) p = 0
h : comp p (X ^ n) = 0
⊢ leadingCoeff p = 0
[PROOFSTEP]
rwa [← leadingCoeff_eq_zero, leadingCoeff_comp, leadingCoeff_X_pow, one_pow, mul_one] at h 
[GOAL]
case rad.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : IsIntegral F (α ^ n)
p : F[X]
h1 : p ≠ 0
h2 : ↑(aeval (α ^ n)) p = 0
h : leadingCoeff (comp p (X ^ n)) = 0
⊢ natDegree (X ^ n) ≠ 0
[PROOFSTEP]
rwa [natDegree_X_pow]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
⊢ P α
[PROOFSTEP]
let p := minpoly F (α ^ n)
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
⊢ P α
[PROOFSTEP]
have hp : p.comp (X ^ n) ≠ 0 := by
  intro h
  cases' comp_eq_zero_iff.mp h with h' h'
  · exact minpoly.ne_zero (isIntegral (α ^ n)) h'
  · exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
⊢ comp p (X ^ n) ≠ 0
[PROOFSTEP]
intro h
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
h : comp p (X ^ n) = 0
⊢ False
[PROOFSTEP]
cases' comp_eq_zero_iff.mp h with h' h'
[GOAL]
case inl
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
h : comp p (X ^ n) = 0
h' : p = 0
⊢ False
[PROOFSTEP]
exact minpoly.ne_zero (isIntegral (α ^ n)) h'
[GOAL]
case inr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
h : comp p (X ^ n) = 0
h' : eval (coeff (X ^ n) 0) p = 0 ∧ X ^ n = ↑C (coeff (X ^ n) 0)
⊢ False
[PROOFSTEP]
exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
h : comp p (X ^ n) = 0
h' : eval (coeff (X ^ n) 0) p = 0 ∧ X ^ n = ↑C (coeff (X ^ n) 0)
⊢ n = 0
[PROOFSTEP]
rw [← @natDegree_C F, ← h'.2, natDegree_X_pow]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
⊢ P α
[PROOFSTEP]
apply gal_isSolvable_of_splits
[GOAL]
case x
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
⊢ Fact (Splits (algebraMap F (SplittingField ?q)) (minpoly F α))
[PROOFSTEP]
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]))⟩
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
⊢ ↑(aeval α) (comp p (X ^ n)) = 0
[PROOFSTEP]
rw [aeval_comp, aeval_X_pow, minpoly.aeval]
[GOAL]
case hq
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
⊢ IsSolvable (Gal (comp p (X ^ n)))
[PROOFSTEP]
refine' gal_isSolvable_tower p (p.comp (X ^ n)) _ hα _
[GOAL]
case hq.refine'_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
⊢ Splits (algebraMap F (SplittingField (comp p (X ^ n)))) p
[PROOFSTEP]
exact Gal.splits_in_splittingField_of_comp _ _ (by rwa [natDegree_X_pow])
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
⊢ natDegree (X ^ n) ≠ 0
[PROOFSTEP]
rwa [natDegree_X_pow]
[GOAL]
case hq.refine'_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
⊢ IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) (comp p (X ^ n))))
[PROOFSTEP]
obtain ⟨s, hs⟩ := (splits_iff_exists_multiset _).1 (SplittingField.splits p)
[GOAL]
case hq.refine'_2.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ IsSolvable (Gal (Polynomial.map (algebraMap F (SplittingField p)) (comp p (X ^ n))))
[PROOFSTEP]
rw [map_comp, Polynomial.map_pow, map_X, hs, mul_comp, C_comp]
[GOAL]
case hq.refine'_2.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ IsSolvable
    (Gal
      (↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) *
        comp (Multiset.prod (Multiset.map (fun a => X - ↑C a) s)) (X ^ n)))
[PROOFSTEP]
apply gal_mul_isSolvable (gal_C_isSolvable _)
[GOAL]
case hq.refine'_2.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ IsSolvable (Gal (comp (Multiset.prod (Multiset.map (fun a => X - ↑C a) s)) (X ^ n)))
[PROOFSTEP]
rw [multiset_prod_comp]
[GOAL]
case hq.refine'_2.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ IsSolvable (Gal (Multiset.prod (Multiset.map (fun p_1 => comp p_1 (X ^ n)) (Multiset.map (fun a => X - ↑C a) s))))
[PROOFSTEP]
apply gal_prod_isSolvable
[GOAL]
case hq.refine'_2.intro.hs
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ ∀ (p_1 : (SplittingField p)[X]),
    p_1 ∈ Multiset.map (fun p_2 => comp p_2 (X ^ n)) (Multiset.map (fun a => X - ↑C a) s) → IsSolvable (Gal p_1)
[PROOFSTEP]
intro q hq
[GOAL]
case hq.refine'_2.intro.hs
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
q : (SplittingField p)[X]
hq : q ∈ Multiset.map (fun p_1 => comp p_1 (X ^ n)) (Multiset.map (fun a => X - ↑C a) s)
⊢ IsSolvable (Gal q)
[PROOFSTEP]
rw [Multiset.mem_map] at hq 
[GOAL]
case hq.refine'_2.intro.hs
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
q : (SplittingField p)[X]
hq : ∃ a, a ∈ Multiset.map (fun a => X - ↑C a) s ∧ comp a (X ^ n) = q
⊢ IsSolvable (Gal q)
[PROOFSTEP]
obtain ⟨q, hq, rfl⟩ := hq
[GOAL]
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
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
q : (SplittingField p)[X]
hq : q ∈ Multiset.map (fun a => X - ↑C a) s
⊢ IsSolvable (Gal (comp q (X ^ n)))
[PROOFSTEP]
rw [Multiset.mem_map] at hq 
[GOAL]
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
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
q : (SplittingField p)[X]
hq : ∃ a, a ∈ s ∧ X - ↑C a = q
⊢ IsSolvable (Gal (comp q (X ^ n)))
[PROOFSTEP]
obtain ⟨q, _, rfl⟩ := hq
[GOAL]
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
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
q : SplittingField p
left✝ : q ∈ s
⊢ IsSolvable (Gal (comp (X - ↑C q) (X ^ n)))
[PROOFSTEP]
rw [sub_comp, X_comp, C_comp]
[GOAL]
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
α✝ : E
α : { x // x ∈ solvableByRad F E }
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : comp p (X ^ n) ≠ 0
s : Multiset (SplittingField p)
hs :
  Polynomial.map (algebraMap F (SplittingField p)) p =
    ↑C (↑(algebraMap F (SplittingField p)) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
q : SplittingField p
left✝ : q ∈ s
⊢ IsSolvable (Gal (X ^ n - ↑C q))
[PROOFSTEP]
exact gal_X_pow_sub_C_isSolvable n q
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
⊢ P γ
[PROOFSTEP]
let p := minpoly F α
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
⊢ P γ
[PROOFSTEP]
let q := minpoly F β
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
⊢ P γ
[PROOFSTEP]
have hpq :=
  Polynomial.splits_of_splits_mul _ (mul_ne_zero (minpoly.ne_zero (isIntegral α)) (minpoly.ne_zero (isIntegral β)))
    (SplittingField.splits (p * q))
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
⊢ P γ
[PROOFSTEP]
let f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField :=
  Classical.choice <|
    algHom_mk_adjoin_splits
      (by
        intro x hx
        cases' hx with hx hx
        rw [hx]
        exact ⟨isIntegral α, hpq.1⟩
        cases hx
        exact ⟨isIntegral β, hpq.2⟩)
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
⊢ ∀ (s : { x // x ∈ solvableByRad F E }),
    s ∈ {α, β} → IsIntegral F s ∧ Splits (algebraMap F (SplittingField (p * q))) (minpoly F s)
[PROOFSTEP]
intro x hx
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
x : { x // x ∈ solvableByRad F E }
hx : x ∈ {α, β}
⊢ IsIntegral F x ∧ Splits (algebraMap F (SplittingField (p * q))) (minpoly F x)
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case inl
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
x : { x // x ∈ solvableByRad F E }
hx : x = α
⊢ IsIntegral F x ∧ Splits (algebraMap F (SplittingField (p * q))) (minpoly F x)
case inr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
x : { x // x ∈ solvableByRad F E }
hx : x ∈ {β}
⊢ IsIntegral F x ∧ Splits (algebraMap F (SplittingField (p * q))) (minpoly F x)
[PROOFSTEP]
rw [hx]
[GOAL]
case inl
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
x : { x // x ∈ solvableByRad F E }
hx : x = α
⊢ IsIntegral F α ∧ Splits (algebraMap F (SplittingField (p * q))) (minpoly F α)
case inr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
x : { x // x ∈ solvableByRad F E }
hx : x ∈ {β}
⊢ IsIntegral F x ∧ Splits (algebraMap F (SplittingField (p * q))) (minpoly F x)
[PROOFSTEP]
exact ⟨isIntegral α, hpq.1⟩
[GOAL]
case inr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
x : { x // x ∈ solvableByRad F E }
hx : x ∈ {β}
⊢ IsIntegral F x ∧ Splits (algebraMap F (SplittingField (p * q))) (minpoly F x)
[PROOFSTEP]
cases hx
[GOAL]
case inr.refl
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
⊢ IsIntegral F β ∧ Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
[PROOFSTEP]
exact ⟨isIntegral β, hpq.2⟩
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
⊢ P γ
[PROOFSTEP]
have key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩) :=
  by
  refine' minpoly.eq_of_irreducible_of_monic (minpoly.irreducible (isIntegral γ)) _ (minpoly.monic (isIntegral γ))
  suffices aeval (⟨γ, hγ⟩ : F⟮α, β⟯) (minpoly F γ) = 0 by
    rw [aeval_algHom_apply, this, AlgHom.map_zero]
      -- Porting note: this instance is needed for the following `apply`
  haveI :=
    @IntermediateField.toAlgebra F (solvableByRad F E) _ _ _ F⟮α, β⟯ (solvableByRad F E) _
      (Algebra.id (solvableByRad F E))
  apply (algebraMap (↥F⟮α, β⟯) (solvableByRad F E)).injective
  simp only [map_zero, _root_.map_eq_zero]
    -- Porting note: end of the proof was `exact minpoly.aeval F γ`.
  apply Subtype.val_injective
  simp [Polynomial.aeval_subalgebra_coe (minpoly F γ)]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
⊢ minpoly F γ = minpoly F (↑f { val := γ, property := hγ })
[PROOFSTEP]
refine' minpoly.eq_of_irreducible_of_monic (minpoly.irreducible (isIntegral γ)) _ (minpoly.monic (isIntegral γ))
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
⊢ ↑(aeval (↑f { val := γ, property := hγ })) (minpoly F γ) = 0
[PROOFSTEP]
suffices aeval (⟨γ, hγ⟩ : F⟮α, β⟯) (minpoly F γ) = 0 by
  rw [aeval_algHom_apply, this, AlgHom.map_zero]
    -- Porting note: this instance is needed for the following `apply`
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
this : ↑(aeval { val := γ, property := hγ }) (minpoly F γ) = 0
⊢ ↑(aeval (↑f { val := γ, property := hγ })) (minpoly F γ) = 0
[PROOFSTEP]
rw [aeval_algHom_apply, this, AlgHom.map_zero]
  -- Porting note: this instance is needed for the following `apply`
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
⊢ ↑(aeval { val := γ, property := hγ }) (minpoly F γ) = 0
[PROOFSTEP]
haveI :=
  @IntermediateField.toAlgebra F (solvableByRad F E) _ _ _ F⟮α, β⟯ (solvableByRad F E) _
    (Algebra.id (solvableByRad F E))
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
this : Algebra { x // x ∈ F⟮α, β⟯ } { x // x ∈ solvableByRad F E }
⊢ ↑(aeval { val := γ, property := hγ }) (minpoly F γ) = 0
[PROOFSTEP]
apply (algebraMap (↥F⟮α, β⟯) (solvableByRad F E)).injective
[GOAL]
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
this : Algebra { x // x ∈ F⟮α, β⟯ } { x // x ∈ solvableByRad F E }
⊢ ↑(algebraMap { x // x ∈ F⟮α, β⟯ } { x // x ∈ solvableByRad F E })
      (↑(aeval { val := γ, property := hγ }) (minpoly F γ)) =
    ↑(algebraMap { x // x ∈ F⟮α, β⟯ } { x // x ∈ solvableByRad F E }) 0
[PROOFSTEP]
simp only [map_zero, _root_.map_eq_zero]
  -- Porting note: end of the proof was `exact minpoly.aeval F γ`.
[GOAL]
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
this : Algebra { x // x ∈ F⟮α, β⟯ } { x // x ∈ solvableByRad F E }
⊢ ↑(aeval { val := γ, property := hγ }) (minpoly F γ) = 0
[PROOFSTEP]
apply Subtype.val_injective
[GOAL]
case a.a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
this : Algebra { x // x ∈ F⟮α, β⟯ } { x // x ∈ solvableByRad F E }
⊢ ↑(↑(aeval { val := γ, property := hγ }) (minpoly F γ)) = ↑0
[PROOFSTEP]
simp [Polynomial.aeval_subalgebra_coe (minpoly F γ)]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
key : minpoly F γ = minpoly F (↑f { val := γ, property := hγ })
⊢ P γ
[PROOFSTEP]
rw [P, key]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
key : minpoly F γ = minpoly F (↑f { val := γ, property := hγ })
⊢ IsSolvable (Gal (minpoly F (↑f { val := γ, property := hγ })))
[PROOFSTEP]
refine' gal_isSolvable_of_splits ⟨Normal.splits _ (f ⟨γ, hγ⟩)⟩ (gal_mul_isSolvable hα hβ)
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α β γ : { x // x ∈ solvableByRad F E }
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (SplittingField (p * q))) (minpoly F α) ∧
    Splits (algebraMap F (SplittingField (p * q))) (minpoly F β)
f : { x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q) :=
  Classical.choice (_ : Nonempty ({ x // x ∈ F⟮α, β⟯ } →ₐ[F] SplittingField (p * q)))
key : minpoly F γ = minpoly F (↑f { val := γ, property := hγ })
⊢ Normal F ((fun x => SplittingField (p * q)) { val := γ, property := hγ })
[PROOFSTEP]
apply SplittingField.instNormal
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : { x // x ∈ solvableByRad F E }
⊢ IsSolvable (Gal (minpoly F α))
[PROOFSTEP]
revert α
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : { x // x ∈ solvableByRad F E }), IsSolvable (Gal (minpoly F α))
[PROOFSTEP]
apply solvableByRad.induction
[GOAL]
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : F), IsSolvable (Gal (minpoly F (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)))
[PROOFSTEP]
exact fun α => by rw [minpoly.eq_X_sub_C (solvableByRad F E)]; exact gal_X_sub_C_isSolvable α
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : F
⊢ IsSolvable (Gal (minpoly F (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)))
[PROOFSTEP]
rw [minpoly.eq_X_sub_C (solvableByRad F E)]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α✝ : E
α : F
⊢ IsSolvable (Gal (X - ↑C α))
[PROOFSTEP]
exact gal_X_sub_C_isSolvable α
[GOAL]
case add
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α β : { x // x ∈ solvableByRad F E }),
    IsSolvable (Gal (minpoly F α)) → IsSolvable (Gal (minpoly F β)) → IsSolvable (Gal (minpoly F (α + β)))
[PROOFSTEP]
exact fun α β =>
  induction2
    (add_mem (subset_adjoin F _ (Set.mem_insert α _))
      (subset_adjoin F _ (Set.mem_insert_of_mem α (Set.mem_singleton β))))
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : { x // x ∈ solvableByRad F E }), IsSolvable (Gal (minpoly F α)) → IsSolvable (Gal (minpoly F (-α)))
[PROOFSTEP]
exact fun α => induction1 (neg_mem (mem_adjoin_simple_self F α))
[GOAL]
case mul
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α β : { x // x ∈ solvableByRad F E }),
    IsSolvable (Gal (minpoly F α)) → IsSolvable (Gal (minpoly F β)) → IsSolvable (Gal (minpoly F (α * β)))
[PROOFSTEP]
exact fun α β =>
  induction2
    (mul_mem (subset_adjoin F _ (Set.mem_insert α _))
      (subset_adjoin F _ (Set.mem_insert_of_mem α (Set.mem_singleton β))))
[GOAL]
case inv
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : { x // x ∈ solvableByRad F E }), IsSolvable (Gal (minpoly F α)) → IsSolvable (Gal (minpoly F α⁻¹))
[PROOFSTEP]
exact fun α => induction1 (inv_mem (mem_adjoin_simple_self F α))
[GOAL]
case rad
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ∀ (α : { x // x ∈ solvableByRad F E }) (n : ℕ),
    n ≠ 0 → IsSolvable (Gal (minpoly F (α ^ n))) → IsSolvable (Gal (minpoly F α))
[PROOFSTEP]
exact fun α n => induction3
[GOAL]
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 (Gal q)
[PROOFSTEP]
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.eq_of_algebraMap_eq (RingHom.injective _) (isIntegral ⟨α, hα⟩) rfl]
  exact isSolvable ⟨α, hα⟩
[GOAL]
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 (Gal (q * ↑C (leadingCoeff q)⁻¹))
[PROOFSTEP]
rw [minpoly.eq_of_irreducible q_irred q_aeval, ←
  show minpoly F (⟨α, hα⟩ : solvableByRad F E) = minpoly F α from
    minpoly.eq_of_algebraMap_eq (RingHom.injective _) (isIntegral ⟨α, hα⟩) rfl]
[GOAL]
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 (Gal (minpoly F { val := α, property := hα }))
[PROOFSTEP]
exact isSolvable ⟨α, hα⟩
[GOAL]
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 (Gal (q * ↑C (leadingCoeff q)⁻¹))
⊢ IsSolvable (Gal q)
[PROOFSTEP]
refine' solvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ _)
[GOAL]
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 (Gal (q * ↑C (leadingCoeff q)⁻¹))
⊢ q * ↑C (leadingCoeff q)⁻¹ ≠ 0
[PROOFSTEP]
rw [mul_ne_zero_iff, Ne, Ne, C_eq_zero, inv_eq_zero]
[GOAL]
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 (Gal (q * ↑C (leadingCoeff q)⁻¹))
⊢ ¬q = 0 ∧ ¬leadingCoeff q = 0
[PROOFSTEP]
exact ⟨q_irred.ne_zero, leadingCoeff_ne_zero.mpr q_irred.ne_zero⟩
