[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ Irreducible (factor f)
[PROOFSTEP]
rw [factor]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ Irreducible (if H : ∃ g, Irreducible g ∧ g ∣ f then Classical.choose H else X)
[PROOFSTEP]
split_ifs with H
[GOAL]
case pos
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
H : ∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible (Classical.choose H)
[PROOFSTEP]
exact (Classical.choose_spec H).1
[GOAL]
case neg
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
H : ¬∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible X
[PROOFSTEP]
exact irreducible_X
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
⊢ factor f ∣ f
[PROOFSTEP]
by_cases hf2 : f = 0
[GOAL]
case pos
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ factor f ∣ f
[PROOFSTEP]
rw [hf2]
[GOAL]
case pos
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ factor 0 ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case neg
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ factor f ∣ f
[PROOFSTEP]
rw [factor, dif_pos (WfDvdMonoid.exists_irreducible_factor hf1 hf2)]
[GOAL]
case neg
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ Classical.choose (_ : ∃ i, Irreducible i ∧ i ∣ f) ∣ f
[PROOFSTEP]
exact (Classical.choose_spec <| WfDvdMonoid.exists_irreducible_factor hf1 hf2).2
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf : natDegree f ≠ 0
⊢ (X - ↑C (AdjoinRoot.root (factor f))) * removeFactor f = map (AdjoinRoot.of (factor f)) f
[PROOFSTEP]
let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf : natDegree f ≠ 0
g : K[X]
hg : f = factor f * g
⊢ (X - ↑C (AdjoinRoot.root (factor f))) * removeFactor f = map (AdjoinRoot.of (factor f)) f
[PROOFSTEP]
apply (mul_divByMonic_eq_iff_isRoot (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
hf : natDegree f ≠ 0
g : K[X]
hg : f = factor f * g
⊢ IsRoot (map (AdjoinRoot.of (factor f)) f) (AdjoinRoot.root (factor f))
[PROOFSTEP]
rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ natDegree (removeFactor f) = natDegree f - 1
[PROOFSTEP]
rw [removeFactor, natDegree_divByMonic (map (AdjoinRoot.of f.factor) f) (monic_X_sub_C _), natDegree_map,
  natDegree_X_sub_C]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
n : ℕ
hfn : natDegree f = n + 1
⊢ natDegree (removeFactor f) = n
[PROOFSTEP]
rw [natDegree_removeFactor, hfn, n.add_sub_cancel]
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), natDegree f = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : natDegree f = Nat.succ n
⊢ Splits (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f
[PROOFSTEP]
rw [← splits_id_iff_splits, algebraMap_succ, ← map_map, splits_id_iff_splits, ←
  X_sub_C_mul_removeFactor f fun h => by rw [h] at hf ; cases hf]
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), natDegree f = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : natDegree f = Nat.succ n
h : natDegree f = 0
⊢ False
[PROOFSTEP]
rw [h] at hf 
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), natDegree f = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : 0 = Nat.succ n
h : natDegree f = 0
⊢ False
[PROOFSTEP]
cases hf
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), natDegree f = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : natDegree f = Nat.succ n
⊢ Splits (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
    ((X - ↑C (AdjoinRoot.root (factor f))) * removeFactor f)
[PROOFSTEP]
exact splits_mul _ (splits_X_sub_C _) (ih _ (natDegree_removeFactor' hf))
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
⊢ Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f))) = ⊤
[PROOFSTEP]
have hndf : f.natDegree ≠ 0 := by intro h; rw [h] at hfn ; cases hfn
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
⊢ natDegree f ≠ 0
[PROOFSTEP]
intro h
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
h : natDegree f = 0
⊢ False
[PROOFSTEP]
rw [h] at hfn 
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : 0 = Nat.succ n
h : natDegree f = 0
⊢ False
[PROOFSTEP]
cases hfn
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
⊢ Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f))) = ⊤
[PROOFSTEP]
have hfn0 : f ≠ 0 := by intro h; rw [h] at hndf ; exact hndf rfl
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
⊢ f ≠ 0
[PROOFSTEP]
intro h
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
h : f = 0
⊢ False
[PROOFSTEP]
rw [h] at hndf 
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree 0 ≠ 0
h : f = 0
⊢ False
[PROOFSTEP]
exact hndf rfl
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
⊢ Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f))) = ⊤
[PROOFSTEP]
have hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0 := map_ne_zero hfn0
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 : map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f ≠ 0
⊢ Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux (Nat.succ n) f)) f))) = ⊤
[PROOFSTEP]
rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
        (X - ↑C (AdjoinRoot.root (factor f))) *
      map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f) ≠
    0
⊢ Algebra.adjoin K
      ↑(Multiset.toFinset
          (roots
            (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
                (X - ↑C (AdjoinRoot.root (factor f))) *
              map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f)))) =
    ⊤
[PROOFSTEP]
rw [roots_mul hmf0, Polynomial.map_sub, map_X, map_C, roots_X_sub_C, Multiset.toFinset_add, Finset.coe_union,
  Multiset.toFinset_singleton, Finset.coe_singleton, Algebra.adjoin_union_eq_adjoin_adjoin, ← Set.image_singleton,
  Algebra.adjoin_algebraMap K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor), AdjoinRoot.adjoinRoot_eq_top,
  Algebra.map_top]
  /- Porting note: was `rw [IsScalarTower.adjoin_range_toAlgHom K (AdjoinRoot f.factor)
          (SplittingFieldAux n f.removeFactor)]` -/
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
        (X - ↑C (AdjoinRoot.root (factor f))) *
      map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f) ≠
    0
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin
        { x //
          x ∈ AlgHom.range (IsScalarTower.toAlgHom K (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) }
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    ⊤
[PROOFSTEP]
have :=
  IsScalarTower.adjoin_range_toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)
    (↑(f.removeFactor.map <| algebraMap (AdjoinRoot f.factor) <| SplittingFieldAux n f.removeFactor).roots.toFinset :
      Set (SplittingFieldAux n f.removeFactor))
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
        (X - ↑C (AdjoinRoot.root (factor f))) *
      map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f) ≠
    0
this :
  Subalgebra.restrictScalars K
      (Algebra.adjoin
        { x //
          x ∈ AlgHom.range (IsScalarTower.toAlgHom K (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) }
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot (factor f))
        ↑(Multiset.toFinset
            (roots (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f)))))
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin
        { x //
          x ∈ AlgHom.range (IsScalarTower.toAlgHom K (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) }
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    ⊤
[PROOFSTEP]
refine this.trans ?_
[GOAL]
F : Type u
K✝¹ : Type v
L : Type w
inst✝³ : Field K✝¹
inst✝² : Field L
inst✝¹ : Field F
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        natDegree f = n →
          Algebra.adjoin K ↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n f)) f))) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : natDegree f = Nat.succ n
hndf : natDegree f ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f)))
        (X - ↑C (AdjoinRoot.root (factor f))) *
      map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f) ≠
    0
this :
  Subalgebra.restrictScalars K
      (Algebra.adjoin
        { x //
          x ∈ AlgHom.range (IsScalarTower.toAlgHom K (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) }
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot (factor f))
        ↑(Multiset.toFinset
            (roots (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f)))))
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot (factor f))
        ↑(Multiset.toFinset
            (roots
              (map (algebraMap (AdjoinRoot (factor f)) (SplittingFieldAux n (removeFactor f))) (removeFactor f))))) =
    ⊤
[PROOFSTEP]
rw [ih _ (natDegree_removeFactor' hfn), Subalgebra.restrictScalars_top]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ Function.Surjective ↑(ofMvPolynomial f)
[PROOFSTEP]
suffices AlgHom.range (ofMvPolynomial f) = ⊤ by rw [← Set.range_iff_surjective]; rwa [SetLike.ext'_iff] at this 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
this : AlgHom.range (ofMvPolynomial f) = ⊤
⊢ Function.Surjective ↑(ofMvPolynomial f)
[PROOFSTEP]
rw [← Set.range_iff_surjective]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
this : AlgHom.range (ofMvPolynomial f) = ⊤
⊢ Set.range ↑(ofMvPolynomial f) = Set.univ
[PROOFSTEP]
rwa [SetLike.ext'_iff] at this 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ AlgHom.range (ofMvPolynomial f) = ⊤
[PROOFSTEP]
rw [ofMvPolynomial, ← Algebra.adjoin_range_eq_range_aeval K, eq_top_iff, ← adjoin_rootSet _ _ rfl]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ Algebra.adjoin K (rootSet f (SplittingFieldAux (natDegree f) f)) ≤ Algebra.adjoin K (Set.range fun i => ↑i)
[PROOFSTEP]
apply Algebra.adjoin_le
[GOAL]
case H
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
⊢ rootSet f (SplittingFieldAux (natDegree f) f) ⊆ ↑(Algebra.adjoin K (Set.range fun i => ↑i))
[PROOFSTEP]
intro α hα
[GOAL]
case H
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
α : SplittingFieldAux (natDegree f) f
hα : α ∈ rootSet f (SplittingFieldAux (natDegree f) f)
⊢ α ∈ ↑(Algebra.adjoin K (Set.range fun i => ↑i))
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
case H.a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
α : SplittingFieldAux (natDegree f) f
hα : α ∈ rootSet f (SplittingFieldAux (natDegree f) f)
⊢ α ∈ Set.range fun i => ↑i
[PROOFSTEP]
exact ⟨⟨α, hα⟩, rfl⟩
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
apply_fun e
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
⊢ ↑e (a * a⁻¹) = ↑e 1
[PROOFSTEP]
have : e a ≠ 0 := fun w' => by
  apply w
  simp at w' 
  exact w'
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
w' : ↑e a = 0
⊢ False
[PROOFSTEP]
apply w
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
w' : ↑e a = 0
⊢ a = 0
[PROOFSTEP]
simp at w' 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
w' : a = 0
⊢ a = 0
[PROOFSTEP]
exact w'
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
this : ↑e a ≠ 0
⊢ ↑e (a * a⁻¹) = ↑e 1
[PROOFSTEP]
simp only [map_mul, AlgEquiv.apply_symm_apply, ne_eq, AddEquivClass.map_eq_zero_iff, map_one]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
this : ↑e a ≠ 0
⊢ ↑(algEquivSplittingFieldAux f) a * (↑(algEquivSplittingFieldAux f) a)⁻¹ = 1
[PROOFSTEP]
rw [mul_inv_cancel]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : SplittingField f
w : a ≠ 0
this : ↑e a ≠ 0
⊢ ↑(algEquivSplittingFieldAux f) a ≠ 0
[PROOFSTEP]
assumption
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
⊢ 0⁻¹ = 0
[PROOFSTEP]
simp
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
apply_fun e
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑e ↑(Rat.mk' a b) = ↑e (↑a * (↑b)⁻¹)
[PROOFSTEP]
change e (algebraMap K _ _) = _
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑e (↑(algebraMap K (SplittingField f)) ↑(Rat.mk' a b)) = ↑e (↑a * (↑b)⁻¹)
[PROOFSTEP]
simp only [map_ratCast, map_natCast, map_mul, map_intCast, AlgEquiv.commutes, AlgEquiv.apply_symm_apply]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
apply Field.ratCast_mk
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℚ
x : SplittingField f
p : MvPolynomial (↑(rootSet f (SplittingFieldAux (natDegree f) f))) K
⊢ (fun x x_1 => x • x_1) a p =
    (fun x x_1 => x * x_1) (↑(algebraMap K (MvPolynomial (↑(rootSet f (SplittingFieldAux (natDegree f) f))) K)) ↑a) p
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : SplittingField f ≃ₐ[K] SplittingFieldAux (natDegree f) f := algEquivSplittingFieldAux f
a : ℚ
x : SplittingField f
p : MvPolynomial (↑(rootSet f (SplittingFieldAux (natDegree f) f))) K
m✝ : ↑(rootSet f (SplittingFieldAux (natDegree f) f)) →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((fun x x_1 => x • x_1) a p) =
    MvPolynomial.coeff m✝
      ((fun x x_1 => x * x_1) (↑(algebraMap K (MvPolynomial (↑(rootSet f (SplittingFieldAux (natDegree f) f))) K)) ↑a)
        p)
[PROOFSTEP]
simp [MvPolynomial.algebraMap_eq, Rat.smul_def]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
⊢ L ≃ₐ[K] SplittingField f
[PROOFSTEP]
refine'
  AlgEquiv.ofBijective (lift L f <| splits (SplittingField f) f)
    ⟨RingHom.injective (lift L f <| splits (SplittingField f) f).toRingHom, _⟩
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
⊢ Function.Surjective ↑(lift L f (_ : Splits (algebraMap K (SplittingField f)) f))
[PROOFSTEP]
haveI := finiteDimensional (SplittingField f) f
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this : FiniteDimensional K (SplittingField f)
⊢ Function.Surjective ↑(lift L f (_ : Splits (algebraMap K (SplittingField f)) f))
[PROOFSTEP]
haveI := finiteDimensional L f
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this✝ : FiniteDimensional K (SplittingField f)
this : FiniteDimensional K L
⊢ Function.Surjective ↑(lift L f (_ : Splits (algebraMap K (SplittingField f)) f))
[PROOFSTEP]
have : FiniteDimensional.finrank K L = FiniteDimensional.finrank K (SplittingField f) :=
  le_antisymm
    (LinearMap.finrank_le_finrank_of_injective
      (show Function.Injective (lift L f <| splits (SplittingField f) f).toLinearMap from
        RingHom.injective (lift L f <| splits (SplittingField f) f : L →+* f.SplittingField)))
    (LinearMap.finrank_le_finrank_of_injective
      (show Function.Injective (lift (SplittingField f) f <| splits L f).toLinearMap from
        RingHom.injective (lift (SplittingField f) f <| splits L f : f.SplittingField →+* L)))
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this✝¹ : FiniteDimensional K (SplittingField f)
this✝ : FiniteDimensional K L
this : FiniteDimensional.finrank K L = FiniteDimensional.finrank K (SplittingField f)
⊢ Function.Surjective ↑(lift L f (_ : Splits (algebraMap K (SplittingField f)) f))
[PROOFSTEP]
change Function.Surjective (lift L f <| splits (SplittingField f) f).toLinearMap
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this✝¹ : FiniteDimensional K (SplittingField f)
this✝ : FiniteDimensional K L
this : FiniteDimensional.finrank K L = FiniteDimensional.finrank K (SplittingField f)
⊢ Function.Surjective ↑(AlgHom.toLinearMap (lift L f (_ : Splits (algebraMap K (SplittingField f)) f)))
[PROOFSTEP]
refine' (LinearMap.injective_iff_surjective_of_finrank_eq_finrank this).1 _
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
this✝¹ : FiniteDimensional K (SplittingField f)
this✝ : FiniteDimensional K L
this : FiniteDimensional.finrank K L = FiniteDimensional.finrank K (SplittingField f)
⊢ Function.Injective ↑(AlgHom.toLinearMap (lift L f (_ : Splits (algebraMap K (SplittingField f)) f)))
[PROOFSTEP]
exact RingHom.injective (lift L f <| splits (SplittingField f) f : L →+* f.SplittingField)
