-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits)
      (hfg : g.natDegree ≤ f.natDegree) (hN : f.natDegree + g.natDegree = m),
      f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr_1 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this_1 :
  (algebraMap K L : (a : K) → L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
      (Multiset.prod
          (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2)
            ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)) :
        L)
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ eval x f) g.roots) =
    (f %ₘ g).leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : K) ↦ eval x r) g.roots)
neg :
  HPow.hPow (α := L) (-1) (g.natDegree * (f.natDegree - r.natDegree)) *
      (HPow.hPow (α := L) (-1) (r.natDegree * g.natDegree) *
        (HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (f %ₘ g).leadingCoeff : L) g.natDegree *
          Multiset.prod
            (Multiset.map
              (fun (x : K) ↦
                ((aeval ((algebraMap K L : (a : K) → L) x) : K[X] →ₐ[K] r.SplittingField) :
                    (a : K[X]) → r.SplittingField)
                  r)
              g.roots))) =
    HPow.hPow (α := L) (-1) (g.natDegree * f.natDegree) *
      (HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (f %ₘ g).leadingCoeff : L) g.natDegree *
        Multiset.prod (Multiset.map (fun (x : K) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (eval x r)) g.roots))
⊢ HMul.hMul (α := L) (β := L)
        (((algebraMap K L : K →+* L) : (a : K) → L)
            (HPow.hPow (α := K) (-1) (g.natDegree * (f.natDegree - r.natDegree))) :
          L)
        (((algebraMap K L : K →+* L) : (a : K) → L) (g.coeff g.natDegree ^ (f.natDegree - r.natDegree)) : L) *
      HMul.hMul (α := L)
        (((algebraMap K L : K →+* L) : (a : K) → L) (HPow.hPow (α := K) (-1) (r.natDegree * g.natDegree)) : L)
        (HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((f %ₘ g).leadingCoeff ^ g.natDegree) : L)
          (Multiset.prod
              (Multiset.map (fun (x : r.SplittingField) ↦ eval x (map (algebraMap K r.SplittingField) r))
                (Multiset.map (⇑(algebraMap K L) : (a : K) → L) g.roots)) :
            r.SplittingField)) =
    HMul.hMul (α := L) (β := L)
      (((algebraMap K L : K →+* L) : (a : K) → L) (HPow.hPow (α := K) (-1) (g.roots.card * f.roots.card)) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) (Multiset.prod (Multiset.map (fun (x : K) ↦ eval x f) g.roots)) : L)

Tactic:
simp only [coeff_natDegree, hg.leadingCoeff, one_pow, map_one, map_multiset_prod,
      ← hf'.natDegree_eq_card_roots, ← hg'.natDegree_eq_card_roots, this, map_mul, Multiset.map_map,
      map_pow, map_neg, mul_one, eval_map_algebraMap, Function.comp_apply]

Premises used: one_pow, Polynomial.coeff_natDegree, map_neg, map_pow, map_multiset_prod, map_mul, Polynomial.Splits.natDegree_eq_card_roots, map_one, Multiset.map_map, Polynomial.eval_map_algebraMap, Function.comp_apply, Polynomial.Monic.leadingCoeff, mul_one