awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ n
⊢ f.resultant g m (n + k) = f.coeff m ^ k * f.resultant g m n
have 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
Tactic: rw [resultant_comm, resultant_add_left_deg _ _ _ _ _ hg, resultant_comm,
    mul_assoc, mul_left_comm (f.coeff m ^ k)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ 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
have 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
Tactic: simp only [← mul_assoc, ← pow_add, ← mul_add, mul_comm _ m]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ 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
have 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
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
hf : f.natDegree < m
hg : g.natDegree < n
⊢ f.resultant g m n = 0
have zero : ∀ (hf : f.natDegree < 0), f.resultant g 0 n = 0
Tactic: obtain _ | m := m
Cleared hypotheses: m, hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ f.resultant g m n = 0
have succ : ∀ (m : ℕ) (hf : f.natDegree < m + 1), f.resultant g (m + 1) n = 0
Tactic: obtain _ | m := m
Cleared hypotheses: m, hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
n : ℕ
hg : g.natDegree < n
m : ℕ
hf : f.natDegree < m + 1
⊢ f.resultant g (m + 1) n = 0
have succ : ∀ (hg : g.natDegree < 0), f.resultant g (m + 1) 0 = 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, hg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ f.resultant g (m + 1) n = 0
have succ₁ : ∀ (n : ℕ) (hg : g.natDegree < n + 1), f.resultant g (m + 1) (n + 1) = 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, hg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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.resultant g (m + 1) (n + 1) = 0
have 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
Tactic: rw [resultant_add_left_deg _ _ _ _ _ (by lia), resultant_add_right_deg _ _ _ _ _ (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
r : R
⊢ resultant ((C : (a : R) → R[X]) r) g m n = HPow.hPow (α := R) (-1) (m * n) * g.coeff n ^ m * r ^ n
have 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
Tactic: rw [← zero_add m, resultant_add_left_deg _ _ _ _ _ (by simp), mul_comm n m]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
r : R
⊢ f.resultant ((C : (a : R) → R[X]) r) m n = f.coeff m ^ n * r ^ m
have rw : f.coeff m ^ n * f.resultant ((C : (a : R) → R[X]) r) m 0 = f.coeff m ^ (0 + n) * r ^ m
Tactic: rw [← zero_add n, resultant_add_right_deg _ _ _ _ _ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg : g.natDegree ≤ n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval r g
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg : g.natDegree ≤ n
h : Nontrivial R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval r g
have 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
Tactic: obtain hg | hg := g.natDegree.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval r g
have 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
Tactic: obtain hg | hg := g.natDegree.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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 g 1 n = eval r g
have 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)
Tactic: obtain ⟨s, rfl⟩ := natDegree_eq_zero.mp hg
Cleared hypotheses: g, hg_1, hg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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 g 1 n
have 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
Tactic: rw [← g.modByMonic_add_div (X - C r)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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 g 1 n = eval r g
have 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
Tactic: conv_lhs => rw [← g.modByMonic_add_div (X - C r)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
      (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
have 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
Tactic: rw [resultant_add_mul_right _ _ _ _ _ _ (natDegree_X_sub_C_le _), modByMonic_X_sub_C_eq_C_eval]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (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
have rw : (g /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree + 1 ≤ n
Tactic: rw [resultant_add_mul_right _ _ _ _ _ _ (natDegree_X_sub_C_le _), modByMonic_X_sub_C_eq_C_eval]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree + 1 ≤ n
have rw : g.natDegree - 1 + 1 ≤ n
Tactic: rw [natDegree_divByMonic g (monic_X_sub_C r), natDegree_sub_C, natDegree_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
n : ℕ
r : R
hg : g.natDegree ≤ n
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval (-r) g
have 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
Tactic: rw [← resultant_X_sub_C_left g n (-r) hg, map_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval (-r) g
have 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
Tactic: rw [← resultant_X_sub_C_left g n (-r) hg, map_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).resultant g 1 n = eval (-r) g
have 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
Tactic: rw [← resultant_X_sub_C_left g n (-r) hg, map_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
⊢ 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
have rw : HPow.hPow (α := R) (-1) (m * 1) * eval r f = HPow.hPow (α := R) (-1) m * eval r f
Tactic: rw [resultant_comm, resultant_X_sub_C_left _ _ _ hf]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
⊢ 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
have 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
Tactic: rw [← resultant_X_sub_C_right f m (-r) hf, map_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [← resultant_X_sub_C_right f m (-r) hf, map_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [← resultant_X_sub_C_right f m (-r) hf, map_neg, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
K : Type u_3
inst : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have 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))
Tactic: wlog hfg : g.natDegree ≤ f.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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))
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have 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))
Tactic: wlog hfg : g.natDegree ≤ f.natDegree
Cleared hypotheses: K, inst, f, g, hf, hg, hf', hg'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have trans : f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots))
Tactic: trans ((f.roots ×ˢ g.roots).map fun ij ↦ (-1) * (ij.2 - ij.1)).prod
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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))
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have 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)))
Tactic: trans ((f.roots ×ˢ g.roots).map fun ij ↦ (-1) * (ij.2 - ij.1)).prod
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots))
have 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)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have 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))
Tactic: generalize hN : f.natDegree + g.natDegree = N
-- 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
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have pos : ∀ (hr : g ∣ f), 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
-- 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
pos : ∀ (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))
have neg : ∀ (hr : ¬g ∣ f), 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
-- 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
⊢ f.resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots))
have 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))
Tactic: obtain ⟨r, rfl⟩ := hr
Cleared hypotheses: f, hf, hf', hfg, hN, hr
-- 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
⊢ (g * r).resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
have hr' : r ≠ 0
Tactic: have hr' : r ≠ 0 := by simpa [hg.ne_zero] using hf.ne_zero
-- 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).resultant g = Multiset.prod (Multiset.map (fun (ij : K × K) ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots))
have 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))
Tactic: rw [← resultant_add_mul_left _ _ (-r) _ _ _ le_rfl]