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
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: 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
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: 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
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: 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
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: 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
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: 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:
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
⊢ (map i f).natSepDegree = f.natSepDegree
have simp_rw : natSepDegree (map (algebraMap E K) f) = 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]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ (map i f).natSepDegree = f.natSepDegree
have 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)))
Tactic: simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K),
    aroots_def, map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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)))
⊢ (map i f).natSepDegree = f.natSepDegree
have 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)))
Tactic: simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K),
    aroots_def, map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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)))
⊢ (map i f).natSepDegree = f.natSepDegree
have 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)))
Tactic: simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K),
    aroots_def, map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
⊢ (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree
have 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)))
Tactic: simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
⊢ (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)))
have 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)))
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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)))
⊢ (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)))
have 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)))
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
⊢ (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree
have 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)))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
have 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)))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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)))
⊢ (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree
have 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)))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
n : ℕ
hn : n ≠ 0
⊢ (f ^ n).natSepDegree = f.natSepDegree
have simp_rw : (if n = 0 then 0 else f.natSepDegree) = f.natSepDegree
Tactic: simp_rw [natSepDegree_pow, hn, ite_false]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ (f ^ n).natSepDegree = f.natSepDegree
have simp_rw₁ : (if False then 0 else f.natSepDegree) = f.natSepDegree
Tactic: simp_rw [natSepDegree_pow, hn, ite_false]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
have pos : ∀ (h : f * g = 0), (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
Tactic: by_cases h : f * g = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
pos : ∀ (h : f * g = 0), (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
have neg : ∀ (h : ¬f * g = 0), (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
Tactic: by_cases h : f * g = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
have 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)))
Tactic: simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
have 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)))
Tactic: classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
  exact Finset.card_union_le _ _
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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)))
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
have 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)))
Tactic: classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
  exact Finset.card_union_le _ _
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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)))
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
have 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)))
Tactic: classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
  exact Finset.card_union_le _ _
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
have pos : ∀ (h : f * g = 0), (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
Tactic: by_cases h : f * g = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
have neg : ∀ (h : ¬f * g = 0), (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
Tactic: by_cases h : f * g = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
have h₁ : f = 0 ∨ g = 0
Tactic: rw [mul_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
h : f = 0 ∨ g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
have 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
Tactic: wlog hf : f = 0 generalizing f g
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
have 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
Tactic: wlog hf : f = 0 generalizing f g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f_1 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
have 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
Tactic: rw [hf, zero_mul, natSepDegree_zero, zero_add, isCoprime_zero_left, isUnit_iff, eq_comm,
      natSepDegree_eq_zero_iff, natDegree_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
have 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
Tactic: refine ⟨fun ⟨x, h⟩ ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ (∃ (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
have 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
Tactic: refine ⟨fun ⟨x, h⟩ ↦ ?_, ?_⟩