-- 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))) ↔
    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
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
neg₇ :
  ∀ (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
neg₈ :
  ∀ (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), u ∣ f → u ∣ g → ∀ (v : F[X]) (hf : f = u * v) (w : F[X]) (hg : g = u * w), False
neg₉ neg₁₀ :
  ∀ (h : ¬f = 0 ∧ ¬g = 0),
    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
neg₁₁ :
  ∀ (h : ¬Eq.{u + 1} (α := F[X]) 0 0 ∧ ¬Eq.{u + 1} (α := F[X]) 0 0) (a : AlgebraicClosure F),
    Ne.{u + 1} (α := F[X]) 0 0 ∧ Eq (α := AlgebraicClosure F) ((aeval a : (a : F[X]) → AlgebraicClosure F) 0) 0 →
      ∀ (b : AlgebraicClosure F),
        Ne.{u + 1} (α := F[X]) 0 0 ∧ Eq (α := AlgebraicClosure F) ((aeval b : (a : F[X]) → AlgebraicClosure F) 0) 0 →
          a ≠ b
neg₁₂ neg₁₃ :
  ∀ (h : ¬f = 0 ∧ ¬g = 0) (hc : 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
neg₁₄ :
  ∀ (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
neg₁₅ :
  ∀ (h : ¬f = 0 ∧ ¬g = 0) (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))
    (u v : F[X]) (hfg : u * f + v * g = 1), False
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ 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)

Premises used: Multiset.toFinset_add, zero_ne_one, map_add, Finset.card_union_eq_card_add_card, Finset.disjoint_iff_ne, mul_eq_zero, not_or, MulZeroClass.mul_zero, map_mul, map_one, Polynomial.natSepDegree_eq_of_isAlgClosed, Polynomial.mem_aroots, Polynomial.aroots_mul, add_zero, AlgebraicClosure, Multiset.mem_toFinset, rfl