awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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)
adjoin_rootSet' : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f * g).aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₁ : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑(f.aroots L + g.aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₂ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f.aroots L).toFinset ∪ (g.aroots L).toFinset) : Set L)) ⊤
adjoin_rootSet'₃ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F ((↑(f.aroots L).toFinset : Set L) ∪ (↑(g.aroots L).toFinset : Set L))) ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₄ : Eq (α := Subalgebra F L)
  (Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)))
    (Algebra.adjoin ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)) (↑(g.aroots L).toFinset : Set L)))
  ⊤
Tactic: classical
    rw [rootSet, aroots_mul (mul_ne_zero hf hg),
      Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
      aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map, (splits K f).roots_map,
      Multiset.toFinset_map, Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet,
      Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet,
      Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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)
adjoin_rootSet' : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f * g).aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₁ : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑(f.aroots L + g.aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₂ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f.aroots L).toFinset ∪ (g.aroots L).toFinset) : Set L)) ⊤
adjoin_rootSet'₃ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F ((↑(f.aroots L).toFinset : Set L) ∪ (↑(g.aroots L).toFinset : Set L))) ⊤
adjoin_rootSet'₄ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)))
      (Algebra.adjoin ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)) (↑(g.aroots L).toFinset : Set L)))
    ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₅ : Eq (α := Subalgebra F L)
  (Subalgebra.restrictScalars F (S :=
    ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L)))
    (Algebra.adjoin ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))
      (↑(g.aroots L).toFinset : Set L)))
  ⊤
Tactic: classical
    rw [rootSet, aroots_mul (mul_ne_zero hf hg),
      Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
      aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map, (splits K f).roots_map,
      Multiset.toFinset_map, Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet,
      Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet,
      Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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)
adjoin_rootSet' : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f * g).aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₁ : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑(f.aroots L + g.aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₂ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f.aroots L).toFinset ∪ (g.aroots L).toFinset) : Set L)) ⊤
adjoin_rootSet'₃ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F ((↑(f.aroots L).toFinset : Set L) ∪ (↑(g.aroots L).toFinset : Set L))) ⊤
adjoin_rootSet'₄ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)))
      (Algebra.adjoin ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)) (↑(g.aroots L).toFinset : Set L)))
    ⊤
adjoin_rootSet'₅ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L)))
      (Algebra.adjoin ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))
        (↑(g.aroots L).toFinset : Set L)))
    ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₆ : Eq (α := Subalgebra F L)
  (Subalgebra.restrictScalars F (S :=
    ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L)))
    (Algebra.adjoin ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))
      (↑(roots (Polynomial.map (algebraMap F L) g)).toFinset : Set L)))
  ⊤
Tactic: classical
    rw [rootSet, aroots_mul (mul_ne_zero hf hg),
      Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
      aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map, (splits K f).roots_map,
      Multiset.toFinset_map, Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet,
      Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet,
      Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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)
adjoin_rootSet' : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f * g).aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₁ : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑(f.aroots L + g.aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₂ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f.aroots L).toFinset ∪ (g.aroots L).toFinset) : Set L)) ⊤
adjoin_rootSet'₃ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F ((↑(f.aroots L).toFinset : Set L) ∪ (↑(g.aroots L).toFinset : Set L))) ⊤
adjoin_rootSet'₄ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)))
      (Algebra.adjoin ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)) (↑(g.aroots L).toFinset : Set L)))
    ⊤
adjoin_rootSet'₅ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L)))
      (Algebra.adjoin ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))
        (↑(g.aroots L).toFinset : Set L)))
    ⊤
adjoin_rootSet'₆ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L)))
      (Algebra.adjoin ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))
        (↑(roots (Polynomial.map (algebraMap F L) g)).toFinset : Set L)))
    ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₇ : Eq (α := Subalgebra F L)
  (Subalgebra.restrictScalars F (S :=
    ↥(Algebra.adjoin F
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  f)).toFinset :
          Set L)))
    (Algebra.adjoin
      ↥(Algebra.adjoin F
          (↑(roots
                  (Polynomial.map
                    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                    f)).toFinset :
            Set L))
      (↑(roots
              (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                g)).toFinset :
        Set L)))
  ⊤
Tactic: classical
    rw [rootSet, aroots_mul (mul_ne_zero hf hg),
      Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
      aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map, (splits K f).roots_map,
      Multiset.toFinset_map, Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet,
      Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet,
      Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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] ↥⊥
have rw : L →ₐ[K] ↥⊤
Tactic: rw [← (splits_iff L f).1 (show f.Splits by simp [hf0])]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
⊢ AlgHom.{v, w, u} K (↥⊤) F
have rw : AlgHom.{v, w, u} K (↥(Algebra.adjoin K (f.rootSet L))) F
Tactic: rw [← adjoin_rootSet L f]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (hypothesis)
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
⊢ IsIntegral K y
have hy₁ : Membership.mem (γ := Set L) ∅ y
Tactic: rw [hf, rootSet_zero] at hy
Cleared hypotheses: hy, hf
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (hypothesis)
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
⊢ Algebra.IsAlgebraic F L
have this : FiniteDimensional K L
Tactic: have : FiniteDimensional K L := IsSplittingField.finiteDimensional L f
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
⊢ IsSplittingField K L p
have splits' : Splits (Polynomial.map (algebraMap K L) p)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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)
⊢ IsSplittingField K L p
have adjoin_rootSet' : Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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 (algebraMap K L) p)
have splits' : Splits (Polynomial.map (↑(↑f : F →ₐ[K] L) : F →+* L) (Polynomial.map (algebraMap K F) p))
Tactic: rw [← f.toAlgHom.comp_algebraMap, ← map_map]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
⊢ Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) ⊤
have adjoin_rootSet' : Algebra.adjoin K (p.rootSet L) = (↑f : F →ₐ[K] L).range
Tactic: rw [← (AlgHom.range_eq_top f.toAlgHom).mpr f.surjective,
      (splits F p).adjoin_rootSet_eq_range, adjoin_rootSet F p]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
⊢ Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) ⊤
have adjoin_rootSet'₁ : Eq (α := Subalgebra K F) (Algebra.adjoin K (p.rootSet F)) ⊤
Tactic: rw [← (AlgHom.range_eq_top f.toAlgHom).mpr f.surjective,
      (splits F p).adjoin_rootSet_eq_range, adjoin_rootSet F p]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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)) ⊤
⊢ Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) ⊤
have adjoin_rootSet'₂ : Eq.{u + 1} (α := Subalgebra K F) ⊤ ⊤
Tactic: rw [← (AlgHom.range_eq_top f.toAlgHom).mpr f.surjective,
      (splits F p).adjoin_rootSet_eq_range, adjoin_rootSet F p]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (hypothesis)
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
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
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)
Tactic: have := Splits.of_splits_map (f := p.map (algebraMap K F)) (algebraMap F L)
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (hypothesis)
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)
⊢ 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)
Tactic: rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
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)
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)
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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)
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
have 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)
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)
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
have refine : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) → ∀ x ∈ p.rootSet L, x ∈ F
Tactic: refine ⟨?_, IntermediateField.splits_of_splits h⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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 ∈ p.rootSet L, x ∈ F
have rw : ∀ ⦃x : ↥F⦄, Membership.mem (γ := Set ↥F) (p.rootSet ↥F) x → Membership.mem (α := L) F ((F.val : (a : ↥F) → L) x : L)
Tactic: rw [← hF.image_rootSet F.val, Set.forall_mem_image]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
have rw : x ∈ F.val.fieldRange
Tactic: rw [← F.fieldRange_val]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
p : K[X]
⊢ IsSplittingField K L p ↔
    Splits (map (algebraMap K L) p) ∧ Eq (α := IntermediateField K L) (IntermediateField.adjoin K (p.rootSet L)) ⊤
have rw : IsSplittingField K L p ↔
  Splits (map (algebraMap K L) p) ∧
    Eq (α := Subalgebra K L) (Algebra.adjoin K (p.rootSet L)) (IntermediateField.toSubalgebra ⊤)
Tactic: rw [← IntermediateField.toSubalgebra_injective.eq_iff,
      IntermediateField.adjoin_toSubalgebra_of_isAlgebraic fun _ ↦ isAlgebraic_of_mem_rootSet]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
⊢ IsSplittingField.{v, w} K (↥F) p ↔
    Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) ∧ F = adjoin K (p.rootSet L)
have suffices : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
  (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔ F = adjoin K (p.rootSet L))
Tactic: suffices _ → (Algebra.adjoin K (p.rootSet F) = ⊤ ↔ F = adjoin K (p.rootSet L)) by
    exact ⟨fun h ↦ ⟨h.1, (this h.1).mp h.2⟩, fun h ↦ ⟨h.1, (this h.1).mpr h.2⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
    (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔ F = adjoin K (p.rootSet L))
have rw : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
  (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔
    F.toSubalgebra = Algebra.adjoin K (p.rootSet L))
Tactic: rw [← toSubalgebra_injective.eq_iff,
      adjoin_toSubalgebra_of_isAlgebraic fun x ↦ isAlgebraic_of_mem_rootSet]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
⊢ Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p) →
    (Eq.{w + 1} (α := Subalgebra K ↥F) (Algebra.adjoin K (p.rootSet ↥F)) ⊤ ↔
      F.toSubalgebra = Algebra.adjoin K (p.rootSet L))
have refine : ∀ (hp : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)),
  Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L)
Tactic: refine fun hp ↦ (hp.adjoin_rootSet_eq_range F.val).symm.trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
hp : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
⊢ Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L)
have rw : Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.val.range = Algebra.adjoin K (p.rootSet L)
Tactic: rw [← F.range_val, eq_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
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
hp : Splits.{w} (R := ↥F) (Polynomial.map (algebraMap K ↥F) p)
rw : Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.val.range = Algebra.adjoin K (p.rootSet L)
⊢ Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L)
have rw₁ : F.val.range = Algebra.adjoin K (p.rootSet L) ↔ F.val.range = Algebra.adjoin K (p.rootSet L)
Tactic: rw [← F.range_val, eq_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.Tower (goal)
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : AddCommMonoid A
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : Eq (α := Submodule F A) (span F (↑b : Set A)) ⊤
⊢ Eq (α := Submodule F A) (restrictScalars F (span K (↑b : Set A))) (restrictScalars.{u, v, w} F (R := K) ⊤)
have rw : (↑b : Set A) ⊆ (↑(restrictScalars F (span K (↑b : Set A))) : Set A)
Tactic: rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]