awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite.{v + 1} (Emb F ↥(adjoin F (Set.range x)) × Emb (↥(adjoin F (Set.range x))) E)
have refine : Infinite.{v + 1} (Emb F ↥(adjoin F (Set.range x)))
Tactic: refine @Prod.infinite_of_left _ _ ?_ _
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite.{v + 1} (Emb F ↥(adjoin F (Set.range x)))
have rw : Infinite (Emb F (FractionRing (MvPolynomial ι F)))
Tactic: rw [← (embEquivOfEquiv _ _ _ hx.1.aevalEquivField).infinite_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))
have obtain : ∀ (i : ι), Infinite (Emb F (FractionRing (MvPolynomial ι F)))
Tactic: obtain ⟨i⟩ := hx.nonempty_iff_transcendental.2 H
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
⊢ Function.Injective (α := MvPolynomial ι F) (β := AlgebraicClosure K)
    (⇑i1 : (a : MvPolynomial ι F) → AlgebraicClosure K)
have rw : Function.Injective (α := MvPolynomial ι F) (β := AlgebraicClosure K)
  (⇑(RingHom.comp (algebraMap K (AlgebraicClosure K)) (algebraMap (MvPolynomial ι F) K)) :
    (a : MvPolynomial ι F) → AlgebraicClosure K)
Tactic: rw [IsScalarTower.coe_toAlgHom', IsScalarTower.algebraMap_eq _ K]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))
have hi1 : Function.Injective (α := MvPolynomial ι F) (β := AlgebraicClosure K) (⇑i1 : (a : MvPolynomial ι F) → AlgebraicClosure K)
Tactic: have hi1 : Function.Injective i1 := by
    rw [IsScalarTower.coe_toAlgHom', IsScalarTower.algebraMap_eq _ K]
    exact (algebraMap K (AlgebraicClosure K)).injective.comp (IsFractionRing.injective _ _)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 :
  Function.Injective (α := MvPolynomial ι F) (β := AlgebraicClosure K)
    (⇑i1 : (a : MvPolynomial ι F) → AlgebraicClosure K)
f : (n : ℕ) → Emb F K :=
  fun (n : ℕ) ↦
    IsFractionRing.liftAlgHom (R := F) (A := MvPolynomial ι F) (K := K) (L := AlgebraicClosure K) (g :=
      i1.comp (MvPolynomial.aeval fun (i : ι) ↦ HPow.hPow (α := MvPolynomial ι F) (MvPolynomial.X i) (n + 1))) ⋯
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))
have refine : ∀ (m n : ℕ) (h : f m = f n), m = n
Tactic: refine Infinite.of_injective f fun m n h ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 :
  Function.Injective (α := MvPolynomial ι F) (β := AlgebraicClosure K)
    (⇑i1 : (a : MvPolynomial ι F) → AlgebraicClosure K)
f : (n : ℕ) → Emb F K :=
  fun (n : ℕ) ↦
    IsFractionRing.liftAlgHom (R := F) (A := MvPolynomial ι F) (K := K) (L := AlgebraicClosure K) (g :=
      i1.comp (MvPolynomial.aeval fun (i : ι) ↦ HPow.hPow (α := MvPolynomial ι F) (MvPolynomial.X i) (n + 1))) ⋯
m n : ℕ
h : f m = f n
⊢ m = n
have h₁ : HPow.hPow (α := MvPolynomial ι F) (MvPolynomial.X i) (m + 1) =
  HPow.hPow (α := MvPolynomial ι F) (MvPolynomial.X i) (n + 1)
Tactic: replace h : (MvPolynomial.X i) ^ (m + 1) = (MvPolynomial.X i) ^ (n + 1) := hi1 <| by
    simpa [f, -map_pow] using congr($h (algebraMap _ K (MvPolynomial.X (R := F) i)))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
⊢ f.natSepDegree ≤ f.natDegree
have this : Multiset.card (α := f.SplittingField) (roots (map (algebraMap F f.SplittingField) f)) ≤
  natDegree (R := f.SplittingField) (map (algebraMap F f.SplittingField) f)
Tactic: have := f.map (algebraMap F f.SplittingField) |>.card_roots'
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
this :
  Multiset.card (α := f.SplittingField) (roots (map (algebraMap F f.SplittingField) f)) ≤
    natDegree (R := f.SplittingField) (map (algebraMap F f.SplittingField) f)
⊢ f.natSepDegree ≤ f.natDegree
have this₁ : Multiset.card (α := f.SplittingField) (f.aroots f.SplittingField) ≤ f.natDegree
Tactic: rw [← aroots_def, natDegree_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree = 0
⊢ f.natSepDegree = 0
have linarith : f.natSepDegree < 0 →
  -1 + HSub.hSub (α := ℤ) 0 (↑f.natSepDegree : ℤ) + (HAdd.hAdd (α := ℤ) (↑f.natSepDegree : ℤ) 1 - 0) = 0
Tactic: linarith only [natSepDegree_le_natDegree f, h]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree = 0
linarith :
  f.natSepDegree < 0 →
    -1 + HSub.hSub (α := ℤ) 0 (↑f.natSepDegree : ℤ) + (HAdd.hAdd (α := ℤ) (↑f.natSepDegree : ℤ) 1 - 0) = 0
⊢ f.natSepDegree = 0
have linarith₁ : 0 < f.natSepDegree →
  -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑f.natSepDegree : ℤ)) + HSub.hSub (α := ℤ) (↑f.natSepDegree : ℤ) (↑f.natDegree : ℤ) +
      HSub.hSub (α := ℤ) (↑f.natDegree : ℤ) 0 =
    0
Tactic: linarith only [natSepDegree_le_natDegree f, h]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
⊢ natSepDegree.{u} (F := F) 0 = 0
have rw : natSepDegree.{u} (F := F) ((C : (a : F) → F[X]) 0) = 0
Tactic: rw [← C_0, natSepDegree_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
rw : natSepDegree.{u} (F := F) ((C : (a : F) → F[X]) 0) = 0
⊢ natSepDegree.{u} (F := F) 0 = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [← C_0, natSepDegree_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
⊢ natSepDegree.{u} (F := F) 1 = 0
have rw : natSepDegree.{u} (F := F) ((C : (a : F) → F[X]) 1) = 0
Tactic: rw [← C_1, natSepDegree_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
rw : natSepDegree.{u} (F := F) ((C : (a : F) → F[X]) 1) = 0
⊢ natSepDegree.{u} (F := F) 1 = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [← C_1, natSepDegree_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f.natSepDegree ≠ 0
have rw : Finset.Nonempty (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField))
Tactic: rw [natSepDegree, ne_eq, Finset.card_eq_zero, ← ne_eq, ← Finset.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ natDegree (R := f.SplittingField) (map (algebraMap F f.SplittingField) f) ≠ Zero.zero
have rwa : f.natDegree ≠ Zero.zero
Tactic: rwa [natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ Finset.Nonempty (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField))
have h₁ : Membership.mem (γ := Finset f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) (rootOfSplits sorry sorry)
Tactic: use rootOfSplits (SplittingField.splits f) (degree_ne_of_natDegree_ne (by rwa [natDegree_map]))
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ Membership.mem (γ := Finset f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) (rootOfSplits ⋯ ⋯)
have h₁ : f ≠ 0 ∧ Eq (α := f.SplittingField) ((aeval (rootOfSplits sorry sorry) : (a : F[X]) → f.SplittingField) f) 0
Tactic: rw [Multiset.mem_toFinset, mem_aroots]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ Membership.mem (γ := Finset f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) (rootOfSplits ⋯ ⋯)
have h₁ : Membership.mem (γ := Multiset f.SplittingField) (f.aroots f.SplittingField) (rootOfSplits sorry sorry)
Tactic: classical
  rw [Multiset.mem_toFinset, mem_aroots]
  exact ⟨ne_of_apply_ne _ h, by simp only [← eval_map_algebraMap, eval_rootOfSplits]⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
h₁ : Membership.mem (γ := Multiset f.SplittingField) (f.aroots f.SplittingField) (rootOfSplits ⋯ ⋯)
⊢ Membership.mem (γ := Finset f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) (rootOfSplits ⋯ ⋯)
have h₂ : f ≠ 0 ∧ Eq (α := f.SplittingField) ((aeval (rootOfSplits sorry sorry) : (a : F[X]) → f.SplittingField) f) 0
Tactic: classical
  rw [Multiset.mem_toFinset, mem_aroots]
  exact ⟨ne_of_apply_ne _ h, by simp only [← eval_map_algebraMap, eval_rootOfSplits]⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ f.Separable
have simp_rw : f.natSepDegree = f.natDegree ↔
  Finset.card (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) = f.natDegree
Tactic: simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ f.Separable
have simp_rw : f.natSepDegree = f.natDegree ↔ Fintype.card.{u} (↑(f.rootSet f.SplittingField) : Type u) = f.natDegree
Tactic: classical
  simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rfl
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
simp_rw : f.natSepDegree = f.natDegree ↔ Fintype.card.{u} (↑(f.rootSet f.SplittingField) : Type u) = f.natDegree
⊢ f.natSepDegree = f.natDegree ↔ f.Separable
have simp_rw₁ : f.natSepDegree = f.natDegree ↔
  Fintype.card.{u} (↑(↑(Multiset.toFinset (f.aroots f.SplittingField)) : Set f.SplittingField) : Type u) = f.natDegree
Tactic: classical
  simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rfl
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
simp_rw : f.natSepDegree = f.natDegree ↔ Fintype.card.{u} (↑(f.rootSet f.SplittingField) : Type u) = f.natDegree
simp_rw₁ :
  f.natSepDegree = f.natDegree ↔
    Fintype.card.{u} (↑(↑(Multiset.toFinset (f.aroots f.SplittingField)) : Set f.SplittingField) : Type u) = f.natDegree
⊢ f.natSepDegree = f.natDegree ↔ f.Separable
have simp_rw₂ : f.natSepDegree = f.natDegree ↔ Fintype.card.{u} ↥(Multiset.toFinset (f.aroots f.SplittingField)) = f.natDegree
Tactic: classical
  simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rfl
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
simp_rw : f.natSepDegree = f.natDegree ↔ Fintype.card.{u} (↑(f.rootSet f.SplittingField) : Type u) = f.natDegree
simp_rw₁ :
  f.natSepDegree = f.natDegree ↔
    Fintype.card.{u} (↑(↑(Multiset.toFinset (f.aroots f.SplittingField)) : Set f.SplittingField) : Type u) = f.natDegree
simp_rw₂ :
  f.natSepDegree = f.natDegree ↔ Fintype.card.{u} ↥(Multiset.toFinset (f.aroots f.SplittingField)) = f.natDegree
⊢ f.natSepDegree = f.natDegree ↔ f.Separable
have simp_rw₃ : f.natSepDegree = f.natDegree ↔
  Finset.card (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) = f.natDegree
Tactic: classical
  simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rfl
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
inst_3 : DecidableEq E
h : Splits (map (algebraMap F E) f)
⊢ f.natSepDegree = (f.aroots E).toFinset.card
have rw : f.natSepDegree = (roots (map (algebraMap F E) f)).toFinset.card
Tactic: rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
inst_3 : DecidableEq E
h : Splits (map (algebraMap F E) f)
rw : f.natSepDegree = (roots (map (algebraMap F E) f)).toFinset.card
⊢ f.natSepDegree = (f.aroots E).toFinset.card
have rw₁ : f.natSepDegree =
  (roots
        (map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(SplittingField.lift f h) : f.SplittingField →+* E)
            (algebraMap F f.SplittingField))
          f)).toFinset.card
Tactic: rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
inst_3 : DecidableEq E
h : Splits (map (algebraMap F E) f)
rw : f.natSepDegree = (roots (map (algebraMap F E) f)).toFinset.card
rw₁ :
  f.natSepDegree =
    (roots
          (map
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(SplittingField.lift f h) : f.SplittingField →+* E)
              (algebraMap F f.SplittingField))
            f)).toFinset.card
⊢ f.natSepDegree = (f.aroots E).toFinset.card
have rw₂ : f.natSepDegree =
  (roots
        (map (↑(SplittingField.lift f h) : f.SplittingField →+* E)
          (map (algebraMap F f.SplittingField) f))).toFinset.card
Tactic: rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
inst_3 : DecidableEq E
h : Splits (map (algebraMap F E) f)
rw : f.natSepDegree = (roots (map (algebraMap F E) f)).toFinset.card
rw₁ :
  f.natSepDegree =
    (roots
          (map
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(SplittingField.lift f h) : f.SplittingField →+* E)
              (algebraMap F f.SplittingField))
            f)).toFinset.card
rw₂ :
  f.natSepDegree =
    (roots
          (map (↑(SplittingField.lift f h) : f.SplittingField →+* E)
            (map (algebraMap F f.SplittingField) f))).toFinset.card
⊢ f.natSepDegree = (f.aroots E).toFinset.card
have rw₃ : f.natSepDegree =
  Finset.card.{v} (α := E)
    (Multiset.toFinset
      (Multiset.map (α := f.SplittingField)
        (⇑(↑(SplittingField.lift f h) : f.SplittingField →+* E) : (a : f.SplittingField) → E)
        (roots (map (algebraMap F f.SplittingField) f))))
Tactic: rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
inst_3 : DecidableEq E
h : Splits (map (algebraMap F E) f)
rw : f.natSepDegree = (roots (map (algebraMap F E) f)).toFinset.card
rw₁ :
  f.natSepDegree =
    (roots
          (map
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(SplittingField.lift f h) : f.SplittingField →+* E)
              (algebraMap F f.SplittingField))
            f)).toFinset.card
rw₂ :
  f.natSepDegree =
    (roots
          (map (↑(SplittingField.lift f h) : f.SplittingField →+* E)
            (map (algebraMap F f.SplittingField) f))).toFinset.card
rw₃ :
  f.natSepDegree =
    Finset.card.{v} (α := E)
      (Multiset.toFinset
        (Multiset.map (α := f.SplittingField)
          (⇑(↑(SplittingField.lift f h) : f.SplittingField →+* E) : (a : f.SplittingField) → E)
          (roots (map (algebraMap F f.SplittingField) f))))
⊢ f.natSepDegree = (f.aroots E).toFinset.card
have rw₄ : f.natSepDegree =
  Finset.card.{v} (α := E)
    (Finset.image (α := f.SplittingField)
      (⇑(↑(SplittingField.lift f h) : f.SplittingField →+* E) : (a : f.SplittingField) → E)
      (Multiset.toFinset (roots (map (algebraMap F f.SplittingField) f))))
Tactic: rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
inst_3 : DecidableEq E
h : Splits (map (algebraMap F E) f)
rw : f.natSepDegree = (roots (map (algebraMap F E) f)).toFinset.card
rw₁ :
  f.natSepDegree =
    (roots
          (map
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(SplittingField.lift f h) : f.SplittingField →+* E)
              (algebraMap F f.SplittingField))
            f)).toFinset.card
rw₂ :
  f.natSepDegree =
    (roots
          (map (↑(SplittingField.lift f h) : f.SplittingField →+* E)
            (map (algebraMap F f.SplittingField) f))).toFinset.card
rw₃ :
  f.natSepDegree =
    Finset.card.{v} (α := E)
      (Multiset.toFinset
        (Multiset.map (α := f.SplittingField)
          (⇑(↑(SplittingField.lift f h) : f.SplittingField →+* E) : (a : f.SplittingField) → E)
          (roots (map (algebraMap F f.SplittingField) f))))
rw₄ :
  f.natSepDegree =
    Finset.card.{v} (α := E)
      (Finset.image (α := f.SplittingField)
        (⇑(↑(SplittingField.lift f h) : f.SplittingField →+* E) : (a : f.SplittingField) → E)
        (Multiset.toFinset (roots (map (algebraMap F f.SplittingField) f))))
⊢ f.natSepDegree = (f.aroots E).toFinset.card
have rw₅ : f.natSepDegree = Finset.card (α := f.SplittingField) (Multiset.toFinset (roots (map (algebraMap F f.SplittingField) f)))
Tactic: rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
inst_3 : DecidableEq E
h : Splits (map (algebraMap F E) f)
rw : f.natSepDegree = (roots (map (algebraMap F E) f)).toFinset.card
rw₁ :
  f.natSepDegree =
    (roots
          (map
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(SplittingField.lift f h) : f.SplittingField →+* E)
              (algebraMap F f.SplittingField))
            f)).toFinset.card
rw₂ :
  f.natSepDegree =
    (roots
          (map (↑(SplittingField.lift f h) : f.SplittingField →+* E)
            (map (algebraMap F f.SplittingField) f))).toFinset.card
rw₃ :
  f.natSepDegree =
    Finset.card.{v} (α := E)
      (Multiset.toFinset
        (Multiset.map (α := f.SplittingField)
          (⇑(↑(SplittingField.lift f h) : f.SplittingField →+* E) : (a : f.SplittingField) → E)
          (roots (map (algebraMap F f.SplittingField) f))))
rw₄ :
  f.natSepDegree =
    Finset.card.{v} (α := E)
      (Finset.image (α := f.SplittingField)
        (⇑(↑(SplittingField.lift f h) : f.SplittingField →+* E) : (a : f.SplittingField) → E)
        (Multiset.toFinset (roots (map (algebraMap F f.SplittingField) f))))
rw₅ :
  f.natSepDegree =
    Finset.card (α := f.SplittingField) (Multiset.toFinset (roots (map (algebraMap F f.SplittingField) f)))
⊢ f.natSepDegree = (f.aroots E).toFinset.card
have rw₆ : Finset.card (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) =
  Finset.card (α := f.SplittingField) (Multiset.toFinset (roots (map (algebraMap F f.SplittingField) f)))
Tactic: rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
inst_3 : DecidableEq E
h : Splits (map (algebraMap F E) f)
⊢ f.natSepDegree = (f.aroots E).toFinset.card
have rw : f.natSepDegree = (roots (map (algebraMap F E) f)).toFinset.card
Tactic: classical
  rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
inst_3 : DecidableEq E
h : Splits (map (algebraMap F E) f)
rw : f.natSepDegree = (roots (map (algebraMap F E) f)).toFinset.card
⊢ f.natSepDegree = (f.aroots E).toFinset.card
have rw₁ : f.natSepDegree =
  (roots
        (map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(SplittingField.lift f h) : f.SplittingField →+* E)
            (algebraMap F f.SplittingField))
          f)).toFinset.card
Tactic: classical
  rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]