awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : K[X]
inst_3 : IsSplittingField K L f
h : f.Splits
y : L
hy : y ∈ (↑(Multiset.toFinset (Multiset.map (⇑(algebraMap K L) : (a : K) → L) f.roots)) : Set L)
rw : ∀ (hy : y ∈ (↑(Finset.image (⇑(algebraMap K L) : (a : K) → L) f.roots.toFinset) : Set L)), y ∈ (↑⊥ : Set L)
rw₁ :
  ∀ (hy : Membership.mem (γ := Finset L) (Finset.image (⇑(algebraMap K L) : (a : K) → L) f.roots.toFinset) y),
    y ∈ (↑⊥ : Set L)
rw₂ rw₃ rw₄ : ∀ (hy : ∃ a ∈ f.roots.toFinset, (algebraMap K L : (a : K) → L) a = y), y ∈ (↑⊥ : Set L)
rw₅ : ∀ (x : K) (hxy : (algebraMap K L : (a : K) → L) x = y), y ∈ (↑⊥ : Set L)
⊢ y ∈ (↑⊥ : Set L)
have rw₆ : ∀ (x : K) (hxy : (algebraMap K L : (a : K) → L) x = y),
  Membership.mem (α := L) (↑⊥ : Set L) ((algebraMap K L : (a : K) → L) x : L)
Tactic: classical
    rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
    obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
    rw [← hxy]
    exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _
Cleared hypotheses: hy
-- 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
f : K[X]
inst_3 : IsSplittingField K L f
h : Eq.{w + 1} (α := Subalgebra K L) ⊤ ⊥
⊢ f.Splits
have rw : Splits
  (Polynomial.map (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) sorry)))
    (Polynomial.map (RingEquiv.toRingHom (RingEquiv.ofBijective (algebraMap K L) sorry)) f))
Tactic: rw [← Polynomial.map_id (p := f), ← RingEquiv.toRingHom_refl, ← RingEquiv.self_trans_symm
      (RingEquiv.ofBijective _ <| Algebra.bijective_algebraMap_iff.2 h),
      RingEquiv.toRingHom_trans, ← 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 F K
inst_5 : Algebra F L
inst_6 : IsScalarTower F K L
f : F[X]
inst_7 : IsSplittingField K L (((mapAlg F K : AlgHom.{u, u, v} F F[X] K[X]) : (a : F[X]) → K[X]) f)
⊢ Splits.{w} (R := L) (((mapAlg F L : AlgHom.{u, u, w} F F[X] L[X]) : (a : F[X]) → L[X]) f)
have rw : Splits (Polynomial.map (algebraMap K L) (((mapAlg F K : AlgHom.{u, u, v} F F[X] K[X]) : (a : F[X]) → K[X]) f))
Tactic: rw [mapAlg_comp K L f, mapAlg_eq_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 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)
⊢ IsSplittingField F L (f * g)
have splits' : Splits (Polynomial.map (algebraMap F L) (f * g))
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 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)
splits' : Splits (Polynomial.map (algebraMap F L) (f * g))
⊢ IsSplittingField F L (f * g)
have adjoin_rootSet' : Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).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 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)
⊢ Splits (Polynomial.map (algebraMap F L) (f * g))
have splits' : (HMul.hMul (α := L[X]) (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f))
    (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) g))).Splits
Tactic: rw [Polynomial.map_mul, IsScalarTower.algebraMap_eq F K L, ← map_map, ← 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 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)
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet' : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f * g).aroots L).toFinset : Set L)) ⊤
Tactic: 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)) ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₁ : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑(f.aroots L + g.aroots L).toFinset : Set L)) ⊤
Tactic: 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)) ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₂ : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f.aroots L).toFinset ∪ (g.aroots L).toFinset) : Set L)) ⊤
Tactic: 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)) ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₃ : Eq (α := Subalgebra F L) (Algebra.adjoin F ((↑(f.aroots L).toFinset : Set L) ∪ (↑(g.aroots L).toFinset : Set L))) ⊤
Tactic: 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))) ⊤
⊢ 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: 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: 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: 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: 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)
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet' : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f * 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)) ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₁ : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑(f.aroots 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)) ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₂ : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f.aroots L).toFinset ∪ (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)) ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₃ : Eq (α := Subalgebra F L) (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]