awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
E : Type u_6
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K₁ E
inst_6 : IsScalarTower F K₁ E
inst_7 : Normal F K₁
h1 : IsSolvable.{u_3} Gal(K₁/F)
h2 : IsSolvable.{u_6} Gal(E/K₁)
f : Gal(E/K₁) →* Gal(E/F) :=
  {
    toFun := fun (ϕ : Gal(E/K₁)) ↦
      AlgEquiv.ofAlgHom (AlgHom.restrictScalars F (↑ϕ : E →ₐ[K₁] E)) (AlgHom.restrictScalars F (↑ϕ.symm : E →ₐ[K₁] E)) ⋯
        ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
⊢ IsSolvable.{u_6} Gal(E/F)

Tactic:
solvable_of_ker_le_range f (AlgEquiv.restrictNormalHom K₁) fun ϕ hϕ =>
      ⟨{ ϕ with commutes' := fun x => ?_ }, AlgEquiv.ext fun _ => rfl⟩

Premises used: solvable_of_ker_le_range, AlgEquiv.mk, AlgEquiv.map_add', AlgEquiv.restrictNormalHom, AlgEquiv.ext, Exists.intro, AlgEquiv.map_mul', AlgEquiv.toEquiv, rfl
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
E : Type u_6
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K₁ E
inst_6 : IsScalarTower F K₁ E
inst_7 : Normal F K₁
h1 : IsSolvable.{u_3} Gal(K₁/F)
h2 : IsSolvable.{u_6} Gal(E/K₁)
f : Gal(E/K₁) →* Gal(E/F) :=
  {
    toFun := fun (ϕ : Gal(E/K₁)) ↦
      AlgEquiv.ofAlgHom (AlgHom.restrictScalars F (↑ϕ : E →ₐ[K₁] E)) (AlgHom.restrictScalars F (↑ϕ.symm : E →ₐ[K₁] E)) ⋯
        ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
solvable_of_ker_le_range :
  ∀ (ϕ : Gal(E/F))
    (hϕ : Membership.mem (γ := Subgroup Gal(E/F)) (MonoidHom.ker (M := Gal(K₁/F)) (AlgEquiv.restrictNormalHom K₁)) ϕ)
    (x : K₁), ϕ.toFun ((algebraMap K₁ E : (a : K₁) → E) x) = (algebraMap K₁ E : (a : K₁) → E) x
⊢ IsSolvable.{u_6} Gal(E/F)

Tactic:
refine
    solvable_of_ker_le_range f (AlgEquiv.restrictNormalHom K₁) fun ϕ hϕ =>
      ⟨{ ϕ with commutes' := fun x => ?_ }, AlgEquiv.ext fun _ => rfl⟩

Premises used: solvable_of_ker_le_range, AlgEquiv.mk, AlgEquiv.map_add', AlgEquiv.restrictNormalHom, AlgEquiv.ext, Exists.intro, AlgEquiv.map_mul', AlgEquiv.toEquiv, rfl
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
E : Type u_6
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K₁ E
inst_6 : IsScalarTower F K₁ E
inst_7 : Normal F K₁
h1 : IsSolvable.{u_3} Gal(K₁/F)
h2 : IsSolvable.{u_6} Gal(E/K₁)
f : Gal(E/K₁) →* Gal(E/F) :=
  {
    toFun := fun (ϕ : Gal(E/K₁)) ↦
      AlgEquiv.ofAlgHom (AlgHom.restrictScalars F (↑ϕ : E →ₐ[K₁] E)) (AlgHom.restrictScalars F (↑ϕ.symm : E →ₐ[K₁] E)) ⋯
        ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
ϕ : Gal(E/F)
hϕ : Membership.mem (γ := Subgroup Gal(E/F)) (MonoidHom.ker (M := Gal(K₁/F)) (AlgEquiv.restrictNormalHom K₁)) ϕ
x : K₁
⊢ ϕ.toFun ((algebraMap K₁ E : (a : K₁) → E) x) = (algebraMap K₁ E : (a : K₁) → E) x

Tactic:
Eq.trans (ϕ.restrictNormal_commutes K₁ x).symm (congr_arg _ (AlgEquiv.ext_iff.mp hϕ x))

Premises used: AlgEquiv.ext_iff, congr_arg, AlgEquiv.restrictNormal_commutes, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
E : Type u_6
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K₁ E
inst_6 : IsScalarTower F K₁ E
inst_7 : Normal F K₁
h1 : IsSolvable.{u_3} Gal(K₁/F)
h2 : IsSolvable.{u_6} Gal(E/K₁)
f : Gal(E/K₁) →* Gal(E/F) :=
  {
    toFun := fun (ϕ : Gal(E/K₁)) ↦
      AlgEquiv.ofAlgHom (AlgHom.restrictScalars F (↑ϕ : E →ₐ[K₁] E)) (AlgHom.restrictScalars F (↑ϕ.symm : E →ₐ[K₁] E)) ⋯
        ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
ϕ : Gal(E/F)
hϕ : Membership.mem (γ := Subgroup Gal(E/F)) (MonoidHom.ker (M := Gal(K₁/F)) (AlgEquiv.restrictNormalHom K₁)) ϕ
x : K₁
⊢ ϕ.toFun ((algebraMap K₁ E : (a : K₁) → E) x) = (algebraMap K₁ E : (a : K₁) → E) x

Tactic:
exact Eq.trans (ϕ.restrictNormal_commutes K₁ x).symm (congr_arg _ (AlgEquiv.ext_iff.mp hϕ x))

Premises used: AlgEquiv.ext_iff, congr_arg, AlgEquiv.restrictNormal_commutes, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
⊢ IsAlgebraic K x

Tactic:
have hx : IsAlgebraic K x := ⟨minpoly K y, ne_zero hy.isIntegral, h_ev⟩
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
rw : (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) ((f : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯) = y
rw₁ : (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (AdjoinSimple.gen K y) = y
rw₂ rw₃ : y = y
⊢ (f.liftNormal L : (a : L) → L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L) = y

Tactic:
rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]

Premises used: minpoly.algEquiv_apply, AlgEquiv.liftNormal_commutes, IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
⊢ (f.liftNormal L : (a : L) → L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L) = y

Tactic:
have hxy : (liftNormal f L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y := by
    rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
hxy : (f.liftNormal L : (a : L) → L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L) = y
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) x = y

Tactic:
⟨(liftNormal f L), hxy⟩

Premises used: AlgEquiv.liftNormal, Exists.intro
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
hxy : (f.liftNormal L : (a : L) → L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L) = y
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) x = y

Tactic:
exact ⟨(liftNormal f L), hxy⟩
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
obtain : ∀ (σ : Gal(L/K)) (hσ : (σ : (a : L) → L) x = y), ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x

Tactic:
obtain ⟨σ, hσ⟩ := exists_algEquiv_of_root hy h_ev

Premises used: minpoly.exists_algEquiv_of_root
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
σ : Gal(L/K)
hσ : (σ : (a : L) → L) x = y
h : (σ.symm : (a : L) → L) y = x
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) y = x

Tactic:
use σ.symm

Premises used: AlgEquiv.symm
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
K : Type u_6
L : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : Eq.{u_7 + 1} (α := L) ((Polynomial.aeval x : (a : K[X]) → L) (minpoly K y) : L) (0 : L)
σ : Gal(L/K)
hσ : (σ : (a : L) → L) x = y
h : (σ.symm : (a : L) → L) ((σ : (a : L) → L) x : L) = x
h₁ h₂ : x = x
⊢ (σ.symm : (a : L) → L) y = x

Tactic:
rw [← hσ, symm_apply_apply]

Premises used: AlgEquiv.symm_apply_apply
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F_1 : Type u_1
K_1 : Type u_2
inst : Field F_1
inst_1 : Field K_1
inst_2 : Algebra F_1 K_1
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F_1 K₁
inst_7 : Algebra F_1 K₂
inst_8 : Algebra F_1 K₃
ϕ : K₁ →ₐ[F_1] K₂
χ : K₁ ≃ₐ[F_1] K₂
ψ : K₂ →ₐ[F_1] K₃
ω : K₂ ≃ₐ[F_1] K₃
F : Type u_6
K : Type u_7
inst_9 : Field F
inst_10 : Field K
inst_11 : Algebra F K
inst_12 : IsQuadraticExtension F K
x : K
inl : ∀ (h : natDegree (minpoly F x) < 2), Splits (map (algebraMap F K) (minpoly F x))
inr : ∀ (h : natDegree (minpoly F x) = 2), Splits (map (algebraMap F K) (minpoly F x))
⊢ Splits (map (algebraMap F K) (minpoly F x))

Tactic:
obtain h | h := le_iff_lt_or_eq.mp (finrank_eq_two F K ▸ minpoly.natDegree_le x)

Premises used: le_iff_lt_or_eq, Iff.mp
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F_1 : Type u_1
K_1 : Type u_2
inst : Field F_1
inst_1 : Field K_1
inst_2 : Algebra F_1 K_1
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F_1 K₁
inst_7 : Algebra F_1 K₂
inst_8 : Algebra F_1 K₃
ϕ : K₁ →ₐ[F_1] K₂
χ : K₁ ≃ₐ[F_1] K₂
ψ : K₂ →ₐ[F_1] K₃
ω : K₂ ≃ₐ[F_1] K₃
F : Type u_6
K : Type u_7
inst_9 : Field F
inst_10 : Field K
inst_11 : Algebra F K
inst_12 : IsQuadraticExtension F K
x : K
h : natDegree (minpoly F x) < 2
rwa rwa₁ rwa₂ rwa₃ : natDegree (minpoly F x) < HAdd.hAdd (α := ℕ) 1 1
⊢ natDegree (minpoly F x) ≤ 1

Tactic:
rwa [Nat.le_iff_lt_add_one]

Premises used: Nat.le_iff_lt_add_one
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F_1 : Type u_1
K_1 : Type u_2
inst : Field F_1
inst_1 : Field K_1
inst_2 : Algebra F_1 K_1
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F_1 K₁
inst_7 : Algebra F_1 K₂
inst_8 : Algebra F_1 K₃
ϕ : K₁ →ₐ[F_1] K₂
χ : K₁ ≃ₐ[F_1] K₂
ψ : K₂ →ₐ[F_1] K₃
ω : K₂ ≃ₐ[F_1] K₃
F : Type u_6
K : Type u_7
inst_9 : Field F
inst_10 : Field K
inst_11 : Algebra F K
inst_12 : IsQuadraticExtension F K
x : K
h : natDegree (minpoly F x) < 2
⊢ Splits (map (algebraMap F K) (minpoly F x))

Tactic:
exact Splits.of_natDegree_le_one <| natDegree_map_le.trans (by rwa [Nat.le_iff_lt_add_one])

Premises used: Polynomial.Splits.of_natDegree_le_one, Polynomial.natDegree_map_le, LE.le.trans
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F_1 : Type u_1
K_1 : Type u_2
inst : Field F_1
inst_1 : Field K_1
inst_2 : Algebra F_1 K_1
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F_1 K₁
inst_7 : Algebra F_1 K₂
inst_8 : Algebra F_1 K₃
ϕ : K₁ →ₐ[F_1] K₂
χ : K₁ ≃ₐ[F_1] K₂
ψ : K₂ →ₐ[F_1] K₃
ω : K₂ ≃ₐ[F_1] K₃
F : Type u_6
K : Type u_7
inst_9 : Field F
inst_10 : Field K
inst_11 : Algebra F K
inst_12 : IsQuadraticExtension F K
x : K
h : natDegree (minpoly F x) = 2
⊢ Splits (map (algebraMap F K) (minpoly F x))

Tactic:
Splits.of_natDegree_eq_two ((natDegree_map _).trans h)
        ((eval_map_algebraMap _ _).trans (minpoly.aeval F x))

Premises used: Polynomial.natDegree_map, minpoly.aeval, Polynomial.eval_map_algebraMap, Polynomial.Splits.of_natDegree_eq_two, Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F_1 : Type u_1
K_1 : Type u_2
inst : Field F_1
inst_1 : Field K_1
inst_2 : Algebra F_1 K_1
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F_1 K₁
inst_7 : Algebra F_1 K₂
inst_8 : Algebra F_1 K₃
ϕ : K₁ →ₐ[F_1] K₂
χ : K₁ ≃ₐ[F_1] K₂
ψ : K₂ →ₐ[F_1] K₃
ω : K₂ ≃ₐ[F_1] K₃
F : Type u_6
K : Type u_7
inst_9 : Field F
inst_10 : Field K
inst_11 : Algebra F K
inst_12 : IsQuadraticExtension F K
x : K
h : natDegree (minpoly F x) = 2
⊢ Splits (map (algebraMap F K) (minpoly F x))

Tactic:
exact Splits.of_natDegree_eq_two ((natDegree_map _).trans h)
        ((eval_map_algebraMap _ _).trans (minpoly.aeval F x))

Premises used: Polynomial.natDegree_map, minpoly.aeval, Polynomial.eval_map_algebraMap, Polynomial.Splits.of_natDegree_eq_two, Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
⊢ Eq (α := IntermediateField F L) (normalClosure F K L) (⨆ (f : K →ₐ[F] L), f.fieldRange)

Tactic:
rfl

Premises used: IntermediateField.normalClosure, rfl
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
h : IsNormalClosure F K L
⊢ Normal F L

Tactic:
Normal.of_algEquiv topEquiv (h := h.adjoin_rootSet ▸ IntermediateField.normal_iSup (h :=
    fun _ ↦ Normal.of_isSplittingField (hFEp := adjoin_rootSet_isSplittingField <| h.splits _)))

Premises used: Normal.of_algEquiv, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
K' : IntermediateField F L
⊢ normalClosure F K L ≤ K' ↔ ∀ (f : K →ₐ[F] L), f.fieldRange ≤ K'

Tactic:
iSup_le_iff

Premises used: Set.Mem, iSup_le_iff
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
f : K →ₐ[F] L
⊢ f.fieldRange ≤ normalClosure F K L

Tactic:
le_iSup AlgHom.fieldRange f

Premises used: Set.Mem, setOf, le_iSup, AlgHom.fieldRange
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x_1 : L
h : x_1 ∈ f.fieldRange
x : K
hx : (f.toRingHom : (a : K) → L) x = x_1
rw : Eq.{u_3 + 1} (α := L) ((aeval x_1 : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
rw₁ :
  Eq.{u_3 + 1} (α := L) (((aeval ((f.toRingHom : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
rw₂ :
  Eq.{u_3 + 1} (α := L) (((aeval (((↑f : K →+* L) : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L)
    (0 : L)
rw₃ : Eq.{u_3 + 1} (α := L) (((aeval ((f : (a : K) → L) x) : F[X] →ₐ[F] L) : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
rw₄ : Eq.{u_3 + 1} (α := L) ((f : (a : K) → L) ((aeval x : (a : F[X]) → K) (minpoly F x) : K) : L) (0 : L)
rw₅ : Eq.{u_3 + 1} (α := L) ((f : (a : K) → L) 0 : L) (0 : L)
rw₆ rw₇ : Eq.{u_3 + 1} (α := L) 0 0
⊢ x_1 ∈ rootSet (minpoly F x) L

Tactic:
rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]

Premises used: Algebra.IsIntegral.isIntegral, AlgHom.coe_toRingHom, map_zero, minpoly.aeval, AlgHom.toRingHom_eq_coe, Polynomial.mem_rootSet_of_ne, Polynomial.aeval_algHom_apply, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ Eq (α := IntermediateField F L) (normalClosure F K L)
    (⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L))

Tactic:
normalClosure_le_iSup_adjoin.antisymm <|
    iSup_le fun x ↦ IntermediateField.adjoin_le_iff.mpr fun _ hy ↦
      let ⟨φ, hφ⟩ := IntermediateField.exists_algHom_of_splits_of_aeval
        (fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, splits x⟩) (mem_rootSet.mp hy).2
      le_iSup AlgHom.fieldRange φ ⟨x, hφ⟩

Premises used: Iff.mpr, Algebra.IsIntegral.isIntegral, IntermediateField.adjoin_le_iff, IntermediateField.normalClosure, Membership.mem, LE.le.antisymm, le_iSup, _private.0.Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits.match_1, AlgHom.fieldRange, SetLike.coe, And.right, And.intro, Exists.intro, Iff.mp, iSup_le, Polynomial.mem_rootSet, IntermediateField.exists_algHom_of_splits_of_aeval, Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
⊢ IsNormalClosure F K L ↔
    (∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))) ∧
      Eq (α := IntermediateField F L) (normalClosure F K L) ⊤

Tactic:
⟨fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩, fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩⟩

Premises used: _private.0.Algebra.IsAlgebraic.isNormalClosure_iff.match_2, IntermediateField.normalClosure, IsNormalClosure, And, _private.0.Algebra.IsAlgebraic.isNormalClosure_iff.match_1, And.intro, Iff.intro, Top.top, Eq, IsNormalClosure.mk
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
refine_1 :
  IsNormalClosure F K L →
    ∀ (splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x)))
      (h :
        Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)) ⊤),
      Eq (α := IntermediateField F L) (normalClosure F K L) ⊤
refine_2 :
  (∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))) ∧
      Eq (α := IntermediateField F L) (normalClosure F K L) ⊤ →
    ∀ (splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x)))
      (h : Eq (α := IntermediateField F L) (normalClosure F K L) ⊤),
      Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)) ⊤
⊢ IsNormalClosure F K L ↔
    (∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))) ∧
      Eq (α := IntermediateField F L) (normalClosure F K L) ⊤

Tactic:
refine ⟨fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩, fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩⟩
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
h_1 : IsNormalClosure F K L
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
h : Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)) ⊤
⊢ Eq (α := IntermediateField F L) (normalClosure F K L) ⊤

Tactic:
simpa only [normalClosure_eq_iSup_adjoin_of_splits splits] using h

Premises used: Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
h_1 :
  (∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))) ∧
    Eq (α := IntermediateField F L) (normalClosure F K L) ⊤
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
h : Eq (α := IntermediateField F L) (normalClosure F K L) ⊤
⊢ Eq.{u_3 + 1} (α := IntermediateField F L) (⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)) ⊤

Tactic:
simpa only [normalClosure_eq_iSup_adjoin_of_splits splits] using h

Premises used: Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
rw :
  (∀ (x : K),
      Splits.{u_3} (R := ↥(normalClosure F K L)) (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x))) ∧
    Eq.{u_3 + 1} (α := IntermediateField F ↥(normalClosure F K L)) (normalClosure F K ↥(normalClosure F K L)) ⊤
⊢ IsNormalClosure.{u_1, u_2, u_3} F K ↥(normalClosure F K L)

Tactic:
rw [isNormalClosure_iff]

Premises used: Algebra.IsAlgebraic.isNormalClosure_iff
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
left :
  ∀ (x : K),
    Splits.{u_3} (R := ↥(normalClosure F K L)) (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x))
right : Eq.{u_3 + 1} (α := IntermediateField F ↥(normalClosure F K L)) (normalClosure F K ↥(normalClosure F K L)) ⊤
⊢ (∀ (x : K),
      Splits.{u_3} (R := ↥(normalClosure F K L)) (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x))) ∧
    Eq.{u_3 + 1} (α := IntermediateField F ↥(normalClosure F K L)) (normalClosure F K ↥(normalClosure F K L)) ⊤

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
left :
  ∀ (x : K),
    Splits.{u_3} (R := ↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)))
      (Polynomial.map (algebraMap F ↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L))) (minpoly F x))
⊢ ∀ (x : K),
    Splits.{u_3} (R := ↥(normalClosure F K L)) (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x))

Tactic:
rw [normalClosure_eq_iSup_adjoin_of_splits splits]

Premises used: Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
⊢ LE.le (α := IntermediateField F L) (IntermediateField.adjoin F (rootSet (minpoly F x) L))
    (⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L))

Tactic:
apply le_iSup _ x

Premises used: le_iSup
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ ∀ (x : K),
    Splits.{u_3} (R := ↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L)))
      (Polynomial.map (algebraMap F ↥(⨆ (x : K), IntermediateField.adjoin F (rootSet (minpoly F x) L))) (minpoly F x))

Tactic:
exact fun x ↦ splits_of_splits (splits x) ((IntermediateField.subset_adjoin F _).trans <|
      SetLike.coe_subset_coe.mpr <| by apply le_iSup _ x)

Premises used: Iff.mpr, Polynomial.rootSet, HasSubset.Subset.trans, IntermediateField.subset_adjoin, minpoly, SetLike.coe_subset_coe, IntermediateField.splits_of_splits
-- Module: Mathlib.FieldTheory.Normal.Closure
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
inst_5 : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
right :
  LE.le.{u_3} (α := IntermediateField F ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)) ⊤
    (⨆ (f : AlgHom.{u_1, u_2, u_3} F K ↥(⨆ (f : K →ₐ[F] L), f.fieldRange)), f.fieldRange)
⊢ Eq.{u_3 + 1} (α := IntermediateField F ↥(normalClosure F K L)) (normalClosure F K ↥(normalClosure F K L)) ⊤

Tactic:
simp_rw [normalClosure, ← top_le_iff]

Premises used: IntermediateField.normalClosure, top_le_iff