awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
b : Fin (m + 1 + (n + 1))
hb : b ≠ Fin.castAdd (n + 1) (Fin.last m)
left :
  ∀ (b : Fin (m + 1))
    (hb :
      Ne (α := Fin ((m + 1).add n).succ) (Fin.castAdd (n + 1) b : Fin (m + 1 + (n + 1)))
        (Fin.castAdd (n + 1) (Fin.last m))),
    f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.castAdd (n + 1) b) = 0
right :
  ∀ (i : Fin (n + 1)) (hb : Fin.natAdd (m + 1) i ≠ Fin.castAdd (n + 1) (Fin.last m)),
    f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n) : Fin (m + 1 + n + 1)) (Fin.natAdd (m + 1) i) = 0
⊢ f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) b = 0

Tactic:
induction b using Fin.addCases with
    | left b =>
      simp only [Nat.add_eq, Nat.succ_eq_add_one, ne_eq, Fin.ext_iff, Fin.val_castAdd,
        Fin.val_last] at hb
      simp only [sylvester, Set.mem_Icc, Matrix.of_apply, Fin.val_last, Fin.addCases_left,
        ite_eq_right_iff, and_imp]
      intros
      lia
    | right i => simpa [sylvester] using fun _ _ ↦ coeff_eq_zero_of_natDegree_lt (by lia)

Premises used: Fin.addCases_left, Fin.ext_iff, Nat.add_eq, Nat.succ_eq_add_one, and_imp, Matrix.of_apply, ne_eq, Fin.val_castAdd, Polynomial.sylvester, ite_eq_right_iff, Polynomial.coeff_eq_zero_of_natDegree_lt, Set.mem_Icc, Fin.val_last
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k : ℕ
hf : f.natDegree ≤ m
⊢ f.resultant g (m + 0) n = HPow.hPow (α := R) (-1) (n * 0) * HPow.hPow (β := ℕ) (g.coeff n) 0 * f.resultant g m n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k_1 : ℕ
hf : f.natDegree ≤ m
k : ℕ
IH : f.resultant g (m + k) n = HPow.hPow (α := R) (-1) (n * k) * g.coeff n ^ k * f.resultant g m n
succ :
  HPow.hPow (α := R) (-1) n * g.coeff n * (HPow.hPow (α := R) (-1) (n * k) * g.coeff n ^ k * f.resultant g m n) =
    HPow.hPow (α := R) (-1) (n * (k + 1)) * g.coeff n ^ (k + 1) * f.resultant g m n
⊢ f.resultant g (m + (k + 1)) n = HPow.hPow (α := R) (-1) (n * (k + 1)) * g.coeff n ^ (k + 1) * f.resultant g m n

Tactic:
simp [← add_assoc, resultant_succ_left_deg, hf.trans, IH]

Premises used: add_assoc, Polynomial.resultant_succ_left_deg, LE.le.trans
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k_1 : ℕ
hf : f.natDegree ≤ m
k : ℕ
IH : f.resultant g (m + k) n = HPow.hPow (α := R) (-1) (n * k) * g.coeff n ^ k * f.resultant g m n
⊢ HPow.hPow (α := R) (-1) n * g.coeff n * (HPow.hPow (α := R) (-1) (n * k) * g.coeff n ^ k * f.resultant g m n) =
    HPow.hPow (α := R) (-1) (n * (k + 1)) * g.coeff n ^ (k + 1) * f.resultant g m n

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k : ℕ
hf : f.natDegree ≤ m
zero : f.resultant g (m + 0) n = HPow.hPow (α := R) (-1) (n * 0) * HPow.hPow (β := ℕ) (g.coeff n) 0 * f.resultant g m n
succ :
  ∀ (k : ℕ) (IH : f.resultant g (m + k) n = HPow.hPow (α := R) (-1) (n * k) * g.coeff n ^ k * f.resultant g m n),
    f.resultant g (m + (k + 1)) n = HPow.hPow (α := R) (-1) (n * (k + 1)) * g.coeff n ^ (k + 1) * f.resultant g m n
⊢ f.resultant g (m + k) n = HPow.hPow (α := R) (-1) (n * k) * g.coeff n ^ k * f.resultant g m n

Tactic:
induction k with
  | zero => simp
  | succ k IH => simp [← add_assoc, resultant_succ_left_deg, hf.trans, IH]; ring

Premises used: add_assoc, Polynomial.resultant_succ_left_deg, LE.le.trans
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ n
rw :
  HPow.hPow (α := R) (-1) (m * (n + k)) *
      (HPow.hPow (α := R) (-1) (m * k) * (HPow.hPow (α := R) (-1) (n * m) * (f.coeff m ^ k * f.resultant g m n))) =
    f.coeff m ^ k * f.resultant g m n
⊢ f.resultant g m (n + k) = f.coeff m ^ k * f.resultant g m n

Tactic:
rw [resultant_comm, resultant_add_left_deg _ _ _ _ _ hg, resultant_comm,
    mul_assoc, mul_left_comm (f.coeff m ^ k)]

Premises used: Polynomial.resultant_add_left_deg, Polynomial.resultant_comm, mul_assoc, mul_left_comm, Polynomial.coeff, HPow.hPow
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ n
simp :
  HPow.hPow (α := R) (-1) (m * (n + k + (k + n))) * f.coeff m ^ k * f.resultant g m n =
    f.coeff m ^ k * f.resultant g m n
⊢ HPow.hPow (α := R) (-1) (m * (n + k)) *
      (HPow.hPow (α := R) (-1) (m * k) * (HPow.hPow (α := R) (-1) (n * m) * (f.coeff m ^ k * f.resultant g m n))) =
    f.coeff m ^ k * f.resultant g m n

Tactic:
simp only [← mul_assoc, ← pow_add, ← mul_add, mul_comm _ m]

Premises used: mul_assoc, pow_add, mul_comm, mul_add
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ n
ring_nf :
  f.coeff m ^ k * f.resultant g m n * HPow.hPow (α := R) (-1) (m * n * 2) * HPow.hPow (α := R) (-1) (m * k * 2) =
    f.coeff m ^ k * f.resultant g m n
⊢ HPow.hPow (α := R) (-1) (m * (n + k + (k + n))) * f.coeff m ^ k * f.resultant g m n =
    f.coeff m ^ k * f.resultant g m n

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ n
⊢ f.coeff m ^ k * f.resultant g m n * HPow.hPow (α := R) (-1) (m * n * 2) * HPow.hPow (α := R) (-1) (m * k * 2) =
    f.coeff m ^ k * f.resultant g m n

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hf : f.natDegree < m
hg : g.natDegree < n
zero : ∀ (hf : f.natDegree < 0), f.resultant g 0 n = 0
succ : ∀ (m : ℕ) (hf : f.natDegree < m + 1), f.resultant g (m + 1) n = 0
⊢ f.resultant g m n = 0

Tactic:
obtain _ | m := m
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
n : ℕ
hg : g.natDegree < n
hf : f.natDegree < 0
⊢ f.resultant g 0 n = 0

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
n : ℕ
hg : g.natDegree < n
m : ℕ
hf : f.natDegree < m + 1
succ : ∀ (hg : g.natDegree < 0), f.resultant g (m + 1) 0 = 0
succ₁ : ∀ (n : ℕ) (hg : g.natDegree < n + 1), f.resultant g (m + 1) (n + 1) = 0
⊢ f.resultant g (m + 1) n = 0

Tactic:
obtain _ | n := n
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
hg : g.natDegree < 0
⊢ f.resultant g (m + 1) 0 = 0

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
n : ℕ
hg : g.natDegree < n + 1
⊢ f.natDegree ≤ m

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
n : ℕ
hg : g.natDegree < n + 1
⊢ g.natDegree ≤ n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
n : ℕ
hg : g.natDegree < n + 1
succ :
  HPow.hPow (α := R) (-1) ((n + 1) * 1) * HPow.hPow (β := ℕ) (g.coeff (n + 1)) 1 *
      (HPow.hPow (β := ℕ) (f.coeff m) 1 * f.resultant g m n) =
    0
⊢ f.resultant g (m + 1) (n + 1) = 0

Tactic:
rw [resultant_add_left_deg _ _ _ _ _ (by lia), resultant_add_right_deg _ _ _ _ _ (by lia)]

Premises used: Polynomial.resultant_add_left_deg, Polynomial.resultant_add_right_deg
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
n : ℕ
hg : g.natDegree < n + 1
⊢ HPow.hPow (α := R) (-1) ((n + 1) * 1) * HPow.hPow (β := ℕ) (g.coeff (n + 1)) 1 *
      (HPow.hPow (β := ℕ) (f.coeff m) 1 * f.resultant g m n) =
    0

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hg]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
r : R
⊢ natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) ≤ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
r : R
rw :
  HPow.hPow (α := R) (-1) (m * n) * g.coeff n ^ m * resultant ((C : (a : R) → R[X]) r) g 0 n =
    HPow.hPow (α := R) (-1) ((0 + m) * n) * g.coeff n ^ (0 + m) * r ^ n
⊢ resultant ((C : (a : R) → R[X]) r) g m n = HPow.hPow (α := R) (-1) (m * n) * g.coeff n ^ m * r ^ n

Tactic:
rw [← zero_add m, resultant_add_left_deg _ _ _ _ _ (by simp), mul_comm n m]

Premises used: Polynomial.resultant_add_left_deg, zero_add, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
r : R
⊢ HPow.hPow (α := R) (-1) (m * n) * g.coeff n ^ m * resultant ((C : (a : R) → R[X]) r) g 0 n =
    HPow.hPow (α := R) (-1) ((0 + m) * n) * g.coeff n ^ (0 + m) * r ^ n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
r : R
⊢ natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) ≤ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
r : R
rw : f.coeff m ^ n * f.resultant ((C : (a : R) → R[X]) r) m 0 = f.coeff m ^ (0 + n) * r ^ m
⊢ f.resultant ((C : (a : R) → R[X]) r) m n = f.coeff m ^ n * r ^ m

Tactic:
rw [← zero_add n, resultant_add_right_deg _ _ _ _ _ (by simp)]

Premises used: zero_add, Polynomial.resultant_add_right_deg
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
r : R
⊢ f.coeff m ^ n * f.resultant ((C : (a : R) → R[X]) r) m 0 = f.coeff m ^ (0 + n) * r ^ m

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
⊢ resultant 1 g m n = HPow.hPow (α := R) (-1) (m * n) * g.coeff n ^ m

Tactic:
simpa [-resultant_C_left] using resultant_C_left g m n 1

Premises used: Polynomial.resultant_C_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
⊢ f.resultant 1 m n = f.coeff m ^ n

Tactic:
simpa [-resultant_C_right] using resultant_C_right f m n 1

Premises used: Polynomial.resultant_C_right, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg : g.natDegree ≤ n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg : g.natDegree ≤ n
h : Nontrivial R
inl :
  ∀ (hg : g.natDegree = 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval r g
inr :
  ∀ (hg : g.natDegree > 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval r g
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval r g

Tactic:
obtain hg | hg := g.natDegree.eq_zero_or_pos

Premises used: Polynomial.natDegree, Nat.eq_zero_or_pos
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg_1 : g.natDegree ≤ n
h : Nontrivial R
hg : g.natDegree = 0
inl :
  ∀ (s : R) (hg : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) s) ≤ n)
    (hg : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) s) = 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant ((C : (a : R) → R[X]) s) 1 n =
      eval r ((C : (a : R) → R[X]) s)
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval r g

Tactic:
obtain ⟨s, rfl⟩ := natDegree_eq_zero.mp hg

Premises used: Iff.mp, Polynomial.natDegree_eq_zero, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
r : R
h : Nontrivial R
s : R
hg_1 : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) s) ≤ n
hg : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) s) = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant ((C : (a : R) → R[X]) s) 1 n =
    eval r ((C : (a : R) → R[X]) s)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg_1 : g.natDegree ≤ n
h : Nontrivial R
hg : g.natDegree > 0
rw :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant
    (g %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) +
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) *
        (g /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])))
    1 n
| (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n

Tactic:
rw [← g.modByMonic_add_div (X - C r)]

Premises used: Polynomial.C, HSub.hSub, Polynomial.modByMonic_add_div, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg_1 : g.natDegree ≤ n
h : Nontrivial R
hg : g.natDegree > 0
inr :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant
      (g %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) +
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) *
          (g /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])))
      1 n =
    eval r g
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval r g

Tactic:
conv_lhs => rw [← g.modByMonic_add_div (X - C r)]

Premises used: Polynomial.C, HSub.hSub, Polynomial.modByMonic_add_div, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg_1 : g.natDegree ≤ n
h : Nontrivial R
hg : g.natDegree > 0
inr :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant ((C : (a : R) → R[X]) (eval r g)) 1
      n =
    eval r g
rw : (g /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree + 1 ≤ n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant
      (g %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) +
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) *
          (g /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])))
      1 n =
    eval r g

Tactic:
rw [resultant_add_mul_right _ _ _ _ _ _ (natDegree_X_sub_C_le _), modByMonic_X_sub_C_eq_C_eval]

Premises used: Polynomial.resultant_add_mul_right, Polynomial.modByMonic_X_sub_C_eq_C_eval, Polynomial.natDegree_X_sub_C_le
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg_1 : g.natDegree ≤ n
h : Nontrivial R
hg : g.natDegree > 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant ((C : (a : R) → R[X]) (eval r g)) 1
      n =
    eval r g

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg_1 : g.natDegree ≤ n
h : Nontrivial R
hg : g.natDegree > 0
rw : g.natDegree - 1 + 1 ≤ n
⊢ (g /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree + 1 ≤ n

Tactic:
rw [natDegree_divByMonic g (monic_X_sub_C r), natDegree_sub_C, natDegree_X]

Premises used: Polynomial.monic_X_sub_C, Polynomial.natDegree_X, Polynomial.natDegree_divByMonic, Polynomial.natDegree_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg_1 : g.natDegree ≤ n
h : Nontrivial R
hg : g.natDegree > 0
⊢ g.natDegree - 1 + 1 ≤ n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg : g.natDegree ≤ n
rw :
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])).resultant g 1 n
rw₁ :
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n =
    (HSub.hSub (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) r : R[X])).resultant g 1 n
rw₂ rw₃ :
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval (-r) g

Tactic:
rw [← resultant_X_sub_C_left g n (-r) hg, map_neg, sub_neg_eq_add]

Premises used: map_neg, Polynomial.resultant_X_sub_C_left, Neg.neg, sub_neg_eq_add
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
rw : HPow.hPow (α := R) (-1) (m * 1) * eval r f = HPow.hPow (α := R) (-1) m * eval r f
⊢ f.resultant (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) m 1 =
    HPow.hPow (α := R) (-1) m * eval r f

Tactic:
rw [resultant_comm, resultant_X_sub_C_left _ _ _ hf]

Premises used: Polynomial.resultant_comm, Polynomial.resultant_X_sub_C_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
⊢ HPow.hPow (α := R) (-1) (m * 1) * eval r f = HPow.hPow (α := R) (-1) m * eval r f

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
rw :
  f.resultant (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) m 1 =
    f.resultant (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) m 1
rw₁ :
  f.resultant (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) m 1 =
    f.resultant (HSub.hSub (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) r : R[X])) m 1
rw₂ rw₃ :
  f.resultant (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) m 1 =
    f.resultant (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) m 1
⊢ f.resultant (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) m 1 =
    HPow.hPow (α := R) (-1) m * eval (-r) f

Tactic:
rw [← resultant_X_sub_C_right f m (-r) hf, map_neg, sub_neg_eq_add]

Premises used: Polynomial.resultant_X_sub_C_right, map_neg, Neg.neg, sub_neg_eq_add
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
inr :
  ∀
    (this :
      ∀ {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),
        f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)))
    (hfg : ¬g.natDegree ≤ f.natDegree),
    f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
wlog :
  ∀ {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),
    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:
wlog hfg : g.natDegree ≤ f.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {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),
    f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
hfg : ¬g.natDegree ≤ f.natDegree
trans : f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots))
trans₁ :
  Eq (α := K) (Multiset.prod (Multiset.map (fun (ij : K × K) ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots)))
    (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:
trans ((f.roots ×ˢ g.roots).map fun ij ↦ (-1) * (ij.2 - ij.1)).prod

Premises used: Polynomial.roots, HMul.hMul, Multiset.map, SProd.sprod, Multiset.prod, HSub.hSub, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {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),
    f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
hfg : ¬g.natDegree ≤ f.natDegree
rw :
  HPow.hPow (α := K) (-1) (f.natDegree * g.natDegree) *
      Multiset.prod (Multiset.map ((fun (ij : K × K) ↦ ij.1 - ij.2) ∘ Prod.swap) (f.roots ×ˢ g.roots)) =
    HMul.hMul (α := K) (Multiset.prod (Multiset.map (fun (ij : K × K) ↦ -1) (f.roots ×ˢ g.roots)))
      (Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.2 - ij.1) (f.roots ×ˢ g.roots)))
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots))

Tactic:
rw [resultant_comm, this g f hg hf hg' hf' (le_of_not_ge hfg), ← Multiset.map_swap_product,
        Multiset.map_map, Multiset.prod_map_mul]

Premises used: Polynomial.resultant_comm, le_of_not_ge, Multiset.prod_map_mul, Multiset.map_map, Multiset.map_swap_product
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {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),
    f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
hfg : ¬g.natDegree ≤ f.natDegree
⊢ HPow.hPow (α := K) (-1) (f.natDegree * g.natDegree) *
      Multiset.prod (Multiset.map ((fun (ij : K × K) ↦ ij.1 - ij.2) ∘ Prod.swap) (f.roots ×ˢ g.roots)) =
    HMul.hMul (α := K) (Multiset.prod (Multiset.map (fun (ij : K × K) ↦ -1) (f.roots ×ˢ g.roots)))
      (Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.2 - ij.1) (f.roots ×ˢ g.roots)))

Tactic:
simp [hf'.natDegree_eq_card_roots, hg'.natDegree_eq_card_roots]

Premises used: Polynomial.Splits.natDegree_eq_card_roots
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {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),
    f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
hfg : ¬g.natDegree ≤ f.natDegree
⊢ Eq (α := K) (Multiset.prod (Multiset.map (fun (ij : K × K) ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots)))
    (Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
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
generalize :
  ∀ (N : ℕ) (hN : f.natDegree + g.natDegree = N),
    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:
generalize hN : f.natDegree + g.natDegree = N

Premises used: Polynomial.natDegree