[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
σ τ : Gal p
h : ∀ (x : SplittingField p), x ∈ rootSet p (SplittingField p) → ↑σ x = ↑τ x
⊢ σ = τ
[PROOFSTEP]
refine'
  AlgEquiv.ext fun x => (AlgHom.mem_equalizer σ.toAlgHom τ.toAlgHom x).mp ((SetLike.ext_iff.mp _ x).mpr Algebra.mem_top)
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
σ τ : Gal p
h : ∀ (x : SplittingField p), x ∈ rootSet p (SplittingField p) → ↑σ x = ↑τ x
x : SplittingField p
⊢ AlgHom.equalizer ↑σ ↑τ = ⊤
[PROOFSTEP]
rwa [eq_top_iff, ← SplittingField.adjoin_rootSet, Algebra.adjoin_le_iff]
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Splits (RingHom.id F) p
f : Gal p
x : SplittingField p
⊢ ↑f x = ↑default x
[PROOFSTEP]
obtain ⟨y, rfl⟩ :=
  Algebra.mem_bot.mp ((SetLike.ext_iff.mp ((IsSplittingField.splits_iff _ p).mp h) x).mp Algebra.mem_top)
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Splits (RingHom.id F) p
f : Gal p
y : F
⊢ ↑f (↑(algebraMap F (SplittingField p)) y) = ↑default (↑(algebraMap F (SplittingField p)) y)
[PROOFSTEP]
rw [AlgEquiv.commutes, AlgEquiv.commutes]
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
⊢ Function.Bijective (mapRoots p E)
[PROOFSTEP]
constructor
[GOAL]
case left
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
⊢ Function.Injective (mapRoots p E)
[PROOFSTEP]
exact fun _ _ h => Subtype.ext (RingHom.injective _ (Subtype.ext_iff.mp h))
[GOAL]
case right
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
⊢ Function.Surjective (mapRoots p E)
[PROOFSTEP]
intro y
[GOAL]
case right
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(rootSet p E)
⊢ ∃ a, mapRoots p E a = y
[PROOFSTEP]
have key :=
  roots_map (IsScalarTower.toAlgHom F p.SplittingField E : p.SplittingField →+* E)
    ((splits_id_iff_splits _).mpr (IsSplittingField.splits p.SplittingField p))
[GOAL]
case right
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(rootSet p E)
key :
  roots (map (↑(IsScalarTower.toAlgHom F (SplittingField p) E)) (map (algebraMap F (SplittingField p)) p)) =
    Multiset.map (↑↑(IsScalarTower.toAlgHom F (SplittingField p) E)) (roots (map (algebraMap F (SplittingField p)) p))
⊢ ∃ a, mapRoots p E a = y
[PROOFSTEP]
rw [map_map, AlgHom.comp_algebraMap] at key 
[GOAL]
case right
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(rootSet p E)
key :
  roots (map (algebraMap F E) p) =
    Multiset.map (↑↑(IsScalarTower.toAlgHom F (SplittingField p) E)) (roots (map (algebraMap F (SplittingField p)) p))
⊢ ∃ a, mapRoots p E a = y
[PROOFSTEP]
have hy := Subtype.mem y
[GOAL]
case right
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(rootSet p E)
key :
  roots (map (algebraMap F E) p) =
    Multiset.map (↑↑(IsScalarTower.toAlgHom F (SplittingField p) E)) (roots (map (algebraMap F (SplittingField p)) p))
hy : ↑y ∈ rootSet p E
⊢ ∃ a, mapRoots p E a = y
[PROOFSTEP]
simp only [rootSet, Finset.mem_coe, (Multiset.mem_toFinset), key, Multiset.mem_map] at hy 
[GOAL]
case right
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(rootSet p E)
key :
  roots (map (algebraMap F E) p) =
    Multiset.map (↑↑(IsScalarTower.toAlgHom F (SplittingField p) E)) (roots (map (algebraMap F (SplittingField p)) p))
hy : ∃ a, a ∈ roots (map (algebraMap F (SplittingField p)) p) ∧ ↑↑(IsScalarTower.toAlgHom F (SplittingField p) E) a = ↑y
⊢ ∃ a, mapRoots p E a = y
[PROOFSTEP]
rcases hy with ⟨x, hx1, hx2⟩
[GOAL]
case right.intro.intro
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(rootSet p E)
key :
  roots (map (algebraMap F E) p) =
    Multiset.map (↑↑(IsScalarTower.toAlgHom F (SplittingField p) E)) (roots (map (algebraMap F (SplittingField p)) p))
x : SplittingField p
hx1 : x ∈ roots (map (algebraMap F (SplittingField p)) p)
hx2 : ↑↑(IsScalarTower.toAlgHom F (SplittingField p) E) x = ↑y
⊢ ∃ a, mapRoots p E a = y
[PROOFSTEP]
exact ⟨⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr hx1⟩, Subtype.ext hx2⟩
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x✝ : ↑(rootSet p (SplittingField p))
⊢ 1 • x✝ = x✝
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x✝ : ↑(rootSet p (SplittingField p))
⊢ ↑(1 • x✝) = ↑x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x✝² x✝¹ : Gal p
x✝ : ↑(rootSet p (SplittingField p))
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x✝² x✝¹ : Gal p
x✝ : ↑(rootSet p (SplittingField p))
⊢ ↑((x✝² * x✝¹) • x✝) = ↑(x✝² • x✝¹ • x✝)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
x✝ : ↑(rootSet p E)
⊢ 1 • x✝ = x✝
[PROOFSTEP]
simp only [smul_def, Equiv.apply_symm_apply, one_smul]
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
x✝² x✝¹ : Gal p
x✝ : ↑(rootSet p E)
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝
[PROOFSTEP]
simp only [smul_def, Equiv.apply_symm_apply, Equiv.symm_apply_apply, mul_smul]
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(rootSet p E)
⊢ ↑(↑(restrict p E) ϕ • x) = ↑ϕ ↑x
[PROOFSTEP]
let ψ := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(rootSet p E)
ψ : SplittingField p ≃ₐ[F] { x // x ∈ AlgHom.range (IsScalarTower.toAlgHom F (SplittingField p) E) } :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F (SplittingField p) E)
⊢ ↑(↑(restrict p E) ϕ • x) = ↑ϕ ↑x
[PROOFSTEP]
change ↑(ψ (ψ.symm _)) = ϕ x
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(rootSet p E)
ψ : SplittingField p ≃ₐ[F] { x // x ∈ AlgHom.range (IsScalarTower.toAlgHom F (SplittingField p) E) } :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F (SplittingField p) E)
⊢ ↑(↑ψ
        (↑(AlgEquiv.symm ψ)
          (↑↑(AlgHom.restrictNormalAux (↑ϕ) (SplittingField p))
            (↑↑↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F (SplittingField p) E))
              ↑(↑(rootsEquivRoots p E).symm x))))) =
    ↑ϕ ↑x
[PROOFSTEP]
rw [AlgEquiv.apply_symm_apply ψ]
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(rootSet p E)
ψ : SplittingField p ≃ₐ[F] { x // x ∈ AlgHom.range (IsScalarTower.toAlgHom F (SplittingField p) E) } :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F (SplittingField p) E)
⊢ ↑(↑↑(AlgHom.restrictNormalAux (↑ϕ) (SplittingField p))
        (↑↑↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F (SplittingField p) E))
          ↑(↑(rootsEquivRoots p E).symm x))) =
    ↑ϕ ↑x
[PROOFSTEP]
change ϕ (rootsEquivRoots p E ((rootsEquivRoots p E).symm x)) = ϕ x
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : E ≃ₐ[F] E
x : ↑(rootSet p E)
ψ : SplittingField p ≃ₐ[F] { x // x ∈ AlgHom.range (IsScalarTower.toAlgHom F (SplittingField p) E) } :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F (SplittingField p) E)
⊢ ↑ϕ ↑(↑(rootsEquivRoots p E) (↑(rootsEquivRoots p E).symm x)) = ↑ϕ ↑x
[PROOFSTEP]
rw [Equiv.apply_symm_apply (rootsEquivRoots p E)]
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
⊢ Function.Injective ↑(galActionHom p E)
[PROOFSTEP]
rw [injective_iff_map_eq_one]
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
⊢ ∀ (a : Gal p), ↑(galActionHom p E) a = 1 → a = 1
[PROOFSTEP]
intro ϕ hϕ
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : Gal p
hϕ : ↑(galActionHom p E) ϕ = 1
⊢ ϕ = 1
[PROOFSTEP]
ext (x hx)
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : Gal p
hϕ : ↑(galActionHom p E) ϕ = 1
x : SplittingField p
hx : x ∈ rootSet p (SplittingField p)
⊢ ↑ϕ x = ↑1 x
[PROOFSTEP]
have key := Equiv.Perm.ext_iff.mp hϕ (rootsEquivRoots p E ⟨x, hx⟩)
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : Gal p
hϕ : ↑(galActionHom p E) ϕ = 1
x : SplittingField p
hx : x ∈ rootSet p (SplittingField p)
key :
  ↑(↑(galActionHom p E) ϕ) (↑(rootsEquivRoots p E) { val := x, property := hx }) =
    ↑1 (↑(rootsEquivRoots p E) { val := x, property := hx })
⊢ ↑ϕ x = ↑1 x
[PROOFSTEP]
change
  rootsEquivRoots p E (ϕ • (rootsEquivRoots p E).symm (rootsEquivRoots p E ⟨x, hx⟩)) = rootsEquivRoots p E ⟨x, hx⟩ at
  key 
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : Gal p
hϕ : ↑(galActionHom p E) ϕ = 1
x : SplittingField p
hx : x ∈ rootSet p (SplittingField p)
key :
  ↑(rootsEquivRoots p E) (ϕ • ↑(rootsEquivRoots p E).symm (↑(rootsEquivRoots p E) { val := x, property := hx })) =
    ↑(rootsEquivRoots p E) { val := x, property := hx }
⊢ ↑ϕ x = ↑1 x
[PROOFSTEP]
rw [Equiv.symm_apply_apply] at key 
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
ϕ : Gal p
hϕ : ↑(galActionHom p E) ϕ = 1
x : SplittingField p
hx : x ∈ rootSet p (SplittingField p)
key : ↑(rootsEquivRoots p E) (ϕ • { val := x, property := hx }) = ↑(rootsEquivRoots p E) { val := x, property := hx }
⊢ ↑ϕ x = ↑1 x
[PROOFSTEP]
exact Subtype.ext_iff.mp (Equiv.injective (rootsEquivRoots p E) key)
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Decidable (q = 0)
hpq : p ∣ q
⊢ restrictDvd hpq = if hq : q = 0 then 1 else restrict p (SplittingField q)
[PROOFSTEP]
unfold restrictDvd
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Decidable (q = 0)
hpq : p ∣ q
⊢ (if hq : q = 0 then 1 else restrict p (SplittingField q)) = if hq : q = 0 then 1 else restrict p (SplittingField q)
[PROOFSTEP]
convert rfl
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : p ∣ q
hq : q ≠ 0
⊢ Function.Surjective ↑(restrictDvd hpq)
[PROOFSTEP]
classical
  -- Porting note: was `simp only [restrictDvd_def, dif_neg hq, restrict_surjective]`
haveI := Fact.mk <| splits_of_splits_of_dvd (algebraMap F q.SplittingField) hq (SplittingField.splits q) hpq
simp only [restrictDvd_def, dif_neg hq]
exact restrict_surjective _ _
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : p ∣ q
hq : q ≠ 0
⊢ Function.Surjective ↑(restrictDvd hpq)
[PROOFSTEP]
haveI := Fact.mk <| splits_of_splits_of_dvd (algebraMap F q.SplittingField) hq (SplittingField.splits q) hpq
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : p ∣ q
hq : q ≠ 0
this : Fact (Splits (algebraMap F (SplittingField q)) p)
⊢ Function.Surjective ↑(restrictDvd hpq)
[PROOFSTEP]
simp only [restrictDvd_def, dif_neg hq]
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : p ∣ q
hq : q ≠ 0
this : Fact (Splits (algebraMap F (SplittingField q)) p)
⊢ Function.Surjective ↑(restrict p (SplittingField q))
[PROOFSTEP]
exact restrict_surjective _ _
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Function.Injective ↑(restrictProd p q)
[PROOFSTEP]
by_cases hpq : p * q = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : p * q = 0
⊢ Function.Injective ↑(restrictProd p q)
[PROOFSTEP]
have : Unique (p * q).Gal := by rw [hpq]; infer_instance
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : p * q = 0
⊢ Unique (Gal (p * q))
[PROOFSTEP]
rw [hpq]
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : p * q = 0
⊢ Unique (Gal 0)
[PROOFSTEP]
infer_instance
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : p * q = 0
this : Unique (Gal (p * q))
⊢ Function.Injective ↑(restrictProd p q)
[PROOFSTEP]
exact fun f g _ => Eq.trans (Unique.eq_default f) (Unique.eq_default g).symm
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
⊢ Function.Injective ↑(restrictProd p q)
[PROOFSTEP]
intro f g hfg
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg : ↑(restrictProd p q) f = ↑(restrictProd p q) g
⊢ f = g
[PROOFSTEP]
classical
simp only [restrictProd, restrictDvd_def] at hfg 
simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk.inj_iff] at hfg 
ext (x hx)
rw [rootSet_def, Polynomial.map_mul, Polynomial.roots_mul] at hx 
cases' Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h h
· haveI : Fact (p.Splits (algebraMap F (p * q).SplittingField)) :=
    ⟨splits_of_splits_of_dvd _ hpq (SplittingField.splits (p * q)) (dvd_mul_right p q)⟩
  have key :
    x =
      algebraMap p.SplittingField (p * q).SplittingField
        ((rootsEquivRoots p _).invFun ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
    Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots p _) ⟨x, _⟩).symm
  rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
  exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)
· haveI : Fact (q.Splits (algebraMap F (p * q).SplittingField)) :=
    ⟨splits_of_splits_of_dvd _ hpq (SplittingField.splits (p * q)) (dvd_mul_left q p)⟩
  have key :
    x =
      algebraMap q.SplittingField (p * q).SplittingField
        ((rootsEquivRoots q _).invFun ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
    Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots q _) ⟨x, _⟩).symm
  rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
  exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)
· rwa [Ne.def, mul_eq_zero, map_eq_zero, map_eq_zero, ← mul_eq_zero]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg : ↑(restrictProd p q) f = ↑(restrictProd p q) g
⊢ f = g
[PROOFSTEP]
simp only [restrictProd, restrictDvd_def] at hfg 
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (SplittingField (p * q)))
          (if hq : p * q = 0 then 1 else restrict q (SplittingField (p * q))))
      f =
    ↑(MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (SplittingField (p * q)))
          (if hq : p * q = 0 then 1 else restrict q (SplittingField (p * q))))
      g
⊢ f = g
[PROOFSTEP]
simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk.inj_iff] at hfg 
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
⊢ f = g
[PROOFSTEP]
ext (x hx)
[GOAL]
case neg.h
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx : x ∈ rootSet (p * q) (SplittingField (p * q))
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [rootSet_def, Polynomial.map_mul, Polynomial.roots_mul] at hx 
[GOAL]
case neg.h
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p) + roots (map (algebraMap F (SplittingField (p * q))) q)))
⊢ ↑f x = ↑g x
case neg.h
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p * map (algebraMap F (SplittingField (p * q))) q)))
⊢ map (algebraMap F (SplittingField (p * q))) p * map (algebraMap F (SplittingField (p * q))) q ≠ 0
[PROOFSTEP]
cases' Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h h
[GOAL]
case neg.h.inl
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p) + roots (map (algebraMap F (SplittingField (p * q))) q)))
h : x ∈ roots (map (algebraMap F (SplittingField (p * q))) p)
⊢ ↑f x = ↑g x
[PROOFSTEP]
haveI : Fact (p.Splits (algebraMap F (p * q).SplittingField)) :=
  ⟨splits_of_splits_of_dvd _ hpq (SplittingField.splits (p * q)) (dvd_mul_right p q)⟩
[GOAL]
case neg.h.inl
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p) + roots (map (algebraMap F (SplittingField (p * q))) q)))
h : x ∈ roots (map (algebraMap F (SplittingField (p * q))) p)
this : Fact (Splits (algebraMap F (SplittingField (p * q))) p)
⊢ ↑f x = ↑g x
[PROOFSTEP]
have key :
  x =
    algebraMap p.SplittingField (p * q).SplittingField
      ((rootsEquivRoots p _).invFun ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
  Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots p _) ⟨x, _⟩).symm
[GOAL]
case neg.h.inl
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p) + roots (map (algebraMap F (SplittingField (p * q))) q)))
h : x ∈ roots (map (algebraMap F (SplittingField (p * q))) p)
this : Fact (Splits (algebraMap F (SplittingField (p * q))) p)
key :
  x =
    ↑(algebraMap (SplittingField p) (SplittingField (p * q)))
      ↑(Equiv.invFun (rootsEquivRoots p (SplittingField (p * q)))
          { val := x, property := (_ : x ∈ Multiset.toFinset (roots (map (algebraMap F (SplittingField (p * q))) p))) })
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
[GOAL]
case neg.h.inl
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p) + roots (map (algebraMap F (SplittingField (p * q))) q)))
h : x ∈ roots (map (algebraMap F (SplittingField (p * q))) p)
this : Fact (Splits (algebraMap F (SplittingField (p * q))) p)
key :
  x =
    ↑(algebraMap (SplittingField p) (SplittingField (p * q)))
      ↑(Equiv.invFun (rootsEquivRoots p (SplittingField (p * q)))
          { val := x, property := (_ : x ∈ Multiset.toFinset (roots (map (algebraMap F (SplittingField (p * q))) p))) })
⊢ ↑(algebraMap (SplittingField p) (SplittingField (p * q)))
      (↑(AlgEquiv.restrictNormal f (SplittingField p))
        ↑(Equiv.invFun (rootsEquivRoots p (SplittingField (p * q)))
            { val := x,
              property := (_ : x ∈ Multiset.toFinset (roots (map (algebraMap F (SplittingField (p * q))) p))) })) =
    ↑(algebraMap (SplittingField p) (SplittingField (p * q)))
      (↑(AlgEquiv.restrictNormal g (SplittingField p))
        ↑(Equiv.invFun (rootsEquivRoots p (SplittingField (p * q)))
            { val := x,
              property := (_ : x ∈ Multiset.toFinset (roots (map (algebraMap F (SplittingField (p * q))) p))) }))
[PROOFSTEP]
exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)
[GOAL]
case neg.h.inr
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p) + roots (map (algebraMap F (SplittingField (p * q))) q)))
h : x ∈ roots (map (algebraMap F (SplittingField (p * q))) q)
⊢ ↑f x = ↑g x
[PROOFSTEP]
haveI : Fact (q.Splits (algebraMap F (p * q).SplittingField)) :=
  ⟨splits_of_splits_of_dvd _ hpq (SplittingField.splits (p * q)) (dvd_mul_left q p)⟩
[GOAL]
case neg.h.inr
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p) + roots (map (algebraMap F (SplittingField (p * q))) q)))
h : x ∈ roots (map (algebraMap F (SplittingField (p * q))) q)
this : Fact (Splits (algebraMap F (SplittingField (p * q))) q)
⊢ ↑f x = ↑g x
[PROOFSTEP]
have key :
  x =
    algebraMap q.SplittingField (p * q).SplittingField
      ((rootsEquivRoots q _).invFun ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
  Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots q _) ⟨x, _⟩).symm
[GOAL]
case neg.h.inr
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p) + roots (map (algebraMap F (SplittingField (p * q))) q)))
h : x ∈ roots (map (algebraMap F (SplittingField (p * q))) q)
this : Fact (Splits (algebraMap F (SplittingField (p * q))) q)
key :
  x =
    ↑(algebraMap (SplittingField q) (SplittingField (p * q)))
      ↑(Equiv.invFun (rootsEquivRoots q (SplittingField (p * q)))
          { val := x, property := (_ : x ∈ Multiset.toFinset (roots (map (algebraMap F (SplittingField (p * q))) q))) })
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
[GOAL]
case neg.h.inr
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p) + roots (map (algebraMap F (SplittingField (p * q))) q)))
h : x ∈ roots (map (algebraMap F (SplittingField (p * q))) q)
this : Fact (Splits (algebraMap F (SplittingField (p * q))) q)
key :
  x =
    ↑(algebraMap (SplittingField q) (SplittingField (p * q)))
      ↑(Equiv.invFun (rootsEquivRoots q (SplittingField (p * q)))
          { val := x, property := (_ : x ∈ Multiset.toFinset (roots (map (algebraMap F (SplittingField (p * q))) q))) })
⊢ ↑(algebraMap (SplittingField q) (SplittingField (p * q)))
      (↑(AlgEquiv.restrictNormal f (SplittingField q))
        ↑(Equiv.invFun (rootsEquivRoots q (SplittingField (p * q)))
            { val := x,
              property := (_ : x ∈ Multiset.toFinset (roots (map (algebraMap F (SplittingField (p * q))) q))) })) =
    ↑(algebraMap (SplittingField q) (SplittingField (p * q)))
      (↑(AlgEquiv.restrictNormal g (SplittingField q))
        ↑(Equiv.invFun (rootsEquivRoots q (SplittingField (p * q)))
            { val := x,
              property := (_ : x ∈ Multiset.toFinset (roots (map (algebraMap F (SplittingField (p * q))) q))) }))
[PROOFSTEP]
exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)
[GOAL]
case neg.h
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hpq : ¬p * q = 0
f g : Gal (p * q)
hfg :
  ↑(restrict p (SplittingField (p * q))) f = ↑(restrict p (SplittingField (p * q))) g ∧
    ↑(restrict q (SplittingField (p * q))) f = ↑(restrict q (SplittingField (p * q))) g
x : SplittingField (p * q)
hx :
  x ∈
    ↑(Multiset.toFinset
        (roots (map (algebraMap F (SplittingField (p * q))) p * map (algebraMap F (SplittingField (p * q))) q)))
⊢ map (algebraMap F (SplittingField (p * q))) p * map (algebraMap F (SplittingField (p * q))) q ≠ 0
[PROOFSTEP]
rwa [Ne.def, mul_eq_zero, map_eq_zero, map_eq_zero, ← mul_eq_zero]
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F (SplittingField q₁)) p₁
h₂ : Splits (algebraMap F (SplittingField q₂)) p₂
⊢ Splits (algebraMap F (SplittingField (q₁ * q₂))) (p₁ * p₂)
[PROOFSTEP]
apply splits_mul
[GOAL]
case hf
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F (SplittingField q₁)) p₁
h₂ : Splits (algebraMap F (SplittingField q₂)) p₂
⊢ Splits (algebraMap F (SplittingField (q₁ * q₂))) p₁
[PROOFSTEP]
rw [←
  (SplittingField.lift q₁
      (splits_of_splits_of_dvd (algebraMap F (q₁ * q₂).SplittingField) (mul_ne_zero hq₁ hq₂) (SplittingField.splits _)
        (dvd_mul_right q₁ q₂))).comp_algebraMap]
[GOAL]
case hf
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F (SplittingField q₁)) p₁
h₂ : Splits (algebraMap F (SplittingField q₂)) p₂
⊢ Splits
    (RingHom.comp (↑(SplittingField.lift q₁ (_ : Splits (algebraMap F (SplittingField (q₁ * q₂))) q₁)))
      (algebraMap F (SplittingField q₁)))
    p₁
[PROOFSTEP]
exact splits_comp_of_splits _ _ h₁
[GOAL]
case hg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F (SplittingField q₁)) p₁
h₂ : Splits (algebraMap F (SplittingField q₂)) p₂
⊢ Splits (algebraMap F (SplittingField (q₁ * q₂))) p₂
[PROOFSTEP]
rw [←
  (SplittingField.lift q₂
      (splits_of_splits_of_dvd (algebraMap F (q₁ * q₂).SplittingField) (mul_ne_zero hq₁ hq₂) (SplittingField.splits _)
        (dvd_mul_left q₂ q₁))).comp_algebraMap]
[GOAL]
case hg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F (SplittingField q₁)) p₁
h₂ : Splits (algebraMap F (SplittingField q₂)) p₂
⊢ Splits
    (RingHom.comp (↑(SplittingField.lift q₂ (_ : Splits (algebraMap F (SplittingField (q₁ * q₂))) q₂)))
      (algebraMap F (SplittingField q₂)))
    p₂
[PROOFSTEP]
exact splits_comp_of_splits _ _ h₂
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
⊢ Splits (algebraMap F (SplittingField (comp p q))) p
[PROOFSTEP]
let P : F[X] → Prop := fun r => r.Splits (algebraMap F (r.comp q).SplittingField)
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
⊢ Splits (algebraMap F (SplittingField (comp p q))) p
[PROOFSTEP]
have key1 : ∀ {r : F[X]}, Irreducible r → P r := by
  intro r hr
  by_cases hr' : natDegree r = 0
  · exact splits_of_natDegree_le_one _ (le_trans (le_of_eq hr') zero_le_one)
  obtain ⟨x, hx⟩ :=
    exists_root_of_splits _ (SplittingField.splits (r.comp q)) fun h =>
      hr' ((mul_eq_zero.mp (natDegree_comp.symm.trans (natDegree_eq_of_degree_eq_some h))).resolve_right hq)
  rw [← aeval_def, aeval_comp] at hx 
  have h_normal : Normal F (r.comp q).SplittingField := SplittingField.instNormal (r.comp q)
  have qx_int := Normal.isIntegral h_normal (aeval x q)
  exact
    splits_of_splits_of_dvd _ (minpoly.ne_zero qx_int) (Normal.splits h_normal _)
      ((minpoly.irreducible qx_int).dvd_symm hr (minpoly.dvd F _ hx))
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
⊢ ∀ {r : F[X]}, Irreducible r → P r
[PROOFSTEP]
intro r hr
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
r : F[X]
hr : Irreducible r
⊢ P r
[PROOFSTEP]
by_cases hr' : natDegree r = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
r : F[X]
hr : Irreducible r
hr' : natDegree r = 0
⊢ P r
[PROOFSTEP]
exact splits_of_natDegree_le_one _ (le_trans (le_of_eq hr') zero_le_one)
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
r : F[X]
hr : Irreducible r
hr' : ¬natDegree r = 0
⊢ P r
[PROOFSTEP]
obtain ⟨x, hx⟩ :=
  exists_root_of_splits _ (SplittingField.splits (r.comp q)) fun h =>
    hr' ((mul_eq_zero.mp (natDegree_comp.symm.trans (natDegree_eq_of_degree_eq_some h))).resolve_right hq)
[GOAL]
case neg.intro
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
r : F[X]
hr : Irreducible r
hr' : ¬natDegree r = 0
x : SplittingField (comp r q)
hx : eval₂ (algebraMap F (SplittingField (comp r q))) x (comp r q) = 0
⊢ P r
[PROOFSTEP]
rw [← aeval_def, aeval_comp] at hx 
[GOAL]
case neg.intro
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
r : F[X]
hr : Irreducible r
hr' : ¬natDegree r = 0
x : SplittingField (comp r q)
hx : ↑(aeval (↑(aeval x) q)) r = 0
⊢ P r
[PROOFSTEP]
have h_normal : Normal F (r.comp q).SplittingField := SplittingField.instNormal (r.comp q)
[GOAL]
case neg.intro
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
r : F[X]
hr : Irreducible r
hr' : ¬natDegree r = 0
x : SplittingField (comp r q)
hx : ↑(aeval (↑(aeval x) q)) r = 0
h_normal : Normal F (SplittingField (comp r q))
⊢ P r
[PROOFSTEP]
have qx_int := Normal.isIntegral h_normal (aeval x q)
[GOAL]
case neg.intro
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
r : F[X]
hr : Irreducible r
hr' : ¬natDegree r = 0
x : SplittingField (comp r q)
hx : ↑(aeval (↑(aeval x) q)) r = 0
h_normal : Normal F (SplittingField (comp r q))
qx_int : IsIntegral F (↑(aeval x) q)
⊢ P r
[PROOFSTEP]
exact
  splits_of_splits_of_dvd _ (minpoly.ne_zero qx_int) (Normal.splits h_normal _)
    ((minpoly.irreducible qx_int).dvd_symm hr (minpoly.dvd F _ hx))
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
⊢ Splits (algebraMap F (SplittingField (comp p q))) p
[PROOFSTEP]
have key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂) :=
  by
  intro p₁ p₂ hp₁ hp₂
  by_cases h₁ : p₁.comp q = 0
  · cases' comp_eq_zero_iff.mp h₁ with h h
    · rw [h, zero_mul]
      exact splits_zero _
    · exact False.elim (hq (by rw [h.2, natDegree_C]))
  by_cases h₂ : p₂.comp q = 0
  · cases' comp_eq_zero_iff.mp h₂ with h h
    · rw [h, mul_zero]
      exact splits_zero _
    · exact False.elim (hq (by rw [h.2, natDegree_C]))
  have key := mul_splits_in_splittingField_of_mul h₁ h₂ hp₁ hp₂
  rwa [← mul_comp] at key 
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
⊢ ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
[PROOFSTEP]
intro p₁ p₂ hp₁ hp₂
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
⊢ P (p₁ * p₂)
[PROOFSTEP]
by_cases h₁ : p₁.comp q = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : comp p₁ q = 0
⊢ P (p₁ * p₂)
[PROOFSTEP]
cases' comp_eq_zero_iff.mp h₁ with h h
[GOAL]
case pos.inl
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : comp p₁ q = 0
h : p₁ = 0
⊢ P (p₁ * p₂)
[PROOFSTEP]
rw [h, zero_mul]
[GOAL]
case pos.inl
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : comp p₁ q = 0
h : p₁ = 0
⊢ P 0
[PROOFSTEP]
exact splits_zero _
[GOAL]
case pos.inr
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : comp p₁ q = 0
h : eval (coeff q 0) p₁ = 0 ∧ q = ↑C (coeff q 0)
⊢ P (p₁ * p₂)
[PROOFSTEP]
exact False.elim (hq (by rw [h.2, natDegree_C]))
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : comp p₁ q = 0
h : eval (coeff q 0) p₁ = 0 ∧ q = ↑C (coeff q 0)
⊢ natDegree q = 0
[PROOFSTEP]
rw [h.2, natDegree_C]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬comp p₁ q = 0
⊢ P (p₁ * p₂)
[PROOFSTEP]
by_cases h₂ : p₂.comp q = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬comp p₁ q = 0
h₂ : comp p₂ q = 0
⊢ P (p₁ * p₂)
[PROOFSTEP]
cases' comp_eq_zero_iff.mp h₂ with h h
[GOAL]
case pos.inl
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬comp p₁ q = 0
h₂ : comp p₂ q = 0
h : p₂ = 0
⊢ P (p₁ * p₂)
[PROOFSTEP]
rw [h, mul_zero]
[GOAL]
case pos.inl
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬comp p₁ q = 0
h₂ : comp p₂ q = 0
h : p₂ = 0
⊢ P 0
[PROOFSTEP]
exact splits_zero _
[GOAL]
case pos.inr
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬comp p₁ q = 0
h₂ : comp p₂ q = 0
h : eval (coeff q 0) p₂ = 0 ∧ q = ↑C (coeff q 0)
⊢ P (p₁ * p₂)
[PROOFSTEP]
exact False.elim (hq (by rw [h.2, natDegree_C]))
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬comp p₁ q = 0
h₂ : comp p₂ q = 0
h : eval (coeff q 0) p₂ = 0 ∧ q = ↑C (coeff q 0)
⊢ natDegree q = 0
[PROOFSTEP]
rw [h.2, natDegree_C]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬comp p₁ q = 0
h₂ : ¬comp p₂ q = 0
⊢ P (p₁ * p₂)
[PROOFSTEP]
have key := mul_splits_in_splittingField_of_mul h₁ h₂ hp₁ hp₂
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬comp p₁ q = 0
h₂ : ¬comp p₂ q = 0
key : Splits (algebraMap F (SplittingField (comp p₁ q * comp p₂ q))) (p₁ * p₂)
⊢ P (p₁ * p₂)
[PROOFSTEP]
rwa [← mul_comp] at key 
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
⊢ Splits (algebraMap F (SplittingField (comp p q))) p
[PROOFSTEP]
induction p using WfDvdMonoid.induction_on_irreducible with
| h0 => exact splits_zero _
| hu u hu => exact splits_of_isUnit (algebraMap F (SplittingField (comp u q))) hu
| hi p₁ p₂ _ hp₂ hp₁ => apply key2 (key1 hp₂) hp₁
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
⊢ Splits (algebraMap F (SplittingField (comp p q))) p
[PROOFSTEP]
induction p using WfDvdMonoid.induction_on_irreducible with
| h0 => exact splits_zero _
| hu u hu => exact splits_of_isUnit (algebraMap F (SplittingField (comp u q))) hu
| hi p₁ p₂ _ hp₂ hp₁ => apply key2 (key1 hp₂) hp₁
[GOAL]
case h0
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
⊢ Splits (algebraMap F (SplittingField (comp 0 q))) 0
[PROOFSTEP]

| h0 => exact splits_zero _
[GOAL]
case h0
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
⊢ Splits (algebraMap F (SplittingField (comp 0 q))) 0
[PROOFSTEP]
exact splits_zero _
[GOAL]
case hu
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
u : F[X]
hu : IsUnit u
⊢ Splits (algebraMap F (SplittingField (comp u q))) u
[PROOFSTEP]

| hu u hu => exact splits_of_isUnit (algebraMap F (SplittingField (comp u q))) hu
[GOAL]
case hu
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
u : F[X]
hu : IsUnit u
⊢ Splits (algebraMap F (SplittingField (comp u q))) u
[PROOFSTEP]
exact splits_of_isUnit (algebraMap F (SplittingField (comp u q))) hu
[GOAL]
case hi
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
p₁ p₂ : F[X]
a✝ : p₁ ≠ 0
hp₂ : Irreducible p₂
hp₁ : Splits (algebraMap F (SplittingField (comp p₁ q))) p₁
⊢ Splits (algebraMap F (SplittingField (comp (p₂ * p₁) q))) (p₂ * p₁)
[PROOFSTEP]

| hi p₁ p₂ _ hp₂ hp₁ => apply key2 (key1 hp₂) hp₁
[GOAL]
case hi
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (SplittingField (comp r q))) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
p₁ p₂ : F[X]
a✝ : p₁ ≠ 0
hp₂ : Irreducible p₂
hp₁ : Splits (algebraMap F (SplittingField (comp p₁ q))) p₁
⊢ Splits (algebraMap F (SplittingField (comp (p₂ * p₁) q))) (p₂ * p₁)
[PROOFSTEP]
apply key2 (key1 hp₂) hp₁
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
⊢ Function.Surjective ↑(restrictComp p q hq)
[PROOFSTEP]
haveI : Fact (Splits (algebraMap F (SplittingField (comp p q))) p) := ⟨splits_in_splittingField_of_comp p q hq⟩
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
this : Fact (Splits (algebraMap F (SplittingField (comp p q))) p)
⊢ Function.Surjective ↑(restrictComp p q hq)
[PROOFSTEP]
rw [restrictComp]
[GOAL]
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hq : natDegree q ≠ 0
this : Fact (Splits (algebraMap F (SplittingField (comp p q))) p)
⊢ Function.Surjective
    ↑(let h := (_ : Fact (Splits (algebraMap F (SplittingField (comp p q))) p));
      restrict p (SplittingField (comp p q)))
[PROOFSTEP]
exact restrict_surjective _ _
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
⊢ natDegree p ∣ Fintype.card (Gal p)
[PROOFSTEP]
rw [Gal.card_of_separable p_irr.separable]
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
⊢ natDegree p ∣ finrank F (SplittingField p)
[PROOFSTEP]
have hp : p.degree ≠ 0 := fun h => Nat.Prime.ne_zero p_deg (natDegree_eq_zero_iff_degree_le_zero.mpr (le_of_eq h))
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
⊢ natDegree p ∣ finrank F (SplittingField p)
[PROOFSTEP]
let α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) (SplittingField.splits p) hp
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
⊢ natDegree p ∣ finrank F (SplittingField p)
[PROOFSTEP]
have hα : IsIntegral F α := Algebra.isIntegral_of_finite _ _ α
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
⊢ natDegree p ∣ finrank F (SplittingField p)
[PROOFSTEP]
use FiniteDimensional.finrank F⟮α⟯ p.SplittingField
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
⊢ finrank F (SplittingField p) = natDegree p * finrank { x // x ∈ F⟮α⟯ } (SplittingField p)
[PROOFSTEP]
suffices (minpoly F α).natDegree = p.natDegree by
  rw [← FiniteDimensional.finrank_mul_finrank F F⟮α⟯ p.SplittingField, IntermediateField.adjoin.finrank hα, this]
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
this : natDegree (minpoly F α) = natDegree p
⊢ finrank F (SplittingField p) = natDegree p * finrank { x // x ∈ F⟮α⟯ } (SplittingField p)
[PROOFSTEP]
rw [← FiniteDimensional.finrank_mul_finrank F F⟮α⟯ p.SplittingField, IntermediateField.adjoin.finrank hα, this]
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
⊢ natDegree (minpoly F α) = natDegree p
[PROOFSTEP]
suffices minpoly F α ∣ p by
  have key := (minpoly.irreducible hα).dvd_symm p_irr this
  apply le_antisymm
  · exact natDegree_le_of_dvd this p_irr.ne_zero
  · exact natDegree_le_of_dvd key (minpoly.ne_zero hα)
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
this : minpoly F α ∣ p
⊢ natDegree (minpoly F α) = natDegree p
[PROOFSTEP]
have key := (minpoly.irreducible hα).dvd_symm p_irr this
[GOAL]
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ natDegree (minpoly F α) = natDegree p
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ natDegree (minpoly F α) ≤ natDegree p
[PROOFSTEP]
exact natDegree_le_of_dvd this p_irr.ne_zero
[GOAL]
case a
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ natDegree p ≤ natDegree (minpoly F α)
[PROOFSTEP]
exact natDegree_le_of_dvd key (minpoly.ne_zero hα)
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
⊢ minpoly F α ∣ p
[PROOFSTEP]
apply minpoly.dvd F α
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
p q : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
hp : degree p ≠ 0
α : SplittingField p :=
  rootOfSplits (algebraMap F (SplittingField p)) (_ : Splits (algebraMap F (SplittingField p)) p) hp
hα : IsIntegral F α
⊢ ↑(aeval α) p = 0
[PROOFSTEP]
rw [aeval_def, map_rootOfSplits _ (SplittingField.splits p) hp]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Set.toFinset (rootSet p ℝ)) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : p = 0
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Set.toFinset (rootSet p ℝ)) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
[PROOFSTEP]
haveI : IsEmpty (p.rootSet ℂ) := by rw [hp, rootSet_zero]; infer_instance
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : p = 0
⊢ IsEmpty ↑(rootSet p ℂ)
[PROOFSTEP]
rw [hp, rootSet_zero]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : p = 0
⊢ IsEmpty ↑∅
[PROOFSTEP]
infer_instance
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : p = 0
this : IsEmpty ↑(rootSet p ℂ)
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Set.toFinset (rootSet p ℝ)) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
[PROOFSTEP]
simp_rw [(galActionHom p ℂ _).support.eq_empty_of_isEmpty, hp, rootSet_zero, Set.toFinset_empty, Finset.card_empty]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Set.toFinset (rootSet p ℝ)) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
[PROOFSTEP]
have inj : Function.Injective (IsScalarTower.toAlgHom ℚ ℝ ℂ) := (algebraMap ℝ ℂ).injective
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Set.toFinset (rootSet p ℝ)) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
[PROOFSTEP]
rw [← Finset.card_image_of_injective _ Subtype.coe_injective, ← Finset.card_image_of_injective _ inj]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))) +
      Finset.card
        (Finset.image (fun a => ↑a)
          (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))))
[PROOFSTEP]
let a : Finset ℂ := ?_
[GOAL]
case neg.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ?neg.refine_1✝
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))) +
      Finset.card
        (Finset.image (fun a => ↑a)
          (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))))
case neg.refine_1
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
⊢ Finset ℂ
[PROOFSTEP]
let b : Finset ℂ := ?_
[GOAL]
case neg.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ?neg.refine_1✝
b : Finset ℂ := ?neg.refine_2.refine_1✝
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))) +
      Finset.card
        (Finset.image (fun a => ↑a)
          (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))))
case neg.refine_2.refine_1
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ?neg.refine_1✝
⊢ Finset ℂ
case neg.refine_1
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
⊢ Finset ℂ
[PROOFSTEP]
let c : Finset ℂ :=
  ?_
    -- Porting note: was
      --   change a.card = b.card + c.card
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ?neg.refine_1✝
b : Finset ℂ := ?neg.refine_2.refine_1✝
c : Finset ℂ := ?neg.refine_2.refine_2.refine_1✝
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))) +
      Finset.card
        (Finset.image (fun a => ↑a)
          (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))))
case neg.refine_2.refine_2.refine_1
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ?neg.refine_1✝
b : Finset ℂ := ?neg.refine_2.refine_1✝
⊢ Finset ℂ
case neg.refine_2.refine_1
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ?neg.refine_1✝
⊢ Finset ℂ
case neg.refine_1
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
⊢ Finset ℂ
[PROOFSTEP]
suffices a.card = b.card + c.card by exact this
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ?neg.refine_1✝
b : Finset ℂ := ?neg.refine_2.refine_1✝
c : Finset ℂ := ?neg.refine_2.refine_2.refine_1✝
this : Finset.card a = Finset.card b + Finset.card c
⊢ Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))) +
      Finset.card
        (Finset.image (fun a => ↑a)
          (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))))
[PROOFSTEP]
exact this
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
⊢ Finset.card a = Finset.card b + Finset.card c
[PROOFSTEP]
have ha : ∀ z : ℂ, z ∈ a ↔ aeval z p = 0 := by intro z; rw [Set.mem_toFinset, mem_rootSet_of_ne hp]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
⊢ ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
[PROOFSTEP]
intro z
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
z : ℂ
⊢ z ∈ a ↔ ↑(aeval z) p = 0
[PROOFSTEP]
rw [Set.mem_toFinset, mem_rootSet_of_ne hp]
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
⊢ Finset.card a = Finset.card b + Finset.card c
[PROOFSTEP]
have hb : ∀ z : ℂ, z ∈ b ↔ aeval z p = 0 ∧ z.im = 0 := by
  intro z
  simp_rw [Finset.mem_image, Set.mem_toFinset, mem_rootSet_of_ne hp]
  constructor
  · rintro ⟨w, hw, rfl⟩
    exact ⟨by rw [aeval_algHom_apply, hw, AlgHom.map_zero], rfl⟩
  · rintro ⟨hz1, hz2⟩
    have key : IsScalarTower.toAlgHom ℚ ℝ ℂ z.re = z := by ext; rfl; rw [hz2]; rfl
    exact ⟨z.re, inj (by rwa [← aeval_algHom_apply, key, AlgHom.map_zero]), key⟩
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
⊢ ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
[PROOFSTEP]
intro z
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
⊢ z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
[PROOFSTEP]
simp_rw [Finset.mem_image, Set.mem_toFinset, mem_rootSet_of_ne hp]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
⊢ (∃ a, ↑(aeval a) p = 0 ∧ ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) a = z) ↔ ↑(aeval z) p = 0 ∧ z.im = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
⊢ (∃ a, ↑(aeval a) p = 0 ∧ ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) a = z) → ↑(aeval z) p = 0 ∧ z.im = 0
[PROOFSTEP]
rintro ⟨w, hw, rfl⟩
[GOAL]
case mp.intro.intro
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
w : ℝ
hw : ↑(aeval w) p = 0
⊢ ↑(aeval (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) w)) p = 0 ∧ (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) w).im = 0
[PROOFSTEP]
exact ⟨by rw [aeval_algHom_apply, hw, AlgHom.map_zero], rfl⟩
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
w : ℝ
hw : ↑(aeval w) p = 0
⊢ ↑(aeval (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) w)) p = 0
[PROOFSTEP]
rw [aeval_algHom_apply, hw, AlgHom.map_zero]
[GOAL]
case mpr
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
⊢ ↑(aeval z) p = 0 ∧ z.im = 0 → ∃ a, ↑(aeval a) p = 0 ∧ ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) a = z
[PROOFSTEP]
rintro ⟨hz1, hz2⟩
[GOAL]
case mpr.intro
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
hz1 : ↑(aeval z) p = 0
hz2 : z.im = 0
⊢ ∃ a, ↑(aeval a) p = 0 ∧ ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) a = z
[PROOFSTEP]
have key : IsScalarTower.toAlgHom ℚ ℝ ℂ z.re = z := by ext; rfl; rw [hz2]; rfl
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
hz1 : ↑(aeval z) p = 0
hz2 : z.im = 0
⊢ ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re = z
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
hz1 : ↑(aeval z) p = 0
hz2 : z.im = 0
⊢ (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).re = z.re
case a
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
hz1 : ↑(aeval z) p = 0
hz2 : z.im = 0
⊢ (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = z.im
[PROOFSTEP]
rfl
[GOAL]
case a
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
hz1 : ↑(aeval z) p = 0
hz2 : z.im = 0
⊢ (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = z.im
[PROOFSTEP]
rw [hz2]
[GOAL]
case a
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
hz1 : ↑(aeval z) p = 0
hz2 : z.im = 0
⊢ (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = 0
[PROOFSTEP]
rfl
[GOAL]
case mpr.intro
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
hz1 : ↑(aeval z) p = 0
hz2 : z.im = 0
key : ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re = z
⊢ ∃ a, ↑(aeval a) p = 0 ∧ ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) a = z
[PROOFSTEP]
exact ⟨z.re, inj (by rwa [← aeval_algHom_apply, key, AlgHom.map_zero]), key⟩
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
z : ℂ
hz1 : ↑(aeval z) p = 0
hz2 : z.im = 0
key : ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re = z
⊢ ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) (↑(aeval z.re) p) = ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ) 0
[PROOFSTEP]
rwa [← aeval_algHom_apply, key, AlgHom.map_zero]
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
⊢ Finset.card a = Finset.card b + Finset.card c
[PROOFSTEP]
have hc0 : ∀ w : p.rootSet ℂ, galActionHom p ℂ (restrict p ℂ (Complex.conjAe.restrictScalars ℚ)) w = w ↔ w.val.im = 0 :=
  by
  intro w
  rw [Subtype.ext_iff, galActionHom_restrict]
  exact Complex.conj_eq_iff_im
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
⊢ ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
[PROOFSTEP]
intro w
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
w : ↑(rootSet p ℂ)
⊢ ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
[PROOFSTEP]
rw [Subtype.ext_iff, galActionHom_restrict]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
w : ↑(rootSet p ℂ)
⊢ ↑(AlgEquiv.restrictScalars ℚ Complex.conjAe) ↑w = ↑w ↔ (↑w).im = 0
[PROOFSTEP]
exact Complex.conj_eq_iff_im
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
⊢ Finset.card a = Finset.card b + Finset.card c
[PROOFSTEP]
have hc : ∀ z : ℂ, z ∈ c ↔ aeval z p = 0 ∧ z.im ≠ 0 := by
  intro z
  simp_rw [Finset.mem_image]
  constructor
  · rintro ⟨w, hw, rfl⟩
    exact ⟨(mem_rootSet.mp w.2).2, mt (hc0 w).mpr (Equiv.Perm.mem_support.mp hw)⟩
  · rintro ⟨hz1, hz2⟩
    exact ⟨⟨z, mem_rootSet.mpr ⟨hp, hz1⟩⟩, Equiv.Perm.mem_support.mpr (mt (hc0 _).mp hz2), rfl⟩
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
⊢ ∀ (z : ℂ), z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
[PROOFSTEP]
intro z
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
z : ℂ
⊢ z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
[PROOFSTEP]
simp_rw [Finset.mem_image]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
z : ℂ
⊢ (∃ a,
      a ∈ Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) ∧
        ↑a = z) ↔
    ↑(aeval z) p = 0 ∧ z.im ≠ 0
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
z : ℂ
⊢ (∃ a,
      a ∈ Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) ∧
        ↑a = z) →
    ↑(aeval z) p = 0 ∧ z.im ≠ 0
[PROOFSTEP]
rintro ⟨w, hw, rfl⟩
[GOAL]
case mp.intro.intro
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
w : { x // x ∈ rootSet p ℂ }
hw : w ∈ Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))
⊢ ↑(aeval ↑w) p = 0 ∧ (↑w).im ≠ 0
[PROOFSTEP]
exact ⟨(mem_rootSet.mp w.2).2, mt (hc0 w).mpr (Equiv.Perm.mem_support.mp hw)⟩
[GOAL]
case mpr
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
z : ℂ
⊢ ↑(aeval z) p = 0 ∧ z.im ≠ 0 →
    ∃ a,
      a ∈ Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) ∧
        ↑a = z
[PROOFSTEP]
rintro ⟨hz1, hz2⟩
[GOAL]
case mpr.intro
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
z : ℂ
hz1 : ↑(aeval z) p = 0
hz2 : z.im ≠ 0
⊢ ∃ a,
    a ∈ Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) ∧ ↑a = z
[PROOFSTEP]
exact ⟨⟨z, mem_rootSet.mpr ⟨hp, hz1⟩⟩, Equiv.Perm.mem_support.mpr (mt (hc0 _).mp hz2), rfl⟩
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
⊢ Finset.card a = Finset.card b + Finset.card c
[PROOFSTEP]
rw [← Finset.card_disjoint_union]
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
⊢ Finset.card a = Finset.card (b ∪ c)
[PROOFSTEP]
apply congr_arg Finset.card
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
⊢ a = b ∪ c
[PROOFSTEP]
simp_rw [Finset.ext_iff, Finset.mem_union, ha, hb, hc]
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
⊢ ∀ (a : ℂ), ↑(aeval a) p = 0 ↔ ↑(aeval a) p = 0 ∧ a.im = 0 ∨ ↑(aeval a) p = 0 ∧ a.im ≠ 0
[PROOFSTEP]
tauto
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
⊢ Disjoint b c
[PROOFSTEP]
rw [Finset.disjoint_left]
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
⊢ ∀ ⦃a : ℂ⦄, a ∈ b → ¬a ∈ c
[PROOFSTEP]
intro z
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
z : ℂ
⊢ z ∈ b → ¬z ∈ c
[PROOFSTEP]
rw [hb, hc]
[GOAL]
case neg.refine_2.refine_2.refine_2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := Set.toFinset (rootSet p ℂ)
b : Finset ℂ := Finset.image (↑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (Set.toFinset (rootSet p ℝ))
c : Finset ℂ :=
  Finset.image (fun a => ↑a)
    (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
ha : ∀ (z : ℂ), z ∈ a ↔ ↑(aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ ↑(aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(rootSet p ℂ)),
    ↑(↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))) w = w ↔ (↑w).im = 0
hc : ∀ (z : ℂ), z ∈ c ↔ ↑(aeval z) p = 0 ∧ z.im ≠ 0
z : ℂ
⊢ ↑(aeval z) p = 0 ∧ z.im = 0 → ¬(↑(aeval z) p = 0 ∧ z.im ≠ 0)
[PROOFSTEP]
tauto
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
⊢ Function.Bijective ↑(galActionHom p ℂ)
[PROOFSTEP]
classical
have h1 : Fintype.card (p.rootSet ℂ) = p.natDegree :=
  by
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rw [Multiset.toFinset_card_of_nodup, ← natDegree_eq_card_roots]
  · exact IsAlgClosed.splits_codomain p
  · exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)
have h2 : Fintype.card p.Gal = Fintype.card (galActionHom p ℂ).range :=
  Fintype.card_congr (MonoidHom.ofInjective (galActionHom_injective p ℂ)).toEquiv
let conj := restrict p ℂ (Complex.conjAe.restrictScalars ℚ)
refine'
  ⟨galActionHom_injective p ℂ, fun x =>
    (congr_arg (Membership.mem x) (show (galActionHom p ℂ).range = ⊤ from _)).mpr (Subgroup.mem_top x)⟩
apply Equiv.Perm.subgroup_eq_top_of_swap_mem
· rwa [h1]
· rw [h1]
  convert prime_degree_dvd_card p_irr p_deg using 1
  convert h2.symm
· exact ⟨conj, rfl⟩
· rw [← Equiv.Perm.card_support_eq_two]
  apply Nat.add_left_cancel
  rw [← p_roots, ← Set.toFinset_card (rootSet p ℝ), ← Set.toFinset_card (rootSet p ℂ)]
  exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
⊢ Function.Bijective ↑(galActionHom p ℂ)
[PROOFSTEP]
have h1 : Fintype.card (p.rootSet ℂ) = p.natDegree :=
  by
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rw [Multiset.toFinset_card_of_nodup, ← natDegree_eq_card_roots]
  · exact IsAlgClosed.splits_codomain p
  · exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
⊢ Fintype.card ↑(rootSet p ℂ) = natDegree p
[PROOFSTEP]
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
⊢ Finset.card (Multiset.toFinset (roots (map (algebraMap ℚ ℂ) p))) = natDegree p
[PROOFSTEP]
rw [Multiset.toFinset_card_of_nodup, ← natDegree_eq_card_roots]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
⊢ Splits (algebraMap ℚ ℂ) p
[PROOFSTEP]
exact IsAlgClosed.splits_codomain p
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
⊢ Multiset.Nodup (roots (map (algebraMap ℚ ℂ) p))
[PROOFSTEP]
exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
⊢ Function.Bijective ↑(galActionHom p ℂ)
[PROOFSTEP]
have h2 : Fintype.card p.Gal = Fintype.card (galActionHom p ℂ).range :=
  Fintype.card_congr (MonoidHom.ofInjective (galActionHom_injective p ℂ)).toEquiv
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
⊢ Function.Bijective ↑(galActionHom p ℂ)
[PROOFSTEP]
let conj := restrict p ℂ (Complex.conjAe.restrictScalars ℚ)
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
⊢ Function.Bijective ↑(galActionHom p ℂ)
[PROOFSTEP]
refine'
  ⟨galActionHom_injective p ℂ, fun x =>
    (congr_arg (Membership.mem x) (show (galActionHom p ℂ).range = ⊤ from _)).mpr (Subgroup.mem_top x)⟩
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ MonoidHom.range (galActionHom p ℂ) = ⊤
[PROOFSTEP]
apply Equiv.Perm.subgroup_eq_top_of_swap_mem
[GOAL]
case h0
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ Nat.Prime (Fintype.card ↑(rootSet p ℂ))
[PROOFSTEP]
rwa [h1]
[GOAL]
case h1
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ Fintype.card ↑(rootSet p ℂ) ∣ Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
[PROOFSTEP]
rw [h1]
[GOAL]
case h1
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ natDegree p ∣ Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
[PROOFSTEP]
convert prime_degree_dvd_card p_irr p_deg using 1
[GOAL]
case h.e'_4
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) } = Fintype.card (Gal p)
[PROOFSTEP]
convert h2.symm
[GOAL]
case h2
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ ?τ ∈ MonoidHom.range (galActionHom p ℂ)
[PROOFSTEP]
exact ⟨conj, rfl⟩
[GOAL]
case h3
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ Equiv.Perm.IsSwap (↑(galActionHom p ℂ) conj)
[PROOFSTEP]
rw [← Equiv.Perm.card_support_eq_two]
[GOAL]
case h3
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) conj)) = 2
[PROOFSTEP]
apply Nat.add_left_cancel
[GOAL]
case h3.a
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ ?h3.n + Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) conj)) = ?h3.n + 2
case h3.n
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ ℕ
[PROOFSTEP]
rw [← p_roots, ← Set.toFinset_card (rootSet p ℝ), ← Set.toFinset_card (rootSet p ℂ)]
[GOAL]
case h3.a
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots : Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
h1 : Fintype.card ↑(rootSet p ℂ) = natDegree p
h2 : Fintype.card (Gal p) = Fintype.card { x // x ∈ MonoidHom.range (galActionHom p ℂ) }
conj : (fun x => Gal p) (AlgEquiv.restrictScalars ℚ Complex.conjAe) :=
  ↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)
x : Equiv.Perm ↑(rootSet p ℂ)
⊢ Finset.card (Set.toFinset (rootSet p ℝ)) + Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) conj)) =
    Finset.card (Set.toFinset (rootSet p ℂ))
[PROOFSTEP]
exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 : Fintype.card ↑(rootSet p ℝ) + 1 ≤ Fintype.card ↑(rootSet p ℂ)
p_roots2 : Fintype.card ↑(rootSet p ℂ) ≤ Fintype.card ↑(rootSet p ℝ) + 3
⊢ Function.Bijective ↑(galActionHom p ℂ)
[PROOFSTEP]
apply galActionHom_bijective_of_prime_degree p_irr p_deg
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 : Fintype.card ↑(rootSet p ℝ) + 1 ≤ Fintype.card ↑(rootSet p ℂ)
p_roots2 : Fintype.card ↑(rootSet p ℂ) ≤ Fintype.card ↑(rootSet p ℝ) + 3
⊢ Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
[PROOFSTEP]
let n := (galActionHom p ℂ (restrict p ℂ (Complex.conjAe.restrictScalars ℚ))).support.card
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 : Fintype.card ↑(rootSet p ℝ) + 1 ≤ Fintype.card ↑(rootSet p ℂ)
p_roots2 : Fintype.card ↑(rootSet p ℂ) ≤ Fintype.card ↑(rootSet p ℝ) + 3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
⊢ Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
[PROOFSTEP]
have hn : 2 ∣ n :=
  Equiv.Perm.two_dvd_card_support
    (by
      rw [← MonoidHom.map_pow, ← MonoidHom.map_pow,
        show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from AlgEquiv.ext Complex.conj_conj, MonoidHom.map_one,
        MonoidHom.map_one])
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 : Fintype.card ↑(rootSet p ℝ) + 1 ≤ Fintype.card ↑(rootSet p ℂ)
p_roots2 : Fintype.card ↑(rootSet p ℂ) ≤ Fintype.card ↑(rootSet p ℝ) + 3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
⊢ ↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)) ^ 2 = 1
[PROOFSTEP]
rw [← MonoidHom.map_pow, ← MonoidHom.map_pow,
  show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from AlgEquiv.ext Complex.conj_conj, MonoidHom.map_one,
  MonoidHom.map_one]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 : Fintype.card ↑(rootSet p ℝ) + 1 ≤ Fintype.card ↑(rootSet p ℂ)
p_roots2 : Fintype.card ↑(rootSet p ℂ) ≤ Fintype.card ↑(rootSet p ℝ) + 3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
hn : 2 ∣ n
⊢ Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
[PROOFSTEP]
have key := card_complex_roots_eq_card_real_add_card_not_gal_inv p
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 : Fintype.card ↑(rootSet p ℝ) + 1 ≤ Fintype.card ↑(rootSet p ℂ)
p_roots2 : Fintype.card ↑(rootSet p ℂ) ≤ Fintype.card ↑(rootSet p ℝ) + 3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
hn : 2 ∣ n
key :
  Finset.card (Set.toFinset (rootSet p ℂ)) =
    Finset.card (Set.toFinset (rootSet p ℝ)) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
⊢ Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
[PROOFSTEP]
simp_rw [Set.toFinset_card] at key 
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 : Fintype.card ↑(rootSet p ℝ) + 1 ≤ Fintype.card ↑(rootSet p ℂ)
p_roots2 : Fintype.card ↑(rootSet p ℂ) ≤ Fintype.card ↑(rootSet p ℝ) + 3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
hn : 2 ∣ n
key :
  Fintype.card ↑(rootSet p ℂ) =
    Fintype.card ↑(rootSet p ℝ) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
⊢ Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
[PROOFSTEP]
rw [key, add_le_add_iff_left] at p_roots1 p_roots2 
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 :
  1 ≤
    Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
p_roots2 :
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))) ≤
    3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
hn : 2 ∣ n
key :
  Fintype.card ↑(rootSet p ℂ) =
    Fintype.card ↑(rootSet p ℝ) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
⊢ Fintype.card ↑(rootSet p ℂ) = Fintype.card ↑(rootSet p ℝ) + 2
[PROOFSTEP]
rw [key, add_right_inj]
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 :
  1 ≤
    Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
p_roots2 :
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))) ≤
    3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
hn : 2 ∣ n
key :
  Fintype.card ↑(rootSet p ℂ) =
    Fintype.card ↑(rootSet p ℝ) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
⊢ Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))) =
    2
[PROOFSTEP]
suffices ∀ m : ℕ, 2 ∣ m → 1 ≤ m → m ≤ 3 → m = 2 by exact this n hn p_roots1 p_roots2
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 :
  1 ≤
    Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
p_roots2 :
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))) ≤
    3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
hn : 2 ∣ n
key :
  Fintype.card ↑(rootSet p ℂ) =
    Fintype.card ↑(rootSet p ℝ) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
this : ∀ (m : ℕ), 2 ∣ m → 1 ≤ m → m ≤ 3 → m = 2
⊢ Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))) =
    2
[PROOFSTEP]
exact this n hn p_roots1 p_roots2
[GOAL]
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 :
  1 ≤
    Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
p_roots2 :
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))) ≤
    3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
hn : 2 ∣ n
key :
  Fintype.card ↑(rootSet p ℂ) =
    Fintype.card ↑(rootSet p ℝ) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
⊢ ∀ (m : ℕ), 2 ∣ m → 1 ≤ m → m ≤ 3 → m = 2
[PROOFSTEP]
rintro m ⟨k, rfl⟩ h2 h3
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
p✝ q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime (natDegree p)
p_roots1 :
  1 ≤
    Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
p_roots2 :
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe)))) ≤
    3
n : ℕ :=
  Finset.card (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
hn : 2 ∣ n
key :
  Fintype.card ↑(rootSet p ℂ) =
    Fintype.card ↑(rootSet p ℝ) +
      Finset.card
        (Equiv.Perm.support (↑(galActionHom p ℂ) (↑(restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))
k : ℕ
h2 : 1 ≤ 2 * k
h3 : 2 * k ≤ 3
⊢ 2 * k = 2
[PROOFSTEP]
exact
  le_antisymm (Nat.lt_succ_iff.mp (lt_of_le_of_ne h3 (show 2 * k ≠ 2 * 1 + 1 from Nat.two_mul_ne_two_mul_add_one)))
    (Nat.succ_le_iff.mpr (lt_of_le_of_ne h2 (show 2 * 0 + 1 ≠ 2 * k from Nat.two_mul_ne_two_mul_add_one.symm)))
