awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hf : Monic.{u_1} (R := R) 1
hf0 : natDegree.{u_1} (R := R) 1 = 0
⊢ IsUnit (resultant 1 g) ↔ IsCoprime 1 g

Tactic:
simp [isCoprime_one_left]

Premises used: isCoprime_one_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g

Tactic:
⟨fun H ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
neg : ∀ (H : IsUnit (f.resultant g)), IsCoprime f g
neg₁ : IsCoprime f g → IsUnit (f.resultant g)
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g

Tactic:
refine ⟨fun H ↦ ?_, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
H : IsUnit (f.resultant g)
⊢ f.natDegree ≠ 0 ∨ g.natDegree ≠ 0

Tactic:
simp [hf0]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
H : IsUnit (f.resultant g)
neg :
  ∀ (p q : R[X]) (hp : p.degree < (↑g.natDegree : WithBot ℕ)) (hq : q.degree < (↑f.natDegree : WithBot ℕ))
    (e : f * p + g * q = (C : (a : R) → R[X]) (f.resultant g)), IsCoprime f g
⊢ IsCoprime f g

Tactic:
obtain ⟨p, q, hp, hq, e⟩ := exists_mul_add_mul_eq_C_resultant f g le_rfl le_rfl (by simp [hf0])

Premises used: le_rfl, Polynomial.exists_mul_add_mul_eq_C_resultant
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
H : IsUnit (f.resultant g)
p q : R[X]
hp : p.degree < (↑g.natDegree : WithBot ℕ)
hq : q.degree < (↑f.natDegree : WithBot ℕ)
e : f * p + g * q = (C : (a : R) → R[X]) (f.resultant g)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑H.unit⁻¹ : R) : R[X]) p * f +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑H.unit⁻¹ : R) : R[X]) q * g =
    1

Tactic:
simp only [mul_assoc, ← mul_add, mul_comm p,
      mul_comm q, e, ← map_mul, IsUnit.val_inv_mul, map_one]

Premises used: mul_assoc, map_mul, map_one, mul_comm, mul_add, IsUnit.val_inv_mul
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
H : IsUnit (f.resultant g)
p q : R[X]
hp : p.degree < (↑g.natDegree : WithBot ℕ)
hq : q.degree < (↑f.natDegree : WithBot ℕ)
e : f * p + g * q = (C : (a : R) → R[X]) (f.resultant g)
⊢ IsCoprime f g

Tactic:
exact ⟨C (H.unit⁻¹).1 * p, C (H.unit⁻¹).1 * q, by simp only [mul_assoc, ← mul_add, mul_comm p,
      mul_comm q, e, ← map_mul, IsUnit.val_inv_mul, map_one]⟩
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
neg : 1 = f.resultant b * f.resultant g
⊢ IsUnit (f.resultant g)

Tactic:
suffices 1 = f.resultant b * f.resultant g from isUnit_iff_exists_inv'.mpr ⟨_, this.symm⟩
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
⊢ f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g

Tactic:
have := resultant_mul_right f b g _ le_rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
neg : ∀ (e : 0 * f + b * g = 1), 1 = f.resultant b * f.resultant g
neg₁ : ∀ (hb0 : a ≠ 0), 1 = f.resultant b * f.resultant g
⊢ 1 = f.resultant b * f.resultant g

Tactic:
obtain rfl | hb0 := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
b : R[X]
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
e : 0 * f + b * g = 1
⊢ b * g = 1

Tactic:
simpa using e
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
b : R[X]
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
e : 0 * f + b * g = 1
⊢ f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g

Tactic:
rw [show b * g = 1 by simpa using e, resultant_one_right] at this

Premises used: Polynomial.resultant_one_right
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
b : R[X]
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
e : 0 * f + b * g = 1
this₁ : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ 0 * f + b * g = 1

Tactic:
rw [show b * g = 1 by simpa using e, resultant_one_right] at this

Premises used: Polynomial.resultant_one_right
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
b : R[X]
this : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
e : 0 * f + b * g = 1
⊢ 1 = f.resultant b * f.resultant g

Tactic:
simpa [hf.leadingCoeff] using this

Premises used: Polynomial.Monic.leadingCoeff
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
neg :
  ∀
    (this :
      f.resultant ((C : (a : R) → R[X]) 1) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g)
    (hb0 : a ≠ 0), 1 = f.resultant b * f.resultant g
rw : a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
⊢ 1 = f.resultant b * f.resultant g

Tactic:
rw [← resultant_add_mul_right _ _ a _ _ _ le_rfl, add_comm, mul_comm, e, ← C.map_one] at this

Premises used: Polynomial.C, le_rfl, RingHom.map_one, add_comm, Polynomial.resultant_add_mul_right, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant ((C : (a : R) → R[X]) 1) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g

Tactic:
simpa [hf.leadingCoeff] using this

Premises used: Polynomial.Monic.leadingCoeff
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
by_contra! : ∀ (H : b.natDegree + g.natDegree < a.natDegree + f.natDegree), False
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
by_contra! H
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : b.natDegree + g.natDegree < a.natDegree + f.natDegree
⊢ (b * g).natDegree < a.natDegree + f.natDegree

Tactic:
replace H := natDegree_mul_le.trans_lt H
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < a.natDegree + f.natDegree
⊢ (b * g).natDegree < (a * f).natDegree

Tactic:
rw [add_comm, ← hf.natDegree_mul' hb0, mul_comm f] at H

Premises used: add_comm, mul_comm, Polynomial.Monic.natDegree_mul'
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < (a * f).natDegree
⊢ (a * f + b * g).natDegree = (a * f).natDegree

Tactic:
have := natDegree_add_eq_left_of_natDegree_lt H
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this_1 : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < (a * f).natDegree
this : (a * f + b * g).natDegree = (a * f).natDegree
⊢ 0 = (a * f).natDegree

Tactic:
simp only [e, natDegree_one] at this

Premises used: Polynomial.natDegree_one
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this_1 : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < (a * f).natDegree
this : 0 = (a * f).natDegree
⊢ False

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
inl : resultant 0 g = 0 ↔ (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g
inr : ∀ (hf : f ≠ 0), f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g

Tactic:
obtain rfl | hf := eq_or_ne f 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
g : K[X]
inl :
  Eq.{u_2 + 1} (α := K) (resultant 0 0) 0 ↔
    (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ Ne.{u_2 + 1} (α := K[X]) 0 0) ∧ ¬IsCoprime.{u_2} (R := K[X]) 0 0
inl₁ : ∀ (hg : g ≠ 0), resultant 0 g = 0 ↔ (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g
⊢ resultant 0 g = 0 ↔ (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g

Tactic:
obtain rfl | hg := eq_or_ne g 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
⊢ Eq.{u_2 + 1} (α := K) (resultant 0 0) 0 ↔
    (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ Ne.{u_2 + 1} (α := K[X]) 0 0) ∧ ¬IsCoprime.{u_2} (R := K[X]) 0 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
g : K[X]
hg : g ≠ 0
⊢ (∀ (x : K), (C : (a : K) → K[X]) x ≠ g) ↔ ∀ (x : K), x ≠ 0 → (C : (a : K) → K[X]) x ≠ g

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
g : K[X]
hg : g ≠ 0
⊢ resultant 0 g = 0 ↔ (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g

Tactic:
simpa [isCoprime_zero_left, isUnit_iff, hg, natDegree_eq_zero] using
      show (∀ x, C x ≠ g) ↔ ∀ x ≠ 0, C x ≠ g by aesop

Premises used: Polynomial.isUnit_iff, isCoprime_zero_left, Polynomial.natDegree_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
⊢ f.leadingCoeff⁻¹ ≠ 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
rw : f.leadingCoeff⁻¹ * f.coeff f.natDegree = 1
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic

Tactic:
rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simpa), coeff_C_mul]

Premises used: Polynomial.coeff_natDegree, Polynomial.coeff_C_mul, Polynomial.natDegree_C_mul, Polynomial.Monic
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
⊢ f.leadingCoeff⁻¹ * f.coeff f.natDegree = 1

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic

Tactic:
have H : (C f.leadingCoeff⁻¹ * f).Monic := by
    rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simpa), coeff_C_mul]; simp [hf]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
H : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic
⊢ IsUnit ((HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).resultant g) ↔
    IsCoprime (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f) g

Tactic:
have := isUnit_resultant_iff_isCoprime (f := C f.leadingCoeff⁻¹ * f) (g := g) H
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
H : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic
this :
  IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧
      IsUnit (f.resultant g (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).natDegree) ↔
    IsCoprime (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f) g
⊢ f.leadingCoeff⁻¹ ≠ 0

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
H : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic
this :
  IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔
    IsCoprime (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f) g
⊢ IsUnit f.leadingCoeff⁻¹

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
H : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic
this :
  IsUnit ((HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).resultant g) ↔
    IsCoprime (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f) g
⊢ IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔ IsCoprime f g

Tactic:
rw [resultant_C_mul_left, IsUnit.mul_iff, natDegree_C_mul (by simp [hf]),
    isCoprime_mul_unit_left_left (isUnit_C.mpr (by simp [hf]))] at this

Premises used: IsUnit.mul_iff, isCoprime_mul_unit_left_left, Polynomial.natDegree_C_mul, Polynomial.resultant_C_mul_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
H : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic
this : IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔ IsCoprime f g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g

Tactic:
simp [← this, hf]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) - 1 + 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
r : R
e : Fin (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) - 1 + natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r)) ≃
  Fin 0 :=
  finCongr ⋯
⊢ Eq.{u_1 + 1} (α := R) (discr ((C : (a : R) → R[X]) r)) 1

Tactic:
simp [discr, ← Matrix.det_reindex_self e]

Premises used: Matrix.det_reindex_self, Polynomial.discr
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.degree = 1
⊢ f.natDegree = 1

Tactic:
rw [← Nat.cast_one, degree_eq_iff_natDegree_eq_of_pos one_pos] at hf

Premises used: Polynomial.degree_eq_iff_natDegree_eq_of_pos, Nat.cast_one, one_pos
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
⊢ f.natDegree - 1 + f.natDegree = 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
⊢ f.natDegree - 1 + f.natDegree ≠ 0

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
⊢ NeZero (f.natDegree - 1 + f.natDegree)

Tactic:
have : NeZero (f.natDegree - 1 + f.natDegree) := ⟨by lia⟩
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
a :
  ∀ (i : ℕ) (hi : i < 1) (j : ℕ) (hj : j < 1),
    Eq (α := R)
      ((Matrix.reindex e e :
            (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
              Matrix (Fin 1) (Fin 1) R)
          f.sylvesterDeriv ⟨i, hi⟩ ⟨j, hj⟩ :
        R)
      (!![1] ⟨i, hi⟩ ⟨j, hj⟩ : R)
⊢ Eq (α := Matrix (Fin 1) (Fin 1) R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv :
      Matrix (Fin 1) (Fin 1) R)
    (!![1] : Matrix (Fin 1) (Fin 1) R)

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
i : ℕ
hi : i < 1
j : ℕ
hj : j < 1
⊢ i = 0

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
i : ℕ
hi : i < 1
j : ℕ
hj : j < 1
a :
  ∀ (hi : LT.lt (α := ℕ) 0 1),
    Eq (α := R)
      ((Matrix.reindex e e :
            (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
              Matrix (Fin 1) (Fin 1) R)
          f.sylvesterDeriv ⟨0, hi⟩ ⟨j, hj⟩ :
        R)
      (!![1] ⟨0, hi⟩ ⟨j, hj⟩ : R)
⊢ Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv ⟨i, hi⟩ ⟨j, hj⟩ :
      R)
    (!![1] ⟨i, hi⟩ ⟨j, hj⟩ : R)

Tactic:
obtain ⟨rfl⟩ : i = 0 := by lia

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
j : ℕ
hj : j < 1
hi : LT.lt (α := ℕ) 0 1
⊢ j = 0

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
j : ℕ
hj : j < 1
hi : LT.lt (α := ℕ) 0 1
a :
  ∀ (hj : LT.lt (α := ℕ) 0 1),
    Eq (α := R)
      ((Matrix.reindex e e :
            (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
              Matrix (Fin 1) (Fin 1) R)
          f.sylvesterDeriv ⟨0, hi⟩ ⟨0, hj⟩ :
        R)
      (!![1] ⟨0, hi⟩ ⟨0, hj⟩ : R)
⊢ Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv ⟨0, hi⟩ ⟨j, hj⟩ :
      R)
    (!![1] ⟨0, hi⟩ ⟨j, hj⟩ : R)

Tactic:
obtain ⟨rfl⟩ : j = 0 := by lia

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
hi hj : LT.lt (α := ℕ) 0 1
⊢ Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv ⟨0, hi⟩ ⟨0, hj⟩ :
      R)
    (!![1] ⟨0, hi⟩ ⟨0, hj⟩ : R)

Tactic:
simp [e, sylvesterDeriv, mul_comm, hf]

Premises used: mul_comm, Polynomial.sylvesterDeriv
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
⊢ Eq (α := Matrix (Fin 1) (Fin 1) R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv :
      Matrix (Fin 1) (Fin 1) R)
    (!![1] : Matrix (Fin 1) (Fin 1) R)

Tactic:
have : f.sylvesterDeriv.reindex e e = !![1] := by
    have : NeZero (f.natDegree - 1 + f.natDegree) := ⟨by lia⟩
    ext ⟨i, hi⟩ ⟨j, hj⟩
    obtain ⟨rfl⟩ : i = 0 := by lia
    obtain ⟨rfl⟩ : j = 0 := by lia
    simp [e, sylvesterDeriv, mul_comm, hf]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this :
  Eq (α := Matrix (Fin 1) (Fin 1) R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv :
      Matrix (Fin 1) (Fin 1) R)
    (!![1] : Matrix (Fin 1) (Fin 1) R)
⊢ f.discr = 1

Tactic:
simp [discr, ← Matrix.det_reindex_self e, this, hf]

Premises used: Matrix.det_reindex_self, Polynomial.discr
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.degree = 2
⊢ f.natDegree = 2

Tactic:
rw [← Nat.cast_two, degree_eq_iff_natDegree_eq_of_pos two_pos] at hf

Premises used: two_pos, Polynomial.degree_eq_iff_natDegree_eq_of_pos, Nat.cast_two
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 2
⊢ f.natDegree - 1 + f.natDegree = 3

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
rw :
  Matrix.det (n := Fin 3)
        ((Matrix.reindex e e :
            (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
              Matrix (Fin 3) (Fin 3) R)
          f.sylvesterDeriv) *
      HPow.hPow (α := R) (-1) (f.natDegree * (f.natDegree - 1) / 2) =
    HPow.hPow (β := ℕ) (f.coeff 1) 2 - 4 * f.coeff 0 * f.coeff 2
⊢ f.discr = HPow.hPow (β := ℕ) (f.coeff 1) 2 - 4 * f.coeff 0 * f.coeff 2

Tactic:
rw [discr, ← Matrix.det_reindex_self e]

Premises used: Matrix.det_reindex_self, Polynomial.discr
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
a :
  ∀ (i j : Fin 3),
    Eq (α := R)
      ((Matrix.reindex e e :
            (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
              Matrix (Fin 3) (Fin 3) R)
          f.sylvesterDeriv i j :
        R)
      (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] i j : R)
⊢ Eq (α := Matrix (Fin 3) (Fin 3) R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 3) (Fin 3) R)
        f.sylvesterDeriv :
      Matrix (Fin 3) (Fin 3) R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] : Matrix (Fin 3) (Fin 3) R)

Tactic:
ext i j