awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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:
classical
  simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rfl

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]
h : f.Separable
⊢ f.natSepDegree = f.natDegree

Tactic:
(natSepDegree_eq_natDegree_iff f h.ne_zero).2 h

Premises used: Iff.mpr, Polynomial.natSepDegree_eq_natDegree_iff, Polynomial.Separable.ne_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
h : f.Separable
⊢ f.natSepDegree = f.natDegree

Tactic:
natSepDegree_eq_natDegree_of_separable f h

Premises used: Polynomial.natSepDegree_eq_natDegree_of_separable
-- Module: Mathlib.FieldTheory.SeparableDegree
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)))
rw₆ rw₇ :
  Finset.card (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) =
    Finset.card (α := f.SplittingField) (Multiset.toFinset (roots (map (algebraMap F f.SplittingField) f)))
⊢ f.natSepDegree = (f.aroots E).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]

Premises used: AlgHom.comp_algebraMap, Polynomial.SplittingField.lift, Polynomial.Splits.roots_map, Polynomial.SplittingField.splits, Finset.card_image_of_injective, RingHom.injective, Polynomial.natSepDegree, Polynomial.aroots, Multiset.toFinset_map, Polynomial.map_map
-- Module: Mathlib.FieldTheory.SeparableDegree
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)))
rw₆ rw₇ :
  Finset.card (α := f.SplittingField) (Multiset.toFinset (f.aroots f.SplittingField)) =
    Finset.card (α := f.SplittingField) (Multiset.toFinset (roots (map (algebraMap F f.SplittingField) f)))
⊢ f.natSepDegree = (f.aroots E).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]

Premises used: AlgHom.comp_algebraMap, Polynomial.SplittingField.lift, Polynomial.Splits.roots_map, Polynomial.SplittingField.splits, Finset.card_image_of_injective, RingHom.injective, Polynomial.natSepDegree, Polynomial.aroots, Multiset.toFinset_map, Polynomial.map_map
-- Module: Mathlib.FieldTheory.SeparableDegree
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
inst_4 : IsAlgClosed E
⊢ f.natSepDegree = (f.aroots E).toFinset.card

Tactic:
natSepDegree_eq_of_splits f (IsAlgClosed.splits _)

Premises used: IsAlgClosed.splits, Polynomial.natSepDegree_eq_of_splits
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
E : Type v
inst : Field E
K : Type w
inst_1 : Field K
f : E[X]
i : E →+* K
x : Algebra E K := i.toAlgebra
⊢ i = algebraMap E K

Tactic:
rfl
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
E : Type v
inst : Field E
K : Type w
inst_1 : Field K
f : E[X]
i : E →+* K
x : Algebra E K := i.toAlgebra
simp_rw : natSepDegree (map (algebraMap E K) f) = f.natSepDegree
simp_rw₁ :
  Finset.card (α := AlgebraicClosure K) (Multiset.toFinset (aroots (map (algebraMap E K) f) (AlgebraicClosure K))) =
    Finset.card.{w} (α := AlgebraicClosure K) (Multiset.toFinset (f.aroots (AlgebraicClosure K)))
simp_rw₂ :
  Finset.card (α := AlgebraicClosure K)
      (Multiset.toFinset (roots (map (algebraMap K (AlgebraicClosure K)) (map (algebraMap E K) f)))) =
    Finset.card.{w} (α := AlgebraicClosure K) (Multiset.toFinset (roots (map (algebraMap E (AlgebraicClosure K)) f)))
simp_rw₃ :
  Finset.card (α := AlgebraicClosure K)
      (Multiset.toFinset
        (roots
          (map
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (AlgebraicClosure K)) (algebraMap E K))
            f))) =
    Finset.card.{w} (α := AlgebraicClosure K) (Multiset.toFinset (roots (map (algebraMap E (AlgebraicClosure K)) f)))
⊢ (map i f).natSepDegree = f.natSepDegree

Tactic:
simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K),
    aroots_def, map_map, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, Polynomial.natSepDegree_eq_of_isAlgClosed, Polynomial.map_map, AlgebraicClosure, Polynomial.aroots_def
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
E : Type v
inst : Field E
K : Type w
inst_1 : Field K
f : E[X]
i : E →+* K
let let₁ let₂ : (map i f).natSepDegree = f.natSepDegree
⊢ (map i f).natSepDegree = f.natSepDegree

Tactic:
classical
  let _ := i.toAlgebra
  simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K),
    aroots_def, map_map, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, Polynomial.natSepDegree_eq_of_isAlgClosed, Polynomial.map_map, AlgebraicClosure, Polynomial.aroots_def
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
x : F
hx : x ≠ 0
⊢ (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) x : F[X]) f).natSepDegree = f.natSepDegree

Tactic:
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_C_mul _ hx]

Premises used: Polynomial.aroots_C_mul, Polynomial.natSepDegree_eq_of_isAlgClosed, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
x : F
hx : x ≠ 0
⊢ (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) x : F[X]) f).natSepDegree = f.natSepDegree

Tactic:
classical
  simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_C_mul _ hx]

Premises used: Polynomial.aroots_C_mul, Polynomial.natSepDegree_eq_of_isAlgClosed, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
x : F
hx : x ≠ 0
⊢ (x • f).natSepDegree = f.natSepDegree

Tactic:
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_smul_nonzero _ hx]

Premises used: Polynomial.aroots_smul_nonzero, Polynomial.natSepDegree_eq_of_isAlgClosed, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
x : F
hx : x ≠ 0
⊢ (x • f).natSepDegree = f.natSepDegree

Tactic:
classical
  simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_smul_nonzero _ hx]

Premises used: Polynomial.aroots_smul_nonzero, Polynomial.natSepDegree_eq_of_isAlgClosed, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
simp :
  (HSMul.hSMul (β := Multiset (AlgebraicClosure F)) n (f.aroots (AlgebraicClosure F))).toFinset.card =
    if n = 0 then 0 else Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))
⊢ (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree

Tactic:
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_pow]

Premises used: Polynomial.natSepDegree_eq_of_isAlgClosed, AlgebraicClosure, Polynomial.aroots_pow
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
pos :
  ∀ (h : n = 0),
    (HSMul.hSMul (β := Multiset (AlgebraicClosure F)) n (f.aroots (AlgebraicClosure F))).toFinset.card =
      if n = 0 then 0 else Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))
neg :
  ∀ (h : ¬n = 0),
    (HSMul.hSMul (β := Multiset (AlgebraicClosure F)) n (f.aroots (AlgebraicClosure F))).toFinset.card =
      if n = 0 then 0 else Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))
⊢ (HSMul.hSMul (β := Multiset (AlgebraicClosure F)) n (f.aroots (AlgebraicClosure F))).toFinset.card =
    if n = 0 then 0 else Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))

Tactic:
by_cases h : n = 0
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
h : n = 0
⊢ (HSMul.hSMul (β := Multiset (AlgebraicClosure F)) n (f.aroots (AlgebraicClosure F))).toFinset.card =
    if n = 0 then 0 else Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))

Tactic:
simp only [h, zero_smul, Multiset.toFinset_zero, Finset.card_empty, ite_true]

Premises used: ite_true, Multiset.toFinset_zero, zero_smul, Finset.card_empty
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
h : ¬n = 0
⊢ (HSMul.hSMul (β := Multiset (AlgebraicClosure F)) n (f.aroots (AlgebraicClosure F))).toFinset.card =
    if n = 0 then 0 else Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))

Tactic:
simp only [h, Multiset.toFinset_nsmul _ n h, ite_false]

Premises used: ite_false, Multiset.toFinset_nsmul
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
simp :
  (HSMul.hSMul (β := Multiset (AlgebraicClosure F)) n (f.aroots (AlgebraicClosure F))).toFinset.card =
    if n = 0 then 0 else Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))
pos :
  ∀ (h : n = 0),
    (HSMul.hSMul (β := Multiset (AlgebraicClosure F)) n (f.aroots (AlgebraicClosure F))).toFinset.card =
      if n = 0 then 0 else Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))
neg neg₁ :
  ∀ (h : ¬n = 0),
    (HSMul.hSMul (β := Multiset (AlgebraicClosure F)) n (f.aroots (AlgebraicClosure F))).toFinset.card =
      if n = 0 then 0 else Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))
⊢ (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree

Tactic:
classical
  simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_pow]
  by_cases h : n = 0
  · simp only [h, zero_smul, Multiset.toFinset_zero, Finset.card_empty, ite_true]
  simp only [h, Multiset.toFinset_nsmul _ n h, ite_false]

Premises used: ite_false, ite_true, Multiset.toFinset_zero, zero_smul, Finset.card_empty, Polynomial.natSepDegree_eq_of_isAlgClosed, AlgebraicClosure, Polynomial.aroots_pow
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
hn : n ≠ 0
simp_rw : (if n = 0 then 0 else f.natSepDegree) = f.natSepDegree
simp_rw₁ : (if False then 0 else f.natSepDegree) = f.natSepDegree
⊢ (f ^ n).natSepDegree = f.natSepDegree

Tactic:
simp_rw [natSepDegree_pow, hn, ite_false]

Premises used: Polynomial.natSepDegree_pow, ite_false
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
n : ℕ
⊢ (HPow.hPow (α := F[X]) X n).natSepDegree = if n = 0 then 0 else 1

Tactic:
simp only [natSepDegree_pow, natSepDegree_X]

Premises used: Polynomial.natSepDegree_pow, Polynomial.natSepDegree_X
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
x : F
n : ℕ
⊢ (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]) ^ n).natSepDegree = if n = 0 then 0 else 1

Tactic:
simp only [natSepDegree_pow, natSepDegree_X_sub_C]

Premises used: Polynomial.natSepDegree_pow, Polynomial.natSepDegree_X_sub_C
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
x y : F
n : ℕ
hx : x ≠ 0
⊢ (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) x : F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]) ^ n)).natSepDegree =
    if n = 0 then 0 else 1

Tactic:
simp only [natSepDegree_C_mul _ hx, natSepDegree_X_sub_C_pow]

Premises used: Polynomial.natSepDegree_X_sub_C_pow, Polynomial.natSepDegree_C_mul
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
pos : ∀ (h : f * g = 0), (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
neg : ∀ (h : ¬f * g = 0), (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
by_cases h : f * g = 0
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
simp only [h, natSepDegree_zero, zero_le]

Premises used: zero_le, Polynomial.natSepDegree_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f * g = 0
neg :
  Finset.card (α := AlgebraicClosure F)
      (Multiset.toFinset (f.aroots (AlgebraicClosure F)) ∪ Multiset.toFinset (g.aroots (AlgebraicClosure F))) ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) +
      Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]

Premises used: Multiset.toFinset_add, Polynomial.natSepDegree_eq_of_isAlgClosed, Polynomial.aroots_mul, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f * g = 0
⊢ Finset.card (α := AlgebraicClosure F)
      (Multiset.toFinset (f.aroots (AlgebraicClosure F)) ∪ Multiset.toFinset (g.aroots (AlgebraicClosure F))) ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) +
      Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))

Tactic:
Finset.card_union_le _ _

Premises used: Finset.card_union_le
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f * g = 0
⊢ Finset.card (α := AlgebraicClosure F)
      (Multiset.toFinset (f.aroots (AlgebraicClosure F)) ∪ Multiset.toFinset (g.aroots (AlgebraicClosure F))) ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) +
      Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))

Tactic:
exact Finset.card_union_le _ _

Premises used: Finset.card_union_le
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f * g = 0
neg :
  Finset.card (α := AlgebraicClosure F) (Multiset.toFinset ((f * g).aroots (AlgebraicClosure F))) ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) +
      Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))
neg₁ :
  (HAdd.hAdd (α := Multiset (AlgebraicClosure F)) (f.aroots (AlgebraicClosure F))
          (g.aroots (AlgebraicClosure F))).toFinset.card ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) +
      Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))
neg₂ :
  Finset.card (α := AlgebraicClosure F)
      (Multiset.toFinset (f.aroots (AlgebraicClosure F)) ∪ Multiset.toFinset (g.aroots (AlgebraicClosure F))) ≤
    Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) +
      Finset.card (α := AlgebraicClosure F) (Multiset.toFinset (g.aroots (AlgebraicClosure F)))
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
  exact Finset.card_union_le _ _

Premises used: Multiset.toFinset_add, Finset.card_union_le, Polynomial.natSepDegree_eq_of_isAlgClosed, Polynomial.aroots_mul, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
pos : ∀ (h : f * g = 0), (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
neg : ∀ (h : ¬f * g = 0), (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
by_cases h : f * g = 0
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : f * g = 0
⊢ f = 0 ∨ g = 0

Tactic:
rw [mul_eq_zero] at h

Premises used: mul_eq_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : f = 0 ∨ g = 0
pos :
  ∀
    (this :
      ∀ (f g : F[X]) (h : f = 0 ∨ g = 0) (hf : f = 0),
        (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g)
    (hf : ¬f = 0), (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
wlog :
  ∀ (f g : F[X]) (h : f = 0 ∨ g = 0) (hf : f = 0),
    (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
wlog hf : f = 0 generalizing f g
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f g : F[X]
h : f = 0 ∨ g = 0
this :
  ∀ (f g : F[X]) (h : f = 0 ∨ g = 0) (hf : f = 0),
    (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
hf : ¬f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
simpa only [mul_comm, add_comm, and_comm,
        isCoprime_comm] using this g f h.symm (h.resolve_left hf)

Premises used: isCoprime_comm, Or.resolve_left, and_comm, add_comm, Or.symm, mul_comm
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
rw :
  (∃ (x : F), (C : (a : F) → F[X]) x = g) ↔
    Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
rw [hf, zero_mul, natSepDegree_zero, zero_add, isCoprime_zero_left, isUnit_iff, eq_comm,
      natSepDegree_eq_zero_iff, natDegree_eq_zero]

Premises used: Polynomial.natSepDegree_eq_zero_iff, MulZeroClass.zero_mul, Polynomial.isUnit_iff, Polynomial.natSepDegree_zero, isCoprime_zero_left, eq_comm, zero_add, Polynomial.natDegree_eq_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (∃ (x : F), (C : (a : F) → F[X]) x = g) ↔
    Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g

Tactic:
⟨fun ⟨x, h⟩ ↦ ?_, ?_⟩

Premises used: Polynomial.C, _private.0.Polynomial.natSepDegree_mul_eq_iff.match_2, IsUnit, Exists, And, Iff.intro, Or, OfNat.ofNat, Eq, DFunLike.coe
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
refine_1 :
  (∃ (x : F), (C : (a : F) → F[X]) x = g) →
    ∀ (x : F) (h : (C : (a : F) → F[X]) x = g),
      Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g
refine_2 :
  (Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g) →
    ∃ (x : F), (C : (a : F) → F[X]) x = g
⊢ (∃ (x : F), (C : (a : F) → F[X]) x = g) ↔
    Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g

Tactic:
refine ⟨fun ⟨x, h⟩ ↦ ?_, ?_⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
h_2 : ∃ (x : F), (C : (a : F) → F[X]) x = g
x : F
h : (C : (a : F) → F[X]) x = g
pos : ∀ (hx : x = 0), Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g
neg : ∀ (hx : ¬x = 0), Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g
⊢ Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
h_2 : ∃ (x : F), (C : (a : F) → F[X]) x = g
x : F
h : (C : (a : F) → F[X]) x = g
hx : x = 0
rw : Eq (α := F[X]) ((C : (a : F) → F[X]) x : F[X]) (0 : F[X])
rw₁ : Eq.{u + 1} (α := F[X]) ((C : (a : F) → F[X]) 0) 0
rw₂ rw₃ : Eq.{u + 1} (α := F[X]) 0 0
⊢ g = 0

Tactic:
rw [← h, hx, map_zero]

Premises used: map_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
h_2 : ∃ (x : F), (C : (a : F) → F[X]) x = g
x : F
h : (C : (a : F) → F[X]) x = g
hx : x = 0
⊢ Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g

Tactic:
exact .inl ⟨rfl, by rw [← h, hx, map_zero]⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
h_2 : ∃ (x : F), (C : (a : F) → F[X]) x = g
x : F
h : (C : (a : F) → F[X]) x = g
hx : ¬x = 0
⊢ Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g

Tactic:
.inr ⟨x, Ne.isUnit hx, h⟩

Premises used: Ne.isUnit, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
h_2 : ∃ (x : F), (C : (a : F) → F[X]) x = g
x : F
h : (C : (a : F) → F[X]) x = g
hx : ¬x = 0
⊢ Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g

Tactic:
exact .inr ⟨x, Ne.isUnit hx, h⟩