awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
n_1 : ℕ
K_1 : Type u
inst : Field K_1
n : ℕ
ih :
  (fun (n : ℕ) ↦
      ∀ {K : Type u} [inst : Field K] (f : K[X]) (_hfn : f.natDegree = n),
        Eq (α := Subalgebra K (SplittingFieldAux n f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n f))) ⊤)
    n
K : Type u
x : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  HMul.hMul (α := (SplittingFieldAux n.succ f)[X])
      (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
        (HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
          ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
            (AdjoinRoot f.factor)[X])))
      (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor) ≠
    0
rw :
  Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
    (Subalgebra.restrictScalars K (S := AdjoinRoot f.factor)
      (Algebra.adjoin (AdjoinRoot f.factor)
        (↑(Multiset.toFinset
              (roots (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor))) :
          Set (SplittingFieldAux n f.removeFactor))))
    ⊤
rw₁ :
  Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
    (Subalgebra.restrictScalars K (S := AdjoinRoot f.factor)
      (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))))
    ⊤
rw₂ :
  Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
    (Subalgebra.restrictScalars K (S := AdjoinRoot f.factor) ⊤) ⊤
⊢ Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
    (Algebra.adjoin K
      ((fun (a : AdjoinRoot f.factor) ↦
            (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor) :
                (a : AdjoinRoot f.factor) → SplittingFieldAux n f.removeFactor)
              a) ''
          {AdjoinRoot.root f.factor} ∪
        (↑(Multiset.toFinset
              (roots (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor))) :
          Set (SplittingFieldAux n f.removeFactor))))
    ⊤
have rw₃ : Eq.{u + 1} (α := Subalgebra K (SplittingFieldAux n f.removeFactor)) ⊤ ⊤
Tactic: rw [← Algebra.adjoin_eq_adjoin_union K {AdjoinRoot.root f.factor}
      ((map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
        f.removeFactor).roots.toFinset : Set (SplittingFieldAux n f.removeFactor))
      AdjoinRoot.adjoinRoot_eq_top, ← rootSet_def, ih _ (natDegree_removeFactor' hfn),
      Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
n_1 : ℕ
K_1 : Type u
inst : Field K_1
n : ℕ
ih :
  (fun (n : ℕ) ↦
      ∀ {K : Type u} [inst : Field K] (f : K[X]) (_hfn : f.natDegree = n),
        Eq (α := Subalgebra K (SplittingFieldAux n f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n f))) ⊤)
    n
K : Type u
x : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : Ne (α := (SplittingFieldAux n.succ f)[X]) (map (algebraMap K (SplittingFieldAux n.succ f)) f) 0
⊢ Eq (α := Subalgebra K (SplittingFieldAux n.succ f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f))) ⊤
have rw : Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
  (Algebra.adjoin K (↑(Multiset.toFinset (f.aroots (SplittingFieldAux n.succ f))) : Set (SplittingFieldAux n.succ f))) ⊤
Tactic: classical
    rw [rootSet_def, aroots_def]
    rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢
    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, ← Set.image_singleton]
    simp only [SplittingFieldAux.succ]
    rw [← Algebra.adjoin_eq_adjoin_union K {AdjoinRoot.root f.factor}
      ((map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
        f.removeFactor).roots.toFinset : Set (SplittingFieldAux n f.removeFactor))
      AdjoinRoot.adjoinRoot_eq_top, ← rootSet_def, ih _ (natDegree_removeFactor' hfn),
      Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
n_1 : ℕ
K_1 : Type u
inst : Field K_1
n : ℕ
ih :
  (fun (n : ℕ) ↦
      ∀ {K : Type u} [inst : Field K] (f : K[X]) (_hfn : f.natDegree = n),
        Eq (α := Subalgebra K (SplittingFieldAux n f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n f))) ⊤)
    n
K : Type u
x : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : Ne (α := (SplittingFieldAux n.succ f)[X]) (map (algebraMap K (SplittingFieldAux n.succ f)) f) 0
rw :
  Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
    (Algebra.adjoin K (↑(Multiset.toFinset (f.aroots (SplittingFieldAux n.succ f))) : Set (SplittingFieldAux n.succ f)))
    ⊤
⊢ Eq (α := Subalgebra K (SplittingFieldAux n.succ f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f))) ⊤
have rw₁ : Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
  (Algebra.adjoin K
    (↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n.succ f)) f))) :
      Set (SplittingFieldAux n.succ f)))
  ⊤
Tactic: classical
    rw [rootSet_def, aroots_def]
    rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢
    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, ← Set.image_singleton]
    simp only [SplittingFieldAux.succ]
    rw [← Algebra.adjoin_eq_adjoin_union K {AdjoinRoot.root f.factor}
      ((map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
        f.removeFactor).roots.toFinset : Set (SplittingFieldAux n f.removeFactor))
      AdjoinRoot.adjoinRoot_eq_top, ← rootSet_def, ih _ (natDegree_removeFactor' hfn),
      Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
n_1 : ℕ
K_1 : Type u
inst : Field K_1
n : ℕ
ih :
  (fun (n : ℕ) ↦
      ∀ {K : Type u} [inst : Field K] (f : K[X]) (_hfn : f.natDegree = n),
        Eq (α := Subalgebra K (SplittingFieldAux n f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n f))) ⊤)
    n
K : Type u
x : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : Ne (α := (SplittingFieldAux n.succ f)[X]) (map (algebraMap K (SplittingFieldAux n.succ f)) f) 0
rw :
  Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
    (Algebra.adjoin K (↑(Multiset.toFinset (f.aroots (SplittingFieldAux n.succ f))) : Set (SplittingFieldAux n.succ f)))
    ⊤
rw₁ rw₂ rw₃ :
  Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
    (Algebra.adjoin K
      (↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n.succ f)) f))) :
        Set (SplittingFieldAux n.succ f)))
    ⊤
⊢ Eq (α := Subalgebra K (SplittingFieldAux n.succ f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f))) ⊤
have rw₄ : ∀
  (hmf0 :
    HMul.hMul (α := (SplittingFieldAux n.succ f)[X])
        (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
          (HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
            ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
              (AdjoinRoot f.factor)[X])))
        (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor) ≠
      0),
  Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
    (Algebra.adjoin K
      (↑(HMul.hMul (α := (SplittingFieldAux n.succ f)[X])
                (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                  (HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
                    ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
                      (AdjoinRoot f.factor)[X])))
                (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                  f.removeFactor)).roots.toFinset :
        Set (SplittingFieldAux n.succ f)))
    ⊤
Tactic: classical
    rw [rootSet_def, aroots_def]
    rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢
    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, ← Set.image_singleton]
    simp only [SplittingFieldAux.succ]
    rw [← Algebra.adjoin_eq_adjoin_union K {AdjoinRoot.root f.factor}
      ((map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
        f.removeFactor).roots.toFinset : Set (SplittingFieldAux n f.removeFactor))
      AdjoinRoot.adjoinRoot_eq_top, ← rootSet_def, ih _ (natDegree_removeFactor' hfn),
      Subalgebra.restrictScalars_top]
Cleared hypotheses: hmf0
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
q : ℚ≥0
⊢ (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q : K) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
have simp_rw : (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)) =
  HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
Tactic: simp_rw [NNRat.cast_def, map_div₀, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
q : ℚ≥0
simp_rw :
  (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
⊢ (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q : K) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
have simp_rw₁ : HDiv.hDiv (α := f.SplittingField) ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.num : K))
    ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.den : K)) =
  HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
Tactic: simp_rw [NNRat.cast_def, map_div₀, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
q : ℚ≥0
x : f.SplittingField
p : MvPolynomial (SplittingFieldAux f.natDegree f) K
⊢ Eq.{v + 1} (α := MvPolynomial (SplittingFieldAux f.natDegree f) K)
    ((fun (x : MvPolynomial (SplittingFieldAux f.natDegree f) K) ↦ q • x) p)
    ((fun (x1 x2 : MvPolynomial (SplittingFieldAux f.natDegree f) K) ↦ x1 * x2)
      ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K) :
          (a : K) → MvPolynomial (SplittingFieldAux f.natDegree f) K)
        (↑q : K))
      p)
have a : ∀ (m : SplittingFieldAux f.natDegree f →₀ ℕ),
  Eq (α := K) (MvPolynomial.coeff m ((fun (x : MvPolynomial (SplittingFieldAux f.natDegree f) K) ↦ q • x) p))
    (MvPolynomial.coeff m
      ((fun (x1 x2 : MvPolynomial (SplittingFieldAux f.natDegree f) K) ↦ x1 * x2)
        ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K) :
            (a : K) → MvPolynomial (SplittingFieldAux f.natDegree f) K)
          (↑q : K))
        p))
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
q : ℚ
⊢ (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q : K) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
have rw : (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)) =
  HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
Tactic: rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
q : ℚ
rw :
  (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
⊢ (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q : K) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
have rw₁ : HDiv.hDiv (α := f.SplittingField) ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.num : K))
    ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.den : K)) =
  HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
Tactic: rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
q : ℚ
rw :
  (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
rw₁ :
  HDiv.hDiv (α := f.SplittingField) ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.num : K))
      ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.den : K)) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
⊢ (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q : K) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
have rw₂ : HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField)
    ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.den : K)) =
  HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
Tactic: rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
q : ℚ
rw :
  (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
rw₁ :
  HDiv.hDiv (α := f.SplittingField) ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.num : K))
      ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.den : K)) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
rw₂ :
  HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField)
      ((algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q.den : K)) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
⊢ (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q : K) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
have rw₃ : HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField) =
  HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)
Tactic: rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
q : ℚ
x : f.SplittingField
p : MvPolynomial (SplittingFieldAux f.natDegree f) K
⊢ Eq.{v + 1} (α := MvPolynomial (SplittingFieldAux f.natDegree f) K)
    ((fun (x : MvPolynomial (SplittingFieldAux f.natDegree f) K) ↦ q • x) p)
    ((fun (x1 x2 : MvPolynomial (SplittingFieldAux f.natDegree f) K) ↦ x1 * x2)
      ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K) :
          (a : K) → MvPolynomial (SplittingFieldAux f.natDegree f) K)
        (↑q : K))
      p)
have a : ∀ (m : SplittingFieldAux f.natDegree f →₀ ℕ),
  Eq (α := K) (MvPolynomial.coeff m ((fun (x : MvPolynomial (SplittingFieldAux f.natDegree f) K) ↦ q • x) p))
    (MvPolynomial.coeff m
      ((fun (x1 x2 : MvPolynomial (SplittingFieldAux f.natDegree f) K) ↦ x1 * x2)
        ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K) :
            (a : K) → MvPolynomial (SplittingFieldAux f.natDegree f) K)
          (↑q : K))
        p))
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra F K
inst_5 : Algebra F L
inst_6 : IsScalarTower F K L
f : F[X]
inst_7 : IsSplittingField F L f
⊢ Splits (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f))
have rw : Splits (Polynomial.map (algebraMap F L) f)
Tactic: rw [map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra F K
inst_5 : Algebra F L
inst_6 : IsScalarTower F K L
f : F[X]
inst_7 : IsSplittingField F L f
⊢ Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (Algebra.adjoin K (rootSet (Polynomial.map (algebraMap F K) f) L)))
    (Subalgebra.restrictScalars.{u, v, w} F (S := K) ⊤)
have rw : f.rootSet L ⊆
  (↑(Subalgebra.restrictScalars F (Algebra.adjoin K (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))) :
    Set L)
Tactic: rw [rootSet, aroots, map_map, ← IsScalarTower.algebraMap_eq, Subalgebra.restrictScalars_top,
        eq_top_iff, ← adjoin_rootSet L f, Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
inst_3 : IsSplittingField K L f
h : f.Splits
⊢ Eq.{w + 1} (α := Subalgebra K L) ⊤ ⊥
have rw : (↑(Multiset.toFinset (Multiset.map (⇑(algebraMap K L) : (a : K) → L) f.roots)) : Set L) ⊆ (↑⊥ : Set L)
Tactic: rw [eq_bot_iff, ← adjoin_rootSet L f, rootSet, aroots, h.roots_map, Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (hypothesis)
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
inst_3 : IsSplittingField K L f
h : f.Splits
y : L
hy : y ∈ (↑(Multiset.toFinset (Multiset.map (⇑(algebraMap K L) : (a : K) → L) f.roots)) : Set L)
⊢ y ∈ (↑⊥ : Set L)
have hy₁ : ∃ a ∈ f.roots.toFinset, (algebraMap K L : (a : K) → L) a = y
Tactic: rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
inst_3 : IsSplittingField K L f
h : f.Splits
y : L
hy : ∃ a ∈ f.roots.toFinset, (algebraMap K L : (a : K) → L) a = y
⊢ y ∈ (↑⊥ : Set L)
have obtain : ∀ (x : K) (hxy : (algebraMap K L : (a : K) → L) x = y), y ∈ (↑⊥ : Set L)
Tactic: obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
inst_3 : IsSplittingField K L f
h : f.Splits
y : L
x : K
hxy : (algebraMap K L : (a : K) → L) x = y
⊢ y ∈ (↑⊥ : Set L)
have rw : Membership.mem (α := L) (↑⊥ : Set L) ((algebraMap K L : (a : K) → L) x : L)
Tactic: rw [← hxy]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
inst_3 : IsSplittingField K L f
h : f.Splits
y : L
hy : y ∈ (↑(Multiset.toFinset (Multiset.map (⇑(algebraMap K L) : (a : K) → L) f.roots)) : Set L)
⊢ y ∈ (↑⊥ : Set L)
have rw : ∀ (hy : y ∈ (↑(Finset.image (⇑(algebraMap K L) : (a : K) → L) f.roots.toFinset) : Set L)), y ∈ (↑⊥ : Set L)
Tactic: classical
    rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
    obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
    rw [← hxy]
    exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
inst_3 : IsSplittingField K L f
h : f.Splits
y : L
hy : y ∈ (↑(Multiset.toFinset (Multiset.map (⇑(algebraMap K L) : (a : K) → L) f.roots)) : Set L)
rw : ∀ (hy : y ∈ (↑(Finset.image (⇑(algebraMap K L) : (a : K) → L) f.roots.toFinset) : Set L)), y ∈ (↑⊥ : Set L)
⊢ y ∈ (↑⊥ : Set L)
have rw₁ : ∀ (hy : Membership.mem (γ := Finset L) (Finset.image (⇑(algebraMap K L) : (a : K) → L) f.roots.toFinset) y),
  y ∈ (↑⊥ : Set L)
Tactic: classical
    rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
    obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
    rw [← hxy]
    exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
inst_3 : IsSplittingField K L f
h : f.Splits
y : L
hy : y ∈ (↑(Multiset.toFinset (Multiset.map (⇑(algebraMap K L) : (a : K) → L) f.roots)) : Set L)
rw : ∀ (hy : y ∈ (↑(Finset.image (⇑(algebraMap K L) : (a : K) → L) f.roots.toFinset) : Set L)), y ∈ (↑⊥ : Set L)
rw₁ :
  ∀ (hy : Membership.mem (γ := Finset L) (Finset.image (⇑(algebraMap K L) : (a : K) → L) f.roots.toFinset) y),
    y ∈ (↑⊥ : Set L)
⊢ y ∈ (↑⊥ : Set L)
have rw₂ : ∀ (hy : ∃ a ∈ f.roots.toFinset, (algebraMap K L : (a : K) → L) a = y), y ∈ (↑⊥ : Set L)
Tactic: classical
    rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
    obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
    rw [← hxy]
    exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
inst_3 : IsSplittingField K L f
h : f.Splits
y : L
hy : y ∈ (↑(Multiset.toFinset (Multiset.map (⇑(algebraMap K L) : (a : K) → L) f.roots)) : Set L)
rw : ∀ (hy : y ∈ (↑(Finset.image (⇑(algebraMap K L) : (a : K) → L) f.roots.toFinset) : Set L)), y ∈ (↑⊥ : Set L)
rw₁ :
  ∀ (hy : Membership.mem (γ := Finset L) (Finset.image (⇑(algebraMap K L) : (a : K) → L) f.roots.toFinset) y),
    y ∈ (↑⊥ : Set L)
rw₂ rw₃ rw₄ : ∀ (hy : ∃ a ∈ f.roots.toFinset, (algebraMap K L : (a : K) → L) a = y), y ∈ (↑⊥ : Set L)
⊢ y ∈ (↑⊥ : Set L)
have rw₅ : ∀ (x : K) (hxy : (algebraMap K L : (a : K) → L) x = y), y ∈ (↑⊥ : Set L)
Tactic: classical
    rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
    obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
    rw [← hxy]
    exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _
Cleared hypotheses: hy