awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g
have pos : ∀ (hx : x = 0), 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
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ Eq.{u + 1} (α := F[X]) 0 0 ∧ g = 0 ∨ ∃ (r : F), IsUnit r ∧ (C : (a : F) → F[X]) r = g
have neg : ∀ (hx : ¬x = 0), 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
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ g = 0
have rw : Eq (α := F[X]) ((C : (a : F) → F[X]) x : F[X]) (0 : F[X])
Tactic: rw [← h, hx, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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])
⊢ g = 0
have rw₁ : Eq.{u + 1} (α := F[X]) ((C : (a : F) → F[X]) 0) 0
Tactic: rw [← h, hx, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ g = 0
have rw₂ : Eq.{u + 1} (α := F[X]) 0 0
Tactic: rw [← h, hx, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
h : g = 0
⊢ (C : (a : F) → F[X]) 0 = g
have rw : Eq.{u + 1} (α := F[X]) ((C : (a : F) → F[X]) 0) 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f_1 f g : F[X]
h_1 : f = 0 ∨ g = 0
hf : f = 0
h : g = 0
rw : Eq.{u + 1} (α := F[X]) ((C : (a : F) → F[X]) 0) 0
⊢ (C : (a : F) → F[X]) 0 = g
have rw₁ : Eq.{u + 1} (α := F[X]) 0 0
Tactic: rw [h, map_zero]
-- 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 ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
have neg : (∀ (a : AlgebraicClosure F),
    f ≠ 0 ∧
        Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
          (0 : AlgebraicClosure F) →
      ∀ (b : AlgebraicClosure F),
        g ≠ 0 ∧
            Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
              (0 : AlgebraicClosure F) →
          a ≠ b) ↔
  f = 0 ∧ g = 0 ∨ IsCoprime f g
Tactic: simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
    Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
inst : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (∀ (a : AlgebraicClosure F),
      f ≠ 0 ∧
          Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
            (0 : AlgebraicClosure F) →
        ∀ (b : AlgebraicClosure F),
          g ≠ 0 ∧
              Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                (0 : AlgebraicClosure F) →
            a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
have h₁ : ¬f = 0 ∧ ¬g = 0
Tactic: rw [mul_eq_zero, not_or] 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
⊢ (∀ (a : AlgebraicClosure F),
      f ≠ 0 ∧
          Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
            (0 : AlgebraicClosure F) →
        ∀ (b : AlgebraicClosure F),
          g ≠ 0 ∧
              Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                (0 : AlgebraicClosure F) →
            a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
have neg : ∀
  (H :
    ∀ (a : AlgebraicClosure F),
      f ≠ 0 ∧
          Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
            (0 : AlgebraicClosure F) →
        ∀ (b : AlgebraicClosure F),
          g ≠ 0 ∧
              Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                (0 : AlgebraicClosure F) →
            a ≠ b)
  (u : F[X]) (hu : Irreducible u), u ∣ f → u ∣ g → ∀ (v : F[X]) (hf : f = u * v) (w : F[X]) (hg : g = u * w), False
Tactic: refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
-- 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
neg :
  ∀
    (H :
      ∀ (a : AlgebraicClosure F),
        f ≠ 0 ∧
            Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
              (0 : AlgebraicClosure F) →
          ∀ (b : AlgebraicClosure F),
            g ≠ 0 ∧
                Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                  (0 : AlgebraicClosure F) →
              a ≠ b)
    (u : F[X]) (hu : Irreducible u), u ∣ f → u ∣ g → ∀ (v : F[X]) (hf : f = u * v) (w : F[X]) (hg : g = u * w), False
⊢ (∀ (a : AlgebraicClosure F),
      f ≠ 0 ∧
          Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
            (0 : AlgebraicClosure F) →
        ∀ (b : AlgebraicClosure F),
          g ≠ 0 ∧
              Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
                (0 : AlgebraicClosure F) →
            a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
have neg₁ : f = 0 ∧ g = 0 ∨ IsCoprime f g →
  ∀ (a : AlgebraicClosure F),
    f ≠ 0 ∧
        Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
          (0 : AlgebraicClosure F) →
      ∀ (b : AlgebraicClosure F),
        g ≠ 0 ∧
            Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
              (0 : AlgebraicClosure F) →
          a ≠ b
Tactic: refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
-- 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
H :
  ∀ (a : AlgebraicClosure F),
    f ≠ 0 ∧
        Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
          (0 : AlgebraicClosure F) →
      ∀ (b : AlgebraicClosure F),
        g ≠ 0 ∧
            Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
              (0 : AlgebraicClosure F) →
          a ≠ b
u : F[X]
hu : Irreducible u
h_1 : u ∣ f
h_2 : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
⊢ False
have neg : ∀ (x : AlgebraicClosure F)
  (hx :
    Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) u : AlgebraicClosure F)
      (0 : AlgebraicClosure F)),
  False
Tactic: obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
-- 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
hc : IsCoprime f g
x : AlgebraicClosure F
hf :
  f ≠ 0 ∧
    Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) f : AlgebraicClosure F)
      (0 : AlgebraicClosure F)
hg :
  g ≠ 0 ∧
    Eq (α := AlgebraicClosure F) ((aeval x : (a : F[X]) → AlgebraicClosure F) g : AlgebraicClosure F)
      (0 : AlgebraicClosure F)
⊢ False
have neg : ∀ (u v : F[X]) (hfg : u * f + v * g = 1), False
Tactic: obtain ⟨u, v, hfg⟩ := hc
Cleared hypotheses: hc
-- 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 ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
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))) ↔
  f = 0 ∧ g = 0 ∨ IsCoprime f g
Tactic: classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
    Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]
  rw [mul_eq_zero, not_or] at h
  refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
  · obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
    exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
      x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl
  rintro (⟨rfl, rfl⟩ | hc)
  · exact (h.1 rfl).elim
  rintro x hf _ hg rfl
  obtain ⟨u, v, hfg⟩ := hc
  simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
    zero_ne_one] using congr(aeval x $hfg)
-- 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 = 0 ∧ g = 0 ∨ IsCoprime f g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
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))) ↔
  f = 0 ∧ g = 0 ∨ IsCoprime f g
Tactic: classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
    Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]
  rw [mul_eq_zero, not_or] at h
  refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
  · obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
    exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
      x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl
  rintro (⟨rfl, rfl⟩ | hc)
  · exact (h.1 rfl).elim
  rintro x hf _ hg rfl
  obtain ⟨u, v, hfg⟩ := hc
  simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
    zero_ne_one] using congr(aeval x $hfg)
-- 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 = 0 ∧ g = 0 ∨ IsCoprime f g
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 = 0 ∧ g = 0 ∨ IsCoprime f g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
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))) ↔
  f = 0 ∧ g = 0 ∨ IsCoprime f g
Tactic: classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
    Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]
  rw [mul_eq_zero, not_or] at h
  refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
  · obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
    exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
      x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl
  rintro (⟨rfl, rfl⟩ | hc)
  · exact (h.1 rfl).elim
  rintro x hf _ hg rfl
  obtain ⟨u, v, hfg⟩ := hc
  simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
    zero_ne_one] using congr(aeval x $hfg)
-- 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 = 0 ∧ g = 0 ∨ IsCoprime f g
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 = 0 ∧ g = 0 ∨ IsCoprime f g
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 = 0 ∧ g = 0 ∨ IsCoprime f g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
have neg₃ : Disjoint (α := Finset (AlgebraicClosure F)) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))
    (Multiset.toFinset (g.aroots (AlgebraicClosure F))) ↔
  f = 0 ∧ g = 0 ∨ IsCoprime f g
Tactic: classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
    Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]
  rw [mul_eq_zero, not_or] at h
  refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
  · obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
    exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
      x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl
  rintro (⟨rfl, rfl⟩ | hc)
  · exact (h.1 rfl).elim
  rintro x hf _ hg rfl
  obtain ⟨u, v, hfg⟩ := hc
  simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
    zero_ne_one] using congr(aeval x $hfg)
-- 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 = 0 ∧ g = 0 ∨ IsCoprime f g
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 = 0 ∧ g = 0 ∨ IsCoprime f g
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 = 0 ∧ g = 0 ∨ IsCoprime f g
neg₃ :
  Disjoint (α := Finset (AlgebraicClosure F)) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))
      (Multiset.toFinset (g.aroots (AlgebraicClosure F))) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
have neg₄ : (∀ (a : AlgebraicClosure F),
    Membership.mem (γ := Finset (AlgebraicClosure F)) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) a →
      ∀ (b : AlgebraicClosure F),
        Membership.mem (γ := Finset (AlgebraicClosure F)) (Multiset.toFinset (g.aroots (AlgebraicClosure F))) b →
          a ≠ b) ↔
  f = 0 ∧ g = 0 ∨ IsCoprime f g
Tactic: classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
    Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]
  rw [mul_eq_zero, not_or] at h
  refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
  · obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
    exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
      x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl
  rintro (⟨rfl, rfl⟩ | hc)
  · exact (h.1 rfl).elim
  rintro x hf _ hg rfl
  obtain ⟨u, v, hfg⟩ := hc
  simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
    zero_ne_one] using congr(aeval x $hfg)
-- 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 = 0 ∧ g = 0 ∨ IsCoprime f g
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 = 0 ∧ g = 0 ∨ IsCoprime f g
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 = 0 ∧ g = 0 ∨ IsCoprime f g
neg₃ :
  Disjoint (α := Finset (AlgebraicClosure F)) (Multiset.toFinset (f.aroots (AlgebraicClosure F)))
      (Multiset.toFinset (g.aroots (AlgebraicClosure F))) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
neg₄ :
  (∀ (a : AlgebraicClosure F),
      Membership.mem (γ := Finset (AlgebraicClosure F)) (Multiset.toFinset (f.aroots (AlgebraicClosure F))) a →
        ∀ (b : AlgebraicClosure F),
          Membership.mem (γ := Finset (AlgebraicClosure F)) (Multiset.toFinset (g.aroots (AlgebraicClosure F))) b →
            a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
have neg₅ : (∀ (a : AlgebraicClosure F),
    Membership.mem (γ := Multiset (AlgebraicClosure F)) (f.aroots (AlgebraicClosure F)) a →
      ∀ (b : AlgebraicClosure F),
        Membership.mem (γ := Multiset (AlgebraicClosure F)) (g.aroots (AlgebraicClosure F)) b → a ≠ b) ↔
  f = 0 ∧ g = 0 ∨ IsCoprime f g
Tactic: classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add,
    Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, Multiset.mem_toFinset, mem_aroots]
  rw [mul_eq_zero, not_or] at h
  refine ⟨fun H ↦ .inr (isCoprime_of_irreducible_dvd (not_and.2 fun _ ↦ h.2)
    fun u hu ⟨v, hf⟩ ⟨w, hg⟩ ↦ ?_), ?_⟩
  · obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
    exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
      x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl
  rintro (⟨rfl, rfl⟩ | hc)
  · exact (h.1 rfl).elim
  rintro x hf _ hg rfl
  obtain ⟨u, v, hfg⟩ := hc
  simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
    zero_ne_one] using congr(aeval x $hfg)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ f.natSepDegree ≤ g.natSepDegree
have simp_rw : 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)]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ f.natSepDegree ≤ g.natSepDegree
have simp_rw : 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)]
  exact Finset.card_le_card <| Multiset.toFinset_subset.mpr <|
    Multiset.Le.subset <| roots.le_of_dvd (map_ne_zero h2) <| map_dvd _ h1
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
hF : ExpChar F q
n : ℕ
⊢ natSepDegree.{u} (F := F) ((expand F (q ^ n) : (a : F[X]) → F[X]) f) = f.natSepDegree
have zero : ∀ [CharZero F], natSepDegree.{u} (F := F) ((expand F (HPow.hPow (α := ℕ) 1 n) : (a : F[X]) → F[X]) f) = f.natSepDegree
Tactic: obtain - | hprime := hF
Cleared hypotheses: q, hF