awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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))
⊢ (g * r).resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
have rw : (-r).natDegree + g.natDegree ≤ (g * r).natDegree
Tactic: rw [← resultant_add_mul_left _ _ (-r) _ _ _ le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (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))
have 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))
Tactic: rw [mul_neg, add_neg_cancel, resultant_zero_left]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ 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))
have 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))
Tactic: by_cases H : g.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases H : g.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ 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))
have 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)))
Tactic: obtain rfl := hg.natDegree_eq_zero.mp H
Cleared hypotheses: g, hg, hg', hf, hf', hfg, hN, H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ 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))
have 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))
Tactic: simp only [zero_pow H]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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
⊢ 0 * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
have H₁ : ∃ (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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ 0 * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
have 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))
Tactic: obtain ⟨x, hx⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ 0 * g.coeff 0 ^ (g * r).natDegree =
    Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
have neg : Membership.mem (γ := Multiset K) (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)) 0
Tactic: rw [Multiset.prod_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ Membership.mem (γ := Multiset K) (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)) 0
have neg : ∃ (a : K) (b : K), (a, b) ∈ (g * r).roots ×ˢ g.roots ∧ a - b = 0
Tactic: simp only [Multiset.mem_map, Prod.exists]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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).natDegree + g.natDegree ≤ (g * r).natDegree
have rw : (-r).natDegree + g.natDegree ≤ g.natDegree + r.natDegree
Tactic: rw [natDegree_mul hg.ne_zero (by simpa [hg.ne_zero] using hf.ne_zero),
        natDegree_neg, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (-r).natDegree + g.natDegree ≤ (g * r).natDegree
have rw₁ : r.natDegree + g.natDegree ≤ g.natDegree + r.natDegree
Tactic: rw [natDegree_mul hg.ne_zero (by simpa [hg.ne_zero] using hf.ne_zero),
        natDegree_neg, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (-r).natDegree + g.natDegree ≤ (g * r).natDegree
have rw₂ : g.natDegree + r.natDegree ≤ g.natDegree + r.natDegree
Tactic: rw [natDegree_mul hg.ne_zero (by simpa [hg.ne_zero] using hf.ne_zero),
        natDegree_neg, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have hr₀ : f %ₘ g ≠ 0
Tactic: have hr₀ : f %ₘ g ≠ 0 := by simpa [modByMonic_eq_zero_iff_dvd, hg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have hrd : 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)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).Monic
have rw : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).leadingCoeff = 1
Tactic: rw [Monic, leadingCoeff, natDegree_C_mul (by simpa), coeff_C_mul, leadingCoeff,
      inv_mul_cancel₀ (by simpa)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
rw : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).leadingCoeff = 1
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).Monic
have rw₁ : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff
    (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).natDegree =
  1
Tactic: rw [Monic, leadingCoeff, natDegree_C_mul (by simpa), coeff_C_mul, leadingCoeff,
      inv_mul_cancel₀ (by simpa)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
rw : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).leadingCoeff = 1
rw₁ :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff
      (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).natDegree =
    1
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).Monic
have rw₂ : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff (f %ₘ g).natDegree = 1
Tactic: rw [Monic, leadingCoeff, natDegree_C_mul (by simpa), coeff_C_mul, leadingCoeff,
      inv_mul_cancel₀ (by simpa)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
rw : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).leadingCoeff = 1
rw₁ :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff
      (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).natDegree =
    1
rw₂ :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff (f %ₘ g).natDegree = 1
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).Monic
have rw₃ : (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g).coeff (f %ₘ g).natDegree = 1
Tactic: rw [Monic, leadingCoeff, natDegree_C_mul (by simpa), coeff_C_mul, leadingCoeff,
      inv_mul_cancel₀ (by simpa)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
rw : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).leadingCoeff = 1
rw₁ :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff
      (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).natDegree =
    1
rw₂ :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff (f %ₘ g).natDegree = 1
rw₃ : (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g).coeff (f %ₘ g).natDegree = 1
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).Monic
have rw₄ : ((f %ₘ g).coeff (f %ₘ g).natDegree)⁻¹ * (f %ₘ g).coeff (f %ₘ g).natDegree = 1
Tactic: rw [Monic, leadingCoeff, natDegree_C_mul (by simpa), coeff_C_mul, leadingCoeff,
      inv_mul_cancel₀ (by simpa)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
rw : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).leadingCoeff = 1
rw₁ :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff
      (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).natDegree =
    1
rw₂ :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).coeff (f %ₘ g).natDegree = 1
rw₃ : (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g).coeff (f %ₘ g).natDegree = 1
rw₄ : ((f %ₘ g).coeff (f %ₘ g).natDegree)⁻¹ * (f %ₘ g).coeff (f %ₘ g).natDegree = 1
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (f %ₘ g).leadingCoeff⁻¹ : K[X]) (f %ₘ g)).Monic
have rw₅ : Eq.{u_3 + 1} (α := K) 1 1
Tactic: rw [Monic, leadingCoeff, natDegree_C_mul (by simpa), coeff_C_mul, leadingCoeff,
      inv_mul_cancel₀ (by simpa)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have hr₁ : r.Monic
Tactic: have hr : r.Monic := by
    dsimp only [r]
    rw [Monic, leadingCoeff, natDegree_C_mul (by simpa), coeff_C_mul, leadingCoeff,
      inv_mul_cancel₀ (by simpa)]