awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
pos : ∀ (hr : g ∣ f), f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
neg :
  ∀ (hr : ¬g ∣ f), f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))

Tactic:
by_cases hr : g ∣ f
-- 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 : g ∣ f
pos :
  ∀ (r : K[X]) (hf : (g * r).Monic) (hf' : (g * r).Splits) (hfg : g.natDegree ≤ (g * r).natDegree)
    (hN : (g * r).natDegree + g.natDegree = n),
    (g * r).resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))

Tactic:
obtain ⟨r, rfl⟩ := hr

Premises used: rfl
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
⊢ r ≠ 0

Tactic:
simpa [hg.ne_zero] using hf.ne_zero

Premises used: Polynomial.Monic.ne_zero
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
⊢ r ≠ 0

Tactic:
have hr' : r ≠ 0 := by simpa [hg.ne_zero] using hf.ne_zero
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
pos :
  (g * r + g * -r).resultant g (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
rw : (-r).natDegree + g.natDegree ≤ (g * r).natDegree
⊢ (g * r).resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))

Tactic:
rw [← resultant_add_mul_left _ _ (-r) _ _ _ le_rfl]

Premises used: le_rfl, Polynomial.resultant_add_mul_left, Neg.neg
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
pos :
  HPow.hPow (α := K) 0 g.natDegree * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
⊢ (g * r + g * -r).resultant g (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))

Tactic:
rw [mul_neg, add_neg_cancel, resultant_zero_left]

Premises used: add_neg_cancel, Polynomial.resultant_zero_left, mul_neg
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
pos :
  ∀ (H : g.natDegree = 0),
    HPow.hPow (α := K) 0 g.natDegree * g.coeff 0 ^ (g * r).natDegree =
      Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
neg :
  ∀ (H : ¬g.natDegree = 0),
    HPow.hPow (α := K) 0 g.natDegree * g.coeff 0 ^ (g * r).natDegree =
      Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
⊢ HPow.hPow (α := K) 0 g.natDegree * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))

Tactic:
by_cases H : g.natDegree = 0

Premises used: Polynomial.natDegree
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : g.natDegree = 0
pos :
  ∀ (hg : Monic.{u_3} (R := K) 1) (hg' : Splits.{u_3} (R := K) 1) (hf : (1 * r).Monic) (hf' : (1 * r).Splits)
    (hfg : natDegree.{u_3} (R := K) 1 ≤ (1 * r).natDegree) (hN : (1 * r).natDegree + natDegree.{u_3} (R := K) 1 = n)
    (H : natDegree.{u_3} (R := K) 1 = 0),
    HPow.hPow (α := K) 0 (natDegree.{u_3} (R := K) 1) * HPow.hPow (α := K) (coeff 1 0) (1 * r).natDegree =
      Multiset.prod
        (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (SProd.sprod (β := Multiset K) (1 * r).roots (roots 1)))
⊢ HPow.hPow (α := K) 0 g.natDegree * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))

Tactic:
obtain rfl := hg.natDegree_eq_zero.mp H

Premises used: Polynomial.Monic.natDegree_eq_zero, Iff.mp, rfl
-- 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
r : K[X]
hr' : r ≠ 0
hg : Monic.{u_3} (R := K) 1
hg' : Splits.{u_3} (R := K) 1
hf : (1 * r).Monic
hf' : (1 * r).Splits
hfg : natDegree.{u_3} (R := K) 1 ≤ (1 * r).natDegree
hN : (1 * r).natDegree + natDegree.{u_3} (R := K) 1 = n
H : natDegree.{u_3} (R := K) 1 = 0
⊢ HPow.hPow (α := K) 0 (natDegree.{u_3} (R := K) 1) * HPow.hPow (α := K) (coeff 1 0) (1 * r).natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (SProd.sprod (β := Multiset K) (1 * r).roots (roots 1)))

Tactic:
simp
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ¬g.natDegree = 0
neg :
  0 * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
⊢ HPow.hPow (α := K) 0 g.natDegree * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))

Tactic:
simp only [zero_pow H]

Premises used: zero_pow
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ¬g.natDegree = 0
⊢ ∃ (x : K), x ∈ g.roots

Tactic:
rw [hg'.natDegree_eq_card_roots, Multiset.card_eq_zero,
          Multiset.eq_zero_iff_forall_notMem, not_forall_not] at H

Premises used: Multiset.card_eq_zero, not_forall_not, Multiset.eq_zero_iff_forall_notMem, Polynomial.Splits.natDegree_eq_card_roots
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ∃ (x : K), x ∈ g.roots
neg :
  ∀ (x : K) (hx : x ∈ g.roots),
    0 * g.coeff 0 ^ (g * r).natDegree =
      Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
⊢ 0 * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))

Tactic:
obtain ⟨x, hx⟩ := H
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
x : K
hx : x ∈ g.roots
neg : Membership.mem (γ := Multiset K) (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)) 0
⊢ 0 * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))

Tactic:
rw [Multiset.prod_eq_zero, zero_mul]

Premises used: Multiset.prod_eq_zero, MulZeroClass.zero_mul
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
x : K
hx : x ∈ g.roots
neg : ∃ (a : K) (b : K), (a, b) ∈ (g * r).roots ×ˢ g.roots ∧ a - b = 0
⊢ Membership.mem (γ := Multiset K) (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)) 0

Tactic:
simp only [Multiset.mem_map, Prod.exists]

Premises used: Multiset.mem_map, Prod.exists
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
x : K
hx : x ∈ g.roots
⊢ (x, x).1 ∈ (g * r).roots ∧ (x, x).2 ∈ g.roots

Tactic:
simp_all [hg.ne_zero]

Premises used: Polynomial.Monic.ne_zero
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
x : K
hx : x ∈ g.roots
⊢ x - x = 0

Tactic:
simp
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
x : K
hx : x ∈ g.roots
⊢ ∃ (a : K) (b : K), (a, b) ∈ (g * r).roots ×ˢ g.roots ∧ a - b = 0

Tactic:
exact ⟨x, x, Multiset.mem_product.mpr (by simp_all [hg.ne_zero]), by simp⟩
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
⊢ r ≠ 0

Tactic:
simpa [hg.ne_zero] using hf.ne_zero

Premises used: Polynomial.Monic.ne_zero
-- 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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
rw : (-r).natDegree + g.natDegree ≤ g.natDegree + r.natDegree
rw₁ : r.natDegree + g.natDegree ≤ g.natDegree + r.natDegree
rw₂ rw₃ : g.natDegree + r.natDegree ≤ g.natDegree + r.natDegree
⊢ (-r).natDegree + g.natDegree ≤ (g * r).natDegree

Tactic:
rw [natDegree_mul hg.ne_zero (by simpa [hg.ne_zero] using hf.ne_zero),
        natDegree_neg, add_comm]

Premises used: Polynomial.natDegree_mul, add_comm, Polynomial.natDegree_neg, Polynomial.Monic.ne_zero
-- 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 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
⊢ f %ₘ g ≠ 0

Tactic:
simpa [modByMonic_eq_zero_iff_dvd, hg]

Premises used: Polynomial.modByMonic_eq_zero_iff_dvd
-- 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 : ¬g ∣ f
r : K[X] := HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)
⊢ f %ₘ g ≠ 0

Tactic:
have hr₀ : f %ₘ g ≠ 0 := by simpa [modByMonic_eq_zero_iff_dvd, hg]
-- 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 : ¬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
⊢ g ≠ 1

Tactic:
aesop
-- 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 : ¬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
⊢ r.natDegree < g.natDegree

Tactic:
simp [r, natDegree_C_mul, hr₀, natDegree_modByMonic_lt _ hg (show g ≠ 1 by aesop)]

Premises used: Polynomial.natDegree_modByMonic_lt, Polynomial.natDegree_C_mul
-- 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 : ¬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
⊢ r.natDegree < g.natDegree

Tactic:
have hrd : r.natDegree < g.natDegree := by
    simp [r, natDegree_C_mul, hr₀, natDegree_modByMonic_lt _ hg (show g ≠ 1 by aesop)]
-- 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 : ¬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
dsimp : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).Monic
⊢ r.Monic

Tactic:
dsimp only [r]
-- 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 : ¬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
⊢ (f %ₘ g).leadingCoeff⁻¹ ≠ 0

Tactic:
simpa
-- 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 : ¬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
⊢ (f %ₘ g).coeff (f %ₘ g).natDegree ≠ 0

Tactic:
simpa