-- 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
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
⊢ (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: 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)