awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (hypothesis)
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)
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
have h2 : 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
-- Lean 4 proof step from Mathlib.FieldTheory.MvRatFunc.Rank (hypothesis)
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)
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
have h2₁ : lift.{u, v} #F ≤ Module.rank F K
Tactic: rw [lift_id'.{v, u}, lift_umax.{v, u}] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
have 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),
            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: refine
    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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)
have 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
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 ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
⊢ ∀ (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)
have 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)
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 ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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)
⊢ 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)
have 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
Tactic: rw [IsRoot.def, eval_map_algebraMap, map_prod]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
let let₁ let₂ : ∃ (p : F[X]), IsSplittingField F K p
⊢ ∃ (p : F[X]), IsSplittingField F K p
have let₃ : let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F 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: classical
  let s := Module.Basis.ofVectorSpace F K
  refine
    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
  rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
  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 ?_)
  · exact minpoly.ne_zero (h.isIntegral (s x))
  rw [IsRoot.def, eval_map_algebraMap, map_prod]
  exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
let let₁ let₂ : ∃ (p : F[X]), IsSplittingField F K p
let₃ :
  let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F 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)
⊢ ∃ (p : F[X]), IsSplittingField F K p
have let₄ : let 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: classical
  let s := Module.Basis.ofVectorSpace F K
  refine
    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
  rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
  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 ?_)
  · exact minpoly.ne_zero (h.isIntegral (s x))
  rw [IsRoot.def, eval_map_algebraMap, map_prod]
  exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
let let₁ let₂ : ∃ (p : F[X]), IsSplittingField F K p
let₃ :
  let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F 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)
let₄ :
  let 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)
⊢ ∃ (p : F[X]), IsSplittingField F K p
have refine_1 : let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K;
∀ (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
Tactic: classical
  let s := Module.Basis.ofVectorSpace F K
  refine
    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
  rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
  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 ?_)
  · exact minpoly.ne_zero (h.isIntegral (s x))
  rw [IsRoot.def, eval_map_algebraMap, map_prod]
  exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
let let₁ let₂ : ∃ (p : F[X]), IsSplittingField F K p
let₃ :
  let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F 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)
let₄ :
  let 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)
refine_1 :
  let s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K) : Type u_2) F K := Module.Basis.ofVectorSpace F K;
  ∀ (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
⊢ ∃ (p : F[X]), IsSplittingField F K p
have refine_2 : let 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)),
  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: classical
  let s := Module.Basis.ofVectorSpace F K
  refine
    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
  rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
  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 ?_)
  · exact minpoly.ne_zero (h.isIntegral (s x))
  rw [IsRoot.def, eval_map_algebraMap, map_prod]
  exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
⊢ Normal F E
have inl : ∀ [hFEp : IsSplittingField F E 0], Normal F E
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
Cleared hypotheses: p, hFEp
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
⊢ Normal F E
have inr : ∀ (hp : p ≠ 0), Normal F E
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
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
⊢ Normal F E
have this : Eq (α := Subalgebra F E) (Algebra.adjoin F (rootSet.{u_1, u_3} (T := F) 0 E)) ⊤
Tactic: have := hFEp.adjoin_rootSet
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
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)) ⊤
⊢ Normal F E
have this₁ : Eq.{u_3 + 1} (α := Subalgebra F E) ⊥ ⊤
Tactic: rw [rootSet_zero, Algebra.adjoin_empty] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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
have inr : ∀ (x : E), IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
Tactic: refine normal_iff.mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
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
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have this : FiniteDimensional F E
Tactic: haveI : FiniteDimensional F E := IsSplittingField.finiteDimensional E p
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
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 ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have hx : IsIntegral F x
Tactic: have hx := IsIntegral.of_finite F x
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
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
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have hL : 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)
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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))
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have 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))
Tactic: rw [Polynomial.map_mul, splits_mul_iff _ (map_ne_zero (minpoly.ne_zero hx))] at hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (goal)
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))
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have 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
Tactic: rw [Polynomial.map_mul, splits_mul_iff _ (map_ne_zero (minpoly.ne_zero hx))] at hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Basic (hypothesis)
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))
⊢ IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have hL1 : Splits (R := (p * minpoly F x).SplittingField) (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p)
Tactic: obtain ⟨hL1, hL2⟩ := hL
Cleared hypotheses: hL