awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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
simp :
  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))))
    ⊤
⊢ Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
    (Algebra.adjoin K
      (Set.image (α := AdjoinRoot f.factor)
          (⇑(algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) :
            (a : AdjoinRoot f.factor) → SplittingFieldAux n.succ f)
          {AdjoinRoot.root f.factor} ∪
        (↑(Multiset.toFinset
              (roots (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor))) :
          Set (SplittingFieldAux n.succ f))))
    ⊤

Tactic:
simp only [SplittingFieldAux.succ]

Premises used: Polynomial.SplittingFieldAux.succ
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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) ⊤) ⊤
rw₃ rw₄ : Eq.{u + 1} (α := Subalgebra K (SplittingFieldAux n f.removeFactor)) ⊤ ⊤
⊢ 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))))
    ⊤

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]

Premises used: Multiset.toFinset, Polynomial.roots, AdjoinRoot, Algebra.algebraMap, Polynomial.factor, Polynomial.SplittingFieldAux, Polynomial.rootSet_def, Algebra.adjoin_eq_adjoin_union, SetLike.coe, Polynomial.natDegree_removeFactor', Polynomial.removeFactor, AdjoinRoot.root, Polynomial.map, AdjoinRoot.adjoinRoot_eq_top, Singleton.singleton, Subalgebra.restrictScalars_top
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
⊢ IsSplittingField K (SplittingFieldAux f.natDegree f) f

Tactic:
⟨SplittingFieldAux.splits _ _ rfl, SplittingFieldAux.adjoin_rootSet _ _ rfl⟩

Premises used: Polynomial.SplittingFieldAux.adjoin_rootSet, Polynomial.SplittingFieldAux.splits, Polynomial.IsSplittingField.mk, rfl
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f_1 f : K[X]
x : SplittingFieldAux f.natDegree f
⊢ (MvPolynomial.aeval id : (a : MvPolynomial (SplittingFieldAux f.natDegree f) K) → SplittingFieldAux f.natDegree f)
      (MvPolynomial.X x) =
    x

Tactic:
simp
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
e : f.SplittingField ≃ₐ[K] SplittingFieldAux f.natDegree f := algEquivSplittingFieldAux f
⊢ Eq (α := f.SplittingField)
    ((e.symm : (a : SplittingFieldAux f.natDegree f) → f.SplittingField)
      ((e : (a : f.SplittingField) → SplittingFieldAux f.natDegree f) 0)⁻¹)
    0

Tactic:
simp
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
e : f.SplittingField ≃ₐ[K] SplittingFieldAux f.natDegree f := algEquivSplittingFieldAux f
a : f.SplittingField
ha : a ≠ 0
⊢ Eq (α := SplittingFieldAux f.natDegree f)
    ((e : (a : f.SplittingField) → SplittingFieldAux f.natDegree f)
        (HMul.hMul (β := f.SplittingField) a
          ((e.symm : (a : SplittingFieldAux f.natDegree f) → f.SplittingField)
              ((e : (a : f.SplittingField) → SplittingFieldAux f.natDegree f) a)⁻¹ :
            f.SplittingField)) :
      SplittingFieldAux f.natDegree f)
    ((e : (a : f.SplittingField) → SplittingFieldAux f.natDegree f) 1 : SplittingFieldAux f.natDegree f)

Tactic:
simp [EmbeddingLike.map_ne_zero_iff.2 ha]

Premises used: Iff.mpr, EmbeddingLike.map_ne_zero_iff
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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)
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)
⊢ (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q : K) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)

Tactic:
simp_rw [NNRat.cast_def, map_div₀, map_natCast]

Premises used: NNRat.cast_def, map_div₀, map_natCast
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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
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))
⊢ 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)

Tactic:
ext
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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
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:
simp [MvPolynomial.algebraMap_eq, NNRat.smul_def]

Premises used: MvPolynomial.algebraMap_eq, NNRat.smul_def
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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)
rw₃ 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)
⊢ (algebraMap K f.SplittingField : (a : K) → f.SplittingField) (↑q : K) =
    HDiv.hDiv (α := f.SplittingField) (↑q.num : f.SplittingField) (↑q.den : f.SplittingField)

Tactic:
rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]

Premises used: map_intCast, Rat.cast_def, map_div₀, map_natCast
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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
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))
⊢ 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)

Tactic:
ext
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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
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:
simp [MvPolynomial.algebraMap_eq, Rat.smul_def]

Premises used: MvPolynomial.algebraMap_eq, Rat.smul_def
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
inst_3 : CharZero K
⊢ CharZero.{v} f.SplittingField

Tactic:
charZero_of_injective_algebraMap (algebraMap K _).injective

Premises used: Algebra.algebraMap, RingHom.injective, charZero_of_injective_algebraMap
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
p : ℕ
inst_3 : CharP K p
⊢ CharP.{v} f.SplittingField p

Tactic:
charP_of_injective_algebraMap (algebraMap K _).injective p

Premises used: Algebra.algebraMap, charP_of_injective_algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f : K[X]
p : ℕ
inst_3 : ExpChar K p
⊢ ExpChar.{v} f.SplittingField p

Tactic:
expChar_of_injective_algebraMap (algebraMap K _).injective p

Premises used: Algebra.algebraMap, RingHom.injective, expChar_of_injective_algebraMap
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
f_1 f : K[X]
⊢ IsSplittingField K f.SplittingField f

Tactic:
IsSplittingField.of_algEquiv _ f (algEquivSplittingFieldAux f).symm

Premises used: AlgEquiv.symm, Polynomial.SplittingField.algEquivSplittingFieldAux, Polynomial.IsSplittingField.of_algEquiv
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
⊢ Splits (R := f.SplittingField) (map (algebraMap K f.SplittingField) f)

Tactic:
IsSplittingField.splits f.SplittingField f

Premises used: Polynomial.SplittingField, Polynomial.IsSplittingField.splits
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
⊢ Eq (α := Subalgebra K f.SplittingField) (Algebra.adjoin K (f.rootSet f.SplittingField)) ⊤

Tactic:
Polynomial.IsSplittingField.adjoin_rootSet _ f

Premises used: Polynomial.IsSplittingField.adjoin_rootSet
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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
f : K[X]
⊢ FiniteDimensional K f.SplittingField

Tactic:
finiteDimensional f.SplittingField f

Premises used: Polynomial.SplittingField, Polynomial.IsSplittingField.finiteDimensional
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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 : Finite K
f : K[X]
⊢ Finite.{v + 1} f.SplittingField

Tactic:
Module.finite_of_finite K

Premises used: Module.finite_of_finite
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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
f : K[X]
⊢ Module.IsTorsionFree K f.SplittingField

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
⊢ Splits (map (algebraMap K L) f)

Tactic:
splits'

Premises used: Polynomial.IsSplittingField.splits'
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
⊢ Eq (α := Subalgebra K L) (Algebra.adjoin K (f.rootSet L)) ⊤

Tactic:
adjoin_rootSet'

Premises used: Polynomial.IsSplittingField.adjoin_rootSet'
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
rw : Splits (Polynomial.map (algebraMap F L) f)
⊢ Splits (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f))

Tactic:
rw [map_map, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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 F L) f)

Tactic:
splits L f

Premises used: Polynomial.IsSplittingField.splits
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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 F L) f)

Tactic:
exact splits L f

Premises used: Polynomial.IsSplittingField.splits
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
rw :
  f.rootSet L ⊆
    (↑(Subalgebra.restrictScalars F
          (Algebra.adjoin K (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))) :
      Set L)
⊢ 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) ⊤)

Tactic:
rw [rootSet, aroots, map_map, ← IsScalarTower.algebraMap_eq, Subalgebra.restrictScalars_top,
        eq_top_iff, ← adjoin_rootSet L f, Algebra.adjoin_le_iff]

Premises used: eq_top_iff, Polynomial.IsSplittingField.adjoin_rootSet, Polynomial.rootSet, Algebra.adjoin_le_iff, Polynomial.aroots, IsScalarTower.algebraMap_eq, Polynomial.map_map, Subalgebra.restrictScalars_top
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
⊢ f.rootSet L ⊆
    (↑(Subalgebra.restrictScalars F
          (Algebra.adjoin K (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))) :
      Set L)

Tactic:
fun x hx => @Algebra.subset_adjoin K _ _ _ _ _ _ hx

Premises used: Set.Mem, Algebra.subset_adjoin, Set.Subset
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
⊢ f.rootSet L ⊆
    (↑(Subalgebra.restrictScalars F
          (Algebra.adjoin K (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))) :
      Set L)

Tactic:
exact fun x hx => @Algebra.subset_adjoin K _ _ _ _ _ _ hx

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
rw : (↑(Multiset.toFinset (Multiset.map (⇑(algebraMap K L) : (a : K) → L) f.roots)) : Set L) ⊆ (↑⊥ : Set L)
⊢ Eq.{w + 1} (α := Subalgebra K L) ⊤ ⊥

Tactic:
rw [eq_bot_iff, ← adjoin_rootSet L f, rootSet, aroots, h.roots_map, Algebra.adjoin_le_iff]

Premises used: Polynomial.IsSplittingField.adjoin_rootSet, Polynomial.rootSet, Polynomial.Splits.roots_map, Algebra.adjoin_le_iff, Polynomial.aroots, eq_bot_iff
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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)
⊢ ∃ 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

Premises used: Finset.mem_image, Multiset.toFinset_map, Finset.mem_coe
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
obtain : ∀ (x : K) (hxy : (algebraMap K L : (a : K) → L) x = y), y ∈ (↑⊥ : Set L)
⊢ y ∈ (↑⊥ : Set L)

Tactic:
obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
rw : Membership.mem (α := L) (↑⊥ : Set L) ((algebraMap K L : (a : K) → L) x : L)
⊢ y ∈ (↑⊥ : Set L)

Tactic:
rw [← hxy]
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
⊢ Membership.mem (α := L) (↑⊥ : Set L) ((algebraMap K L : (a : K) → L) x : L)

Tactic:
SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _

Premises used: Iff.mpr, SetLike.mem_coe, Subalgebra.algebraMap_mem
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
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
⊢ Membership.mem (α := L) (↑⊥ : Set L) ((algebraMap K L : (a : K) → L) x : L)

Tactic:
exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _

Premises used: Iff.mpr, SetLike.mem_coe, Subalgebra.algebraMap_mem