awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
⊢ Module.rank F R ≤ Module.rank F K

Tactic:
have h1 := (IsScalarTower.toAlgHom F R K).toLinearMap.rank_le_of_injective hinj
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : Module.rank F R ≤ Module.rank F K
⊢ lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K

Tactic:
rw [MvPolynomial.rank_eq_lift, mk_finsupp_nat, lift_max, lift_aleph0, max_le_iff] at h1

Premises used: Cardinal.mk_finsupp_nat, max_le_iff, Cardinal.lift_aleph0, MvPolynomial.rank_eq_lift, Cardinal.lift_max
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
refine_2 : ∀ (i : σ), max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
obtain ⟨i⟩ := ‹Nonempty σ›

Premises used: Nonempty
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
⊢ Transcendental F (A := K) ((algebraMap R K : (a : R) → K) (MvPolynomial.X i) : K)

Tactic:
have hx : Transcendental F (algebraMap R K (MvPolynomial.X i)) :=
    (transcendental_algebraMap_iff hinj).2 (MvPolynomial.transcendental_X F i)
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F (A := K) ((algebraMap R K : (a : R) → K) (MvPolynomial.X i) : K)
⊢ lift.{max u v, v} #F ≤ lift.{v, max u v} (Module.rank F K)

Tactic:
have h2 := hx.linearIndependent_sub_inv.cardinal_lift_le_rank
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F (A := K) ((algebraMap R K : (a : R) → K) (MvPolynomial.X i) : K)
h2 : lift.{max u v, v} #F ≤ lift.{v, max u v} (Module.rank F K)
⊢ lift.{u, v} #F ≤ Module.rank F K

Tactic:
rw [lift_id'.{v, u}, lift_umax.{v, u}] at h2
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F (A := K) ((algebraMap R K : (a : R) → K) (MvPolynomial.X i) : K)
h2 : lift.{u, v} #F ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
max_le (max_le h2 h1.1) h1.2

Premises used: And.right, And.left, max_le
-- Module: Mathlib.FieldTheory.MvRatFunc.Rank
Goal:
σ : Type u
F : Type v
inst : Field F
inst_1 : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F (A := K) ((algebraMap R K : (a : R) → K) (MvPolynomial.X i) : K)
h2 : lift.{u, v} #F ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
exact max_le (max_le h2 h1.1) h1.2

Premises used: And.right, And.left, max_le
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
⊢ ∃ (p : F[X]), IsSplittingField F K p

Tactic:
⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩

Premises used: Finset.univ, RelEmbedding.injective, minpoly, Finset.prod, Subalgebra.toSubmodule, Exists.intro, Polynomial.IsSplittingField.mk, DFunLike.coe
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
minpoly :
  Eq (α := Submodule F K)
    ((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K)
        (Algebra.adjoin F
          (rootSet.{u_1, u_2} (T := F)
            (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
              _root_.minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K))
            K)) :
      Submodule F K)
    ((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K) ⊤ : Submodule F K)
⊢ ∃ (p : F[X]), IsSplittingField F K p

Tactic:
refine
    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
rw :
  ∀ (y : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)),
    Membership.mem (α := K)
      (↑((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K)
              (Algebra.adjoin F
                (rootSet.{u_1, u_2} (T := F)
                  (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
                    minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K))
                  K)) :
            Submodule F K) :
        Set K)
      ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) y : K)
⊢ Eq (α := Submodule F K)
    ((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K)
        (Algebra.adjoin F
          (rootSet.{u_1, u_2} (T := F)
            (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
              minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K))
            K)) :
      Submodule F K)
    ((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K) ⊤ : Submodule F K)

Tactic:
rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]

Premises used: eq_top_iff, Algebra.top_toSubmodule, Set.range_subset_iff, Module.Basis.span_eq, Submodule.span_le
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
⊢ ∀ (y : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)),
    Membership.mem (α := K)
      (↑((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K)
              (Algebra.adjoin F
                (rootSet.{u_1, u_2} (T := F)
                  (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
                    minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K))
                  K)) :
            Submodule F K) :
        Set K)
      ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) y : K)

Tactic:
fun x =>
    Algebra.subset_adjoin
      (Multiset.mem_toFinset.mpr <|
        (mem_roots <|
              mt (Polynomial.map_eq_zero <| algebraMap F K).1 <|
                Finset.prod_ne_zero_iff.2 fun x _ => ?_).2 ?_)

Premises used: Iff.mpr, iInf, Algebra.algebraMap, Set.Mem, Set.iInter, Algebra.subset_adjoin, setOf, mt, Finset.prod_ne_zero_iff, Polynomial.mem_roots, Iff.mp, Polynomial.map_eq_zero, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
refine_1 :
  ∀ (x x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)),
    Membership.mem (γ := Finset (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) Finset.univ x →
      Ne (α := F[X]) (minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K)) 0
refine_2 :
  ∀ (x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)),
    IsRoot
      (map (algebraMap F K : F →+* K)
        (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
          minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K)))
      ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x)
⊢ ∀ (y : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)),
    Membership.mem (α := K)
      (↑((Subalgebra.toSubmodule : (a : Subalgebra F K) → Submodule F K)
              (Algebra.adjoin F
                (rootSet.{u_1, u_2} (T := F)
                  (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
                    minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K))
                  K)) :
            Submodule F K) :
        Set K)
      ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) y : K)

Tactic:
refine fun x =>
    Algebra.subset_adjoin
      (Multiset.mem_toFinset.mpr <|
        (mem_roots <|
              mt (Polynomial.map_eq_zero <| algebraMap F K).1 <|
                Finset.prod_ne_zero_iff.2 fun x _ => ?_).2 ?_)

Premises used: Iff.mpr, Algebra.algebraMap, Algebra.subset_adjoin, mt, Finset.prod_ne_zero_iff, Polynomial.mem_roots, Iff.mp, Polynomial.map_eq_zero, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
x_1 x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)
h_1 : Membership.mem (γ := Finset (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) Finset.univ x
⊢ Ne (α := F[X]) (minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K)) 0

Tactic:
minpoly.ne_zero (h.isIntegral (s x))

Premises used: Normal.isIntegral, DFunLike.coe, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
x_1 x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)
h_1 : Membership.mem (γ := Finset (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) Finset.univ x
⊢ Ne (α := F[X]) (minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K)) 0

Tactic:
exact minpoly.ne_zero (h.isIntegral (s x))

Premises used: Normal.isIntegral, DFunLike.coe, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)
refine_2 :
  Eq.{u_2 + 1} (α := K)
    (∏ x_1 : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
      ((aeval ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x) : F[X] →ₐ[F] K) : (a : F[X]) → K)
        (minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x_1 : K)))
    0
⊢ IsRoot
    (map (algebraMap F K : F →+* K)
      (∏ x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
        minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x : K)))
    ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x)

Tactic:
rw [IsRoot.def, eval_map_algebraMap, map_prod]

Premises used: Polynomial.IsRoot.def, map_prod, Polynomial.eval_map_algebraMap
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)
⊢ Eq.{u_2 + 1} (α := K)
    (∏ x_1 : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
      ((aeval ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x) : F[X] →ₐ[F] K) : (a : F[X]) → K)
        (minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x_1 : K)))
    0

Tactic:
Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)

Premises used: Finset.mem_univ, minpoly.aeval, Finset.prod_eq_zero
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
h : Normal F K
inst_3 : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K
x : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)
⊢ Eq.{u_2 + 1} (α := K)
    (∏ x_1 : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2),
      ((aeval ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x) : F[X] →ₐ[F] K) : (a : F[X]) → K)
        (minpoly F (B := K) ((s : (a : (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2)) → K) x_1 : K)))
    0

Tactic:
exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)

Premises used: Finset.mem_univ, Finset.prod_eq_zero
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
inl : ∀ [hFEp : IsSplittingField F E 0], Normal F E
inr : ∀ (hp : p ≠ 0), Normal F E
⊢ Normal F E

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
hFEp : IsSplittingField F E 0
⊢ Eq (α := Subalgebra F E) (Algebra.adjoin F (rootSet.{u_1, u_3} (T := F) 0 E)) ⊤

Tactic:
have := hFEp.adjoin_rootSet
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
hFEp : IsSplittingField F E 0
this : Eq (α := Subalgebra F E) (Algebra.adjoin F (rootSet.{u_1, u_3} (T := F) 0 E)) ⊤
⊢ Eq.{u_3 + 1} (α := Subalgebra F E) ⊥ ⊤

Tactic:
rw [rootSet_zero, Algebra.adjoin_empty] at this

Premises used: Polynomial.rootSet_zero, Algebra.adjoin_empty
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
hFEp : IsSplittingField F E 0
this : Eq.{u_3 + 1} (α := Subalgebra F E) ⊥ ⊤
⊢ Normal F E

Tactic:
Normal.of_algEquiv
      (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm))

Premises used: Iff.mpr, AlgEquiv.ofBijective, Algebra.bijective_algebraMap_iff, Algebra.ofId, Normal.of_algEquiv, Eq.symm
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
hFEp : IsSplittingField F E 0
this : Eq.{u_3 + 1} (α := Subalgebra F E) ⊥ ⊤
⊢ Normal F E

Tactic:
exact Normal.of_algEquiv
      (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm))

Premises used: Iff.mpr, AlgEquiv.ofBijective, Algebra.bijective_algebraMap_iff, Algebra.ofId, Normal.of_algEquiv, Eq.symm
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
⊢ Normal F E

Tactic:
normal_iff.mpr fun x ↦ ?_

Premises used: Iff.mpr, normal_iff
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
inr : ∀ (x : E), IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
⊢ Normal F E

Tactic:
refine normal_iff.mpr fun x ↦ ?_

Premises used: Iff.mpr, normal_iff
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
⊢ FiniteDimensional F E

Tactic:
haveI : FiniteDimensional F E := IsSplittingField.finiteDimensional E p
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
⊢ IsIntegral F x

Tactic:
have hx := IsIntegral.of_finite F x
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
⊢ Splits (R := (p * minpoly F x).SplittingField)
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (p * minpoly F x))

Tactic:
have hL := SplittingField.splits (p * minpoly F x)
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (R := (p * minpoly F x).SplittingField)
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (p * minpoly F x))
inr :
  ∀
    (hL :
      Splits (R := (p * minpoly F x).SplittingField)
          (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p) ∧
        Splits (R := (p * minpoly F x).SplittingField)
          (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))),
    IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
rw :
  ∀
    (hL :
      (HMul.hMul (α := (p * minpoly F x).SplittingField[X])
          (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
          (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))).Splits),
    Ne (α := (p * minpoly F x).SplittingField[X]) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p) 0
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))

Tactic:
rw [Polynomial.map_mul, splits_mul_iff _ (map_ne_zero (minpoly.ne_zero hx))] at hL

Premises used: Polynomial.map_mul, Polynomial.splits_mul_iff, Polynomial.map_ne_zero, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p) ∧
    Splits (R := (p * minpoly F x).SplittingField)
      (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))
⊢ Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)

Tactic:
obtain ⟨hL1, hL2⟩ := hL
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p) ∧
    Splits (R := (p * minpoly F x).SplittingField)
      (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
⊢ Splits (R := (p * minpoly F x).SplittingField)
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))

Tactic:
obtain ⟨hL1, hL2⟩ := hL
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
hL2 :
  Splits (R := (p * minpoly F x).SplittingField)
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x))
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
⊢ Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))

Tactic:
rw [← j.comp_algebraMap, ← Polynomial.map_map] at hL2

Premises used: AlgHom.comp_algebraMap, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))

Tactic:
⟨hx, Splits.of_splits_map (j : E →+* L) hL2 fun a ha ↦ ?_⟩

Premises used: Polynomial.Splits.of_splits_map, RingHomClass.toRingHom, And.intro
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_3
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : Splits (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))
inr :
  ∀ (a : L) (ha : a ∈ roots (Polynomial.map (↑j : E →+* L) (Polynomial.map (algebraMap F E) (minpoly F x)))),
    Membership.mem (γ := Subring L) (RingHom.range (↑j : E →+* L)) a
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))

Tactic:
refine ⟨hx, Splits.of_splits_map (j : E →+* L) hL2 fun a ha ↦ ?_⟩