-- Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
theorem splits_iff (f : K[X]) [IsSplittingField K L f] :
    Splits (RingHom.id K) f ↔ (⊤ : Subalgebra K L) = ⊥ :=
  ⟨fun h => by
    rw [eq_bot_iff, ← adjoin_rootSet L f, rootSet, aroots, roots_map (algebraMap K L) h,
      Algebra.adjoin_le_iff]
    intro y hy
    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 _ _,
    fun h => @RingEquiv.toRingHom_refl K _ ▸ RingEquiv.self_trans_symm
      (RingEquiv.ofBijective _ <| Algebra.bijective_algebraMap_iff.2 h) ▸ by
        rw [RingEquiv.toRingHom_trans]
        exact splits_comp_of_splits _ _ (splits L f)⟩

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset
⊢ y ∈ ↑⊥

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 _ _

Result:
no goals

Proof state:
case intro.intro
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
x : K
hxy : (algebraMap K L) x = y
⊢ y ∈ ↑⊥

Tactic:
rw [← hxy]

Result:
case intro.intro
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
x : K
hxy : (algebraMap K L) x = y
⊢ (algebraMap K L) x ∈ ↑⊥

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits ((RingEquiv.ofBijective (algebraMap K L) ⋯).trans (RingEquiv.ofBijective (algebraMap K L) ⋯).symm).toRingHom f

Tactic:
rw [RingEquiv.toRingHom_trans]

Result:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits
    ((RingEquiv.ofBijective (algebraMap K L) ⋯).symm.toRingHom.comp
      (RingEquiv.ofBijective (algebraMap K L) ⋯).toRingHom)
    f

Proof state:
case intro.intro
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
x : K
hxy : (algebraMap K L) x = y
⊢ (algebraMap K L) x ∈ ↑⊥

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

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : ∃ a ∈ f.roots.toFinset, (algebraMap K L) a = y
⊢ y ∈ ↑⊥

Tactic:
obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy

Result:
case intro.intro
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
x : K
hxy : (algebraMap K L) x = y
⊢ y ∈ ↑⊥

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits
    ((RingEquiv.ofBijective (algebraMap K L) ⋯).symm.toRingHom.comp
      (RingEquiv.ofBijective (algebraMap K L) ⋯).toRingHom)
    f

Tactic:
exact splits_comp_of_splits _ _ (splits L f)

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset ⊆ ↑⊥

Tactic:
intro y hy

Result:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset
⊢ y ∈ ↑⊥

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ⊤ = ⊥

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

Result:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset ⊆ ↑⊥

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset
⊢ y ∈ ↑⊥

Tactic:
rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy

Result:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : ∃ a ∈ f.roots.toFinset, (algebraMap K L) a = y
⊢ y ∈ ↑⊥