awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
rw₅ : ∀ (x : K) (hxy : (algebraMap K L : (a : K) → L) x = y), y ∈ (↑⊥ : Set L)
rw₆ :
  ∀ (x : K) (hxy : (algebraMap K L : (a : K) → L) x = y),
    Membership.mem (α := L) (↑⊥ : Set L) ((algebraMap K L : (a : K) → L) x : 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 _ _

Premises used: Iff.mpr, Finset.mem_image, SetLike.mem_coe, Subalgebra.algebraMap_mem, 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 : Eq.{w + 1} (α := Subalgebra K L) ⊤ ⊥
rw :
  Splits
    (Polynomial.map (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) ⋯)))
      (Polynomial.map (RingEquiv.toRingHom (RingEquiv.ofBijective (algebraMap K L) ⋯)) f))
⊢ f.Splits

Tactic:
rw [← Polynomial.map_id (p := f), ← RingEquiv.toRingHom_refl, ← RingEquiv.self_trans_symm
      (RingEquiv.ofBijective _ <| Algebra.bijective_algebraMap_iff.2 h),
      RingEquiv.toRingHom_trans, ← map_map]

Premises used: Iff.mpr, RingEquiv.ofBijective, Algebra.bijective_algebraMap_iff, RingEquiv.toRingHom_trans, Polynomial.map_id, RingEquiv.toRingHom_refl, Polynomial.map_map, RingEquiv.self_trans_symm
-- 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 : Eq.{w + 1} (α := Subalgebra K L) ⊤ ⊥
⊢ Splits
    (Polynomial.map (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) ⋯)))
      (Polynomial.map (RingEquiv.toRingHom (RingEquiv.ofBijective (algebraMap K L) ⋯)) f))

Tactic:
apply (splits L f).map

Premises used: Polynomial.IsSplittingField.splits, Polynomial.Splits.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 K L (((mapAlg F K : AlgHom.{u, u, v} F F[X] K[X]) : (a : F[X]) → K[X]) f)
rw : Splits (Polynomial.map (algebraMap K L) (((mapAlg F K : AlgHom.{u, u, v} F F[X] K[X]) : (a : F[X]) → K[X]) f))
⊢ Splits.{w} (R := L) (((mapAlg F L : AlgHom.{u, u, w} F F[X] L[X]) : (a : F[X]) → L[X]) f)

Tactic:
rw [mapAlg_comp K L f, mapAlg_eq_map]

Premises used: Polynomial.mapAlg_eq_map, Polynomial.mapAlg_comp
-- 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 K L (((mapAlg F K : AlgHom.{u, u, v} F F[X] K[X]) : (a : F[X]) → K[X]) f)
⊢ Splits (Polynomial.map (algebraMap K L) (((mapAlg F K : AlgHom.{u, u, v} F F[X] K[X]) : (a : F[X]) → K[X]) f))

Tactic:
apply IsSplittingField.splits

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 g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst_7 : IsSplittingField F K f
inst_8 : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
splits' : Splits (Polynomial.map (algebraMap F L) (f * g))
adjoin_rootSet' : Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
⊢ IsSplittingField F L (f * g)

Tactic:
constructor
-- 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 g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst_7 : IsSplittingField F K f
inst_8 : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
splits' :
  (HMul.hMul (α := L[X]) (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f))
      (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) g))).Splits
⊢ Splits (Polynomial.map (algebraMap F L) (f * g))

Tactic:
rw [Polynomial.map_mul, IsScalarTower.algebraMap_eq F K L, ← map_map, ← map_map]

Premises used: Polynomial.map_mul, 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 g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst_7 : IsSplittingField F K f
inst_8 : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ (HMul.hMul (α := L[X]) (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f))
      (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) g))).Splits

Tactic:
Splits.mul ((splits K f).map _) (splits L (g.map (algebraMap F K)))

Premises used: Algebra.algebraMap, Polynomial.IsSplittingField.splits, Polynomial.map, Polynomial.Splits.map, Polynomial.Splits.mul
-- 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 g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst_7 : IsSplittingField F K f
inst_8 : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ (HMul.hMul (α := L[X]) (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f))
      (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) g))).Splits

Tactic:
exact Splits.mul ((splits K f).map _) (splits L (g.map (algebraMap F K)))

Premises used: Algebra.algebraMap, Polynomial.IsSplittingField.splits, Polynomial.map, Polynomial.Splits.map, Polynomial.Splits.mul
-- 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 K F
f : K[X]
inst_5 : IsSplittingField K L f
hf : Splits (Polynomial.map (algebraMap K F) f)
hf0 : f = 0
⊢ f.Splits

Tactic:
simp [hf0]
-- 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 K F
f : K[X]
inst_5 : IsSplittingField K L f
hf : Splits (Polynomial.map (algebraMap K F) f)
hf0 : f = 0
rw : L →ₐ[K] ↥⊤
⊢ L →ₐ[K] ↥⊥

Tactic:
rw [← (splits_iff L f).1 (show f.Splits by simp [hf0])]

Premises used: Polynomial.IsSplittingField.splits_iff, Iff.mp
-- 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 K F
f : K[X]
inst_5 : IsSplittingField K L f
hf : Splits (Polynomial.map (algebraMap K F) f)
hf0 : f = 0
⊢ L →ₐ[K] ↥⊤

Tactic:
exact Algebra.toTop

Premises used: Algebra.toTop
-- 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 K F
f : K[X]
inst_5 : IsSplittingField K L f
hf : Splits (Polynomial.map (algebraMap K F) f)
hf0 : ¬f = 0
rw : AlgHom.{v, w, u} K (↥(Algebra.adjoin K (f.rootSet L))) F
⊢ AlgHom.{v, w, u} K (↥⊤) F

Tactic:
rw [← adjoin_rootSet L f]

Premises used: Polynomial.IsSplittingField.adjoin_rootSet
-- 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
y : L
hy : y ∈ f.rootSet L
hf : f = 0
⊢ Membership.mem (γ := Set L) ∅ y

Tactic:
rw [hf, rootSet_zero] at hy

Premises used: Polynomial.rootSet_zero
-- 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
y : L
hy : y ∈ f.rootSet L
hf : f = 0
hy₁ : Membership.mem (γ := Set L) ∅ y
⊢ f = 0

Tactic:
rw [hf, rootSet_zero] at hy

Premises used: Polynomial.rootSet_zero
-- 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
y : L
hy : Membership.mem (γ := Set L) ∅ y
hf : f = 0
⊢ IsIntegral K y

Tactic:
cases 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
⊢ FiniteDimensional K L

Tactic:
exact ⟨@Algebra.top_toSubmodule K L _ _ _ ▸
    adjoin_rootSet L f ▸ fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
      if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy
      else IsAlgebraic.isIntegral ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩
-- 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
⊢ FiniteDimensional K L

Tactic:
classical
  exact ⟨@Algebra.top_toSubmodule K L _ _ _ ▸
    adjoin_rootSet L f ▸ fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
      if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy
      else IsAlgebraic.isIntegral ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩
-- 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 : Algebra.IsAlgebraic F K
inst_7 : IsScalarTower F K L
f : K[X]
inst_8 : IsSplittingField K L f
⊢ FiniteDimensional K L

Tactic:
have : FiniteDimensional K L := IsSplittingField.finiteDimensional L f
-- 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 : Algebra.IsAlgebraic F K
inst_7 : IsScalarTower F K L
f : K[X]
inst_8 : IsSplittingField K L f
this : FiniteDimensional K L
⊢ Algebra.IsAlgebraic F L

Tactic:
Algebra.IsAlgebraic.trans F K L

Premises used: Algebra.IsAlgebraic.trans
-- 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 : Algebra.IsAlgebraic F K
inst_7 : IsScalarTower F K L
f : K[X]
inst_8 : IsSplittingField K L f
this : FiniteDimensional K L
⊢ Algebra.IsAlgebraic F L

Tactic:
exact Algebra.IsAlgebraic.trans F K L

Premises used: Algebra.IsAlgebraic.trans
-- 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 K F
p : K[X]
f : F ≃ₐ[K] L
inst_5 : IsSplittingField K F p
splits' : Splits (Polynomial.map (algebraMap K L) p)
adjoin_rootSet' : Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) ⊤
⊢ IsSplittingField K L p

Tactic:
constructor
-- 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 K F
p : K[X]
f : F ≃ₐ[K] L
inst_5 : IsSplittingField K F p
splits' : Splits (Polynomial.map (↑(↑f : F →ₐ[K] L) : F →+* L) (Polynomial.map (algebraMap K F) p))
⊢ Splits (Polynomial.map (algebraMap K L) p)

Tactic:
rw [← f.toAlgHom.comp_algebraMap, ← map_map]

Premises used: AlgHom.comp_algebraMap, AlgEquiv.toAlgHom, 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 K F
p : K[X]
f : F ≃ₐ[K] L
inst_5 : IsSplittingField K F p
⊢ Splits (Polynomial.map (↑(↑f : F →ₐ[K] L) : F →+* L) (Polynomial.map (algebraMap K F) p))

Tactic:
(splits F p).map _

Premises used: Polynomial.IsSplittingField.splits, Polynomial.Splits.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 K F
p : K[X]
f : F ≃ₐ[K] L
inst_5 : IsSplittingField K F p
⊢ Splits (Polynomial.map (↑(↑f : F →ₐ[K] L) : F →+* L) (Polynomial.map (algebraMap K F) p))

Tactic:
exact (splits F p).map _

Premises used: Polynomial.IsSplittingField.splits, Polynomial.Splits.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 K F
p : K[X]
f : F ≃ₐ[K] L
inst_5 : IsSplittingField K F p
adjoin_rootSet' : Algebra.adjoin K (p.rootSet L) = (↑f : F →ₐ[K] L).range
adjoin_rootSet'₁ : Eq (α := Subalgebra K F) (Algebra.adjoin K (p.rootSet F)) ⊤
adjoin_rootSet'₂ adjoin_rootSet'₃ : Eq.{u + 1} (α := Subalgebra K F) ⊤ ⊤
⊢ Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) ⊤

Tactic:
rw [← (AlgHom.range_eq_top f.toAlgHom).mpr f.surjective,
      (splits F p).adjoin_rootSet_eq_range, adjoin_rootSet F p]

Premises used: Iff.mpr, AlgEquiv.toAlgHom, Polynomial.IsSplittingField.adjoin_rootSet, Polynomial.Splits.adjoin_rootSet_eq_range, Polynomial.IsSplittingField.splits, AlgHom.range_eq_top, AlgEquiv.surjective
-- 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 K F
f : K[X]
inst_5 : IsSplittingField K L f
i : L →ₐ[K] F
⊢ Algebra.adjoin K (f.rootSet F) = i.range

Tactic:
((splits L f).adjoin_rootSet_eq_range i).mpr (adjoin_rootSet L f)

Premises used: Iff.mpr, Polynomial.IsSplittingField.adjoin_rootSet, Polynomial.Splits.adjoin_rootSet_eq_range, 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
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
hF : ∀ x ∈ p.rootSet L, x ∈ F
⊢ ∀ (hf : Splits (Polynomial.map (R := ↥F) (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)))
    (hi :
      ∀ a ∈ roots (Polynomial.map (R := ↥F) (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)),
        Membership.mem (γ := Subring L) (RingHom.range (R := ↥F) (algebraMap (↥F) L)) a),
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)

Tactic:
have := Splits.of_splits_map (f := p.map (algebraMap K F)) (algebraMap F L)
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
hF : ∀ x ∈ p.rootSet L, x ∈ F
this :
  ∀ (hf : Splits (Polynomial.map (R := ↥F) (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)))
    (hi :
      ∀ a ∈ roots (Polynomial.map (R := ↥F) (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)),
        Membership.mem (γ := Subring L) (RingHom.range (R := ↥F) (algebraMap (↥F) L)) a),
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
⊢ ∀ (hf : Splits (Polynomial.map (algebraMap K L) p))
    (hi :
      ∀ a ∈ roots (Polynomial.map (algebraMap K L) p),
        Membership.mem (γ := Subring L) (RingHom.range (R := ↥F) (algebraMap (↥F) L)) a),
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)

Tactic:
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq] at this

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
hF : ∀ x ∈ p.rootSet L, x ∈ F
this :
  ∀ (hf : Splits (Polynomial.map (algebraMap K L) p))
    (hi :
      ∀ a ∈ roots (Polynomial.map (algebraMap K L) p),
        Membership.mem (γ := Subring L) (RingHom.range (R := ↥F) (algebraMap (↥F) L)) a),
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
⊢ ∀ a ∈ roots (Polynomial.map (algebraMap K L) p),
    Membership.mem (γ := Subring L) (RingHom.range (R := ↥F) (algebraMap (↥F) L)) a

Tactic:
simpa [rootSet_def] using hF

Premises used: Polynomial.rootSet_def
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
hF : ∀ x ∈ p.rootSet L, x ∈ F
this :
  ∀ (hf : Splits (Polynomial.map (algebraMap K L) p))
    (hi :
      ∀ a ∈ roots (Polynomial.map (algebraMap K L) p),
        Membership.mem (γ := Subring L) (RingHom.range (R := ↥F) (algebraMap (↥F) L)) a),
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)

Tactic:
exact this h (by simpa [rootSet_def] using hF)
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
hF : ∀ x ∈ p.rootSet L, x ∈ F
have have₁ have₂ :
  ∀
    (this :
      ∀ (hf : Splits (Polynomial.map (R := ↥F) (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)))
        (hi :
          ∀ a ∈ roots (Polynomial.map (R := ↥F) (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)),
            Membership.mem (γ := Subring L) (RingHom.range (R := ↥F) (algebraMap (↥F) L)) a),
        Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)),
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
have₃ :
  ∀
    (this :
      ∀ (hf : Splits (Polynomial.map (algebraMap K L) p))
        (hi :
          ∀ a ∈ roots (Polynomial.map (algebraMap K L) p),
            Membership.mem (γ := Subring L) (RingHom.range (R := ↥F) (algebraMap (↥F) L)) a),
        Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)),
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)

Tactic:
classical
  have := Splits.of_splits_map (f := p.map (algebraMap K F)) (algebraMap F L)
  rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq] at this
  exact this h (by simpa [rootSet_def] using hF)

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) ↔ ∀ x ∈ p.rootSet L, x ∈ F

Tactic:
⟨?_, IntermediateField.splits_of_splits h⟩

Premises used: Iff.intro, IntermediateField.splits_of_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
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
refine : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) → ∀ x ∈ p.rootSet L, x ∈ F
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) ↔ ∀ x ∈ p.rootSet L, x ∈ F

Tactic:
refine ⟨?_, IntermediateField.splits_of_splits h⟩
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
hF : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
rw :
  ∀ ⦃x : ↥F⦄, Membership.mem (γ := Set ↥F) (p.rootSet ↥F) x → Membership.mem (α := L) F ((F.val : (a : ↥F) → L) x : L)
⊢ ∀ x ∈ p.rootSet L, x ∈ F

Tactic:
rw [← hF.image_rootSet F.val, Set.forall_mem_image]

Premises used: Polynomial.Splits.image_rootSet, IntermediateField.val, Set.forall_mem_image
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
hF : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
⊢ ∀ ⦃x : ↥F⦄, Membership.mem (γ := Set ↥F) (p.rootSet ↥F) x → Membership.mem (α := L) F ((F.val : (a : ↥F) → L) x : L)

Tactic:
fun x _ ↦ x.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (Polynomial.map (algebraMap K L) p)
hF : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
⊢ ∀ ⦃x : ↥F⦄, Membership.mem (γ := Set ↥F) (p.rootSet ↥F) x → Membership.mem (α := L) F ((F.val : (a : ↥F) → L) x : L)

Tactic:
exact fun x _ ↦ x.2
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
int : IsIntegral K x
F : IntermediateField K L
h : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) (minpoly K x))
rw : x ∈ F.val.fieldRange
⊢ x ∈ F

Tactic:
rw [← F.fieldRange_val]

Premises used: IntermediateField.fieldRange_val
-- Module: Mathlib.FieldTheory.SplittingField.IsSplittingField
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
int : IsIntegral K x
F : IntermediateField K L
h : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) (minpoly K x))
⊢ x ∈ F.val.fieldRange

Tactic:
int.mem_range_algebraMap_of_minpoly_splits h

Premises used: Set.Mem, IsIntegral.mem_range_algebraMap_of_minpoly_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
x : L
int : IsIntegral K x
F : IntermediateField K L
h : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) (minpoly K x))
⊢ x ∈ F.val.fieldRange

Tactic:
exact int.mem_range_algebraMap_of_minpoly_splits h

Premises used: IsIntegral.mem_range_algebraMap_of_minpoly_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
p : K[X]
rw :
  IsSplittingField K L p ↔
    Splits (map (algebraMap K L) p) ∧
      Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) (IntermediateField.toSubalgebra ⊤)
⊢ IsSplittingField K L p ↔
    Splits (map (algebraMap K L) p) ∧ Eq (α := IntermediateField K L) (IntermediateField.adjoin K (p.rootSet L)) ⊤

Tactic:
rw [← IntermediateField.toSubalgebra_injective.eq_iff,
      IntermediateField.adjoin_toSubalgebra_of_isAlgebraic fun _ ↦ isAlgebraic_of_mem_rootSet]

Premises used: Function.Injective.eq_iff, IntermediateField.toSubalgebra_injective, isAlgebraic_of_mem_rootSet, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic