awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableDegree
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
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed K
⊢ finSepDegree F E = Nat.card (E →ₐ[F] K)

Tactic:
Nat.card_congr (embEquivOfIsAlgClosed F E K)

Premises used: Field.finSepDegree, Nat.card_congr, Field.embEquivOfIsAlgClosed
-- Module: Mathlib.FieldTheory.SeparableDegree
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
obtain : ∀ (ι : Type v) (x : ι → E) (hx : IsTranscendenceBasis F x), Infinite.{v + 1} (Emb F E)
⊢ Infinite.{v + 1} (Emb F E)

Tactic:
obtain ⟨ι, x, hx⟩ := exists_isTranscendenceBasis' F E

Premises used: exists_isTranscendenceBasis'
-- Module: Mathlib.FieldTheory.SeparableDegree
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
⊢ Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E

Tactic:
have := hx.isAlgebraic_field
-- Module: Mathlib.FieldTheory.SeparableDegree
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
rw : Infinite.{v + 1} (Emb F ↥(adjoin F (Set.range x)) × Emb (↥(adjoin F (Set.range x))) E)
⊢ Infinite.{v + 1} (Emb F E)

Tactic:
rw [← (embProdEmbOfIsAlgebraic F (adjoin F (Set.range x)) E).infinite_iff]

Premises used: Field.embProdEmbOfIsAlgebraic, Membership.mem, Subtype, IntermediateField.adjoin, Equiv.infinite_iff, Set.range
-- Module: Mathlib.FieldTheory.SeparableDegree
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)

Tactic:
@Prod.infinite_of_left _ _ ?_ _

Premises used: Prod.infinite_of_left
-- Module: Mathlib.FieldTheory.SeparableDegree
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
refine : Infinite.{v + 1} (Emb F ↥(adjoin F (Set.range x)))
⊢ Infinite.{v + 1} (Emb F ↥(adjoin F (Set.range x)) × Emb (↥(adjoin F (Set.range x))) E)

Tactic:
refine @Prod.infinite_of_left _ _ ?_ _

Premises used: Prod.infinite_of_left
-- Module: Mathlib.FieldTheory.SeparableDegree
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
rw : Infinite (Emb F (FractionRing (MvPolynomial ι F)))
⊢ Infinite.{v + 1} (Emb F ↥(adjoin F (Set.range x)))

Tactic:
rw [← (embEquivOfEquiv _ _ _ hx.1.aevalEquivField).infinite_iff]

Premises used: AlgebraicIndependent.aevalEquivField, Field.embEquivOfEquiv, And.left, Equiv.infinite_iff
-- Module: Mathlib.FieldTheory.SeparableDegree
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
obtain : ∀ (i : ι), Infinite (Emb F (FractionRing (MvPolynomial ι F)))
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))

Tactic:
obtain ⟨i⟩ := hx.nonempty_iff_transcendental.2 H

Premises used: Iff.mpr, IsTranscendenceBasis.nonempty_iff_transcendental
-- Module: Mathlib.FieldTheory.SeparableDegree
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)
rw :
  Function.Injective (α := MvPolynomial ι F) (β := AlgebraicClosure K)
    (⇑(RingHom.comp (algebraMap K (AlgebraicClosure K)) (algebraMap (MvPolynomial ι F) K)) :
      (a : MvPolynomial ι F) → AlgebraicClosure K)
⊢ Function.Injective (α := MvPolynomial ι F) (β := AlgebraicClosure K)
    (⇑i1 : (a : MvPolynomial ι F) → AlgebraicClosure K)

Tactic:
rw [IsScalarTower.coe_toAlgHom', IsScalarTower.algebraMap_eq _ K]

Premises used: IsScalarTower.coe_toAlgHom', IsScalarTower.algebraMap_eq
-- Module: Mathlib.FieldTheory.SeparableDegree
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)
    (⇑(RingHom.comp (algebraMap K (AlgebraicClosure K)) (algebraMap (MvPolynomial ι F) K)) :
      (a : MvPolynomial ι F) → AlgebraicClosure K)

Tactic:
(algebraMap K (AlgebraicClosure K)).injective.comp (IsFractionRing.injective _ _)

Premises used: Algebra.algebraMap, IsFractionRing.injective, Submodule.Quotient.mk, RingHom.injective, Function.Injective.comp, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
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)
    (⇑(RingHom.comp (algebraMap K (AlgebraicClosure K)) (algebraMap (MvPolynomial ι F) K)) :
      (a : MvPolynomial ι F) → AlgebraicClosure K)

Tactic:
exact (algebraMap K (AlgebraicClosure K)).injective.comp (IsFractionRing.injective _ _)

Premises used: Algebra.algebraMap, IsFractionRing.injective, RingHom.injective, Function.Injective.comp, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
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)

Tactic:
have hi1 : Function.Injective i1 := by
    rw [IsScalarTower.coe_toAlgHom', IsScalarTower.algebraMap_eq _ K]
    exact (algebraMap K (AlgebraicClosure K)).injective.comp (IsFractionRing.injective _ _)
-- Module: Mathlib.FieldTheory.SeparableDegree
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)
n : ℕ
⊢ Function.Injective (α := MvPolynomial ι F) (β := MvPolynomial ι F)
    (⇑(↑(MvPolynomial.aeval fun (i : ι) ↦ HPow.hPow (α := MvPolynomial ι F) (MvPolynomial.X i) (n + 1)) :
          MvPolynomial ι F →+* MvPolynomial ι F) :
      (a : MvPolynomial ι F) → MvPolynomial ι F)

Tactic:
simpa [algebraicIndependent_iff_injective_aeval] using
        MvPolynomial.algebraicIndependent_polynomial_aeval_X _
          fun i : ι ↦ (Polynomial.transcendental_X F).pow n.succ_pos

Premises used: MvPolynomial.algebraicIndependent_polynomial_aeval_X, Polynomial.transcendental_X, algebraicIndependent_iff_injective_aeval, Nat.succ_pos, Transcendental.pow
-- Module: Mathlib.FieldTheory.SeparableDegree
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)))

Tactic:
Infinite.of_injective f fun m n h ↦ ?_

Premises used: Infinite.of_injective
-- Module: Mathlib.FieldTheory.SeparableDegree
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))) ⋯
refine : ∀ (m n : ℕ) (h : f m = f n), m = n
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))

Tactic:
refine Infinite.of_injective f fun m n h ↦ ?_

Premises used: Infinite.of_injective
-- Module: Mathlib.FieldTheory.SeparableDegree
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
⊢ Eq (α := AlgebraicClosure K)
    ((i1 : (a : MvPolynomial ι F) → AlgebraicClosure K) (HPow.hPow (α := MvPolynomial ι F) (MvPolynomial.X i) (m + 1)) :
      AlgebraicClosure K)
    ((i1 : (a : MvPolynomial ι F) → AlgebraicClosure K) (HPow.hPow (α := MvPolynomial ι F) (MvPolynomial.X i) (n + 1)) :
      AlgebraicClosure K)

Tactic:
simpa [f, -map_pow] using congr($h (algebraMap _ K (MvPolynomial.X (R := F) i)))

Premises used: map_pow
-- Module: Mathlib.FieldTheory.SeparableDegree
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
⊢ 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)))
-- Module: Mathlib.FieldTheory.SeparableDegree
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 :
  HPow.hPow (α := MvPolynomial ι F) (MvPolynomial.X i) (m + 1) =
    HPow.hPow (α := MvPolynomial ι F) (MvPolynomial.X i) (n + 1)
⊢ m = n

Tactic:
simpa using congr(MvPolynomial.totalDegree $h)
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.Transcendental F E
⊢ finSepDegree F E = 0

Tactic:
Nat.card_eq_zero_of_infinite

Premises used: Nat.card_eq_zero_of_infinite, Field.finSepDegree
-- Module: Mathlib.FieldTheory.SeparableDegree
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic E K
⊢ finSepDegree F E * finSepDegree E K = finSepDegree F K

Tactic:
simpa only [Nat.card_prod] using Nat.card_congr (embProdEmbOfIsAlgebraic F E K)

Premises used: Field.embProdEmbOfIsAlgebraic, Nat.card_congr, Nat.card_prod
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
⊢ 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'
-- Module: Mathlib.FieldTheory.SeparableDegree
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)
⊢ Multiset.card (α := f.SplittingField) (f.aroots f.SplittingField) ≤ f.natDegree

Tactic:
rw [← aroots_def, natDegree_map] at this

Premises used: Polynomial.natDegree_map, Polynomial.aroots_def
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
this : Multiset.card (α := f.SplittingField) (f.aroots f.SplittingField) ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
(f.aroots f.SplittingField).toFinset_card_le.trans this

Premises used: Multiset.toFinset_card_le, Polynomial.SplittingField, Polynomial.natSepDegree, Polynomial.aroots, LE.le.trans
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
this : Multiset.card (α := f.SplittingField) (f.aroots f.SplittingField) ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
exact (f.aroots f.SplittingField).toFinset_card_le.trans this

Premises used: Multiset.toFinset_card_le, Polynomial.SplittingField, Polynomial.aroots, LE.le.trans
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
this : Multiset.card (α := f.SplittingField) (f.aroots f.SplittingField) ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
classical
  exact (f.aroots f.SplittingField).toFinset_card_le.trans this
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
x : F
⊢ (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])).natSepDegree = 1

Tactic:
simp only [natSepDegree, aroots_X_sub_C, Multiset.toFinset_singleton, Finset.card_singleton]

Premises used: Polynomial.aroots_X_sub_C, Polynomial.natSepDegree, Multiset.toFinset_singleton, Finset.card_singleton
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
⊢ natSepDegree.{u} (F := F) X = 1

Tactic:
simp only [natSepDegree, aroots_X, Multiset.toFinset_singleton, Finset.card_singleton]

Premises used: Polynomial.aroots_X, Polynomial.natSepDegree, Multiset.toFinset_singleton, Finset.card_singleton
-- Module: Mathlib.FieldTheory.SeparableDegree
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
linarith₁ :
  0 < f.natSepDegree →
    -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑f.natSepDegree : ℤ)) +
          HSub.hSub (α := ℤ) (↑f.natSepDegree : ℤ) (↑f.natDegree : ℤ) +
        HSub.hSub (α := ℤ) (↑f.natDegree : ℤ) 0 =
      0
⊢ f.natSepDegree = 0

Tactic:
linarith only [natSepDegree_le_natDegree f, h]

Premises used: Polynomial.natSepDegree_le_natDegree
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
x : F
⊢ natSepDegree.{u} (F := F) ((C : (a : F) → F[X]) x) = 0

Tactic:
natSepDegree_eq_zero _ (natDegree_C _)

Premises used: Polynomial.natSepDegree_eq_zero, Polynomial.natDegree_C
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
rw : natSepDegree.{u} (F := F) ((C : (a : F) → F[X]) 0) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ natSepDegree.{u} (F := F) 0 = 0

Tactic:
rw [← C_0, natSepDegree_C]

Premises used: Polynomial.C_0, Polynomial.natSepDegree_C
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
rw : natSepDegree.{u} (F := F) ((C : (a : F) → F[X]) 1) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ natSepDegree.{u} (F := F) 1 = 0

Tactic:
rw [← C_1, natSepDegree_C]

Premises used: Polynomial.C_1, Polynomial.natSepDegree_C
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
rw : Finset.Nonempty (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField))
⊢ f.natSepDegree ≠ 0

Tactic:
rw [natSepDegree, ne_eq, Finset.card_eq_zero, ← ne_eq, ← Finset.nonempty_iff_ne_empty]

Premises used: Finset.nonempty_iff_ne_empty, ne_eq, Polynomial.natSepDegree, Finset.card_eq_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
rwa rwa₁ rwa₂ rwa₃ : f.natDegree ≠ Zero.zero
⊢ natDegree (R := f.SplittingField) (map (algebraMap F f.SplittingField) f) ≠ Zero.zero

Tactic:
rwa [natDegree_map]

Premises used: Polynomial.natDegree_map
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
h₁ : Membership.mem (γ := Finset f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) (rootOfSplits ⋯ ⋯)
⊢ Finset.Nonempty (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField))

Tactic:
use rootOfSplits (SplittingField.splits f) (degree_ne_of_natDegree_ne (by rwa [natDegree_map]))

Premises used: Polynomial.degree_ne_of_natDegree_ne, Polynomial.SplittingField.splits, Polynomial.rootOfSplits
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
h₁ : f ≠ 0 ∧ Eq (α := f.SplittingField) ((aeval (rootOfSplits ⋯ ⋯) : (a : F[X]) → f.SplittingField) f) 0
⊢ Membership.mem (γ := Finset f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) (rootOfSplits ⋯ ⋯)

Tactic:
rw [Multiset.mem_toFinset, mem_aroots]

Premises used: Polynomial.mem_aroots, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ Eq (α := f.SplittingField) ((aeval (rootOfSplits ⋯ ⋯) : (a : F[X]) → f.SplittingField) f) 0

Tactic:
simp only [← eval_map_algebraMap, eval_rootOfSplits]

Premises used: Polynomial.eval_map_algebraMap, Polynomial.eval_rootOfSplits
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f ≠ 0 ∧ Eq (α := f.SplittingField) ((aeval (rootOfSplits ⋯ ⋯) : (a : F[X]) → f.SplittingField) f) 0

Tactic:
exact ⟨ne_of_apply_ne _ h, by simp only [← eval_map_algebraMap, eval_rootOfSplits]⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
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 ⋯ ⋯)
h₂ h₃ h₄ : f ≠ 0 ∧ Eq (α := f.SplittingField) ((aeval (rootOfSplits ⋯ ⋯) : (a : F[X]) → f.SplittingField) f) 0
⊢ Membership.mem (γ := Finset f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) (rootOfSplits ⋯ ⋯)

Tactic:
classical
  rw [Multiset.mem_toFinset, mem_aroots]
  exact ⟨ne_of_apply_ne _ h, by simp only [← eval_map_algebraMap, eval_rootOfSplits]⟩

Premises used: Polynomial.mem_aroots, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
⊢ f.natSepDegree = 0 ↔ f.natDegree = 0

Tactic:
⟨(natSepDegree_ne_zero f).mtr, natSepDegree_eq_zero f⟩

Premises used: Polynomial.natSepDegree_eq_zero, Polynomial.natSepDegree_ne_zero, Function.mtr, Iff.intro
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
⊢ f.natSepDegree ≠ 0 ↔ f.natDegree ≠ 0

Tactic:
Iff.not <| natSepDegree_eq_zero_iff f

Premises used: Polynomial.natSepDegree_eq_zero_iff, Iff.not
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
simp_rw :
  f.natSepDegree = f.natDegree ↔
    Finset.card (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) = f.natDegree
⊢ f.natSepDegree = f.natDegree ↔ f.Separable

Tactic:
simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]

Premises used: Finset.coe_sort_coe, Polynomial.card_rootSet_eq_natDegree_iff_of_splits, Polynomial.SplittingField.splits, Polynomial.rootSet_def, Fintype.card_coe
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔
    Finset.card (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) = f.natDegree

Tactic:
rfl