awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⋯
i j : Fin 3
a :
  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 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : R)
a₁ :
  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 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : R)
a₂ :
  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 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : R)
⊢ 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)

Tactic:
fin_cases i
-- 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 ⋯
j : Fin 3
a :
  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 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)
a₁ :
  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 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)
a₂ :
  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 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : R)

Tactic:
fin_cases j
-- 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 ⋯
j : Fin 3
a :
  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 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)
a₁ :
  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 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)
a₂ :
  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 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : R)

Tactic:
fin_cases j
-- 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 ⋯
j : Fin 3
a :
  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 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)
a₁ :
  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 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)
a₂ :
  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 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : R)

Tactic:
fin_cases j
-- 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 ⋯
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)

Tactic:
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Premises used: Polynomial.coeff_derivative, one_add_one_eq_two, Fin.cast, Polynomial.sylvester, mul_comm, Polynomial.sylvesterDeriv
-- 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 ⋯
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)

Tactic:
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Premises used: Polynomial.coeff_derivative, one_add_one_eq_two, Fin.cast, Polynomial.sylvester, mul_comm, Polynomial.sylvesterDeriv
-- 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 ⋯
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)

Tactic:
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Premises used: Polynomial.coeff_derivative, one_add_one_eq_two, Fin.cast, Polynomial.sylvester, mul_comm, Polynomial.sylvesterDeriv
-- 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 ⋯
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)

Tactic:
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Premises used: Polynomial.coeff_derivative, one_add_one_eq_two, Fin.cast, Polynomial.sylvester, mul_comm, Polynomial.sylvesterDeriv
-- 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 ⋯
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)

Tactic:
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Premises used: Polynomial.coeff_derivative, one_add_one_eq_two, Fin.cast, Polynomial.sylvester, mul_comm, Polynomial.sylvesterDeriv
-- 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 ⋯
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)

Tactic:
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Premises used: Polynomial.coeff_derivative, one_add_one_eq_two, Fin.cast, Polynomial.sylvester, mul_comm, Polynomial.sylvesterDeriv
-- 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 ⋯
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) :
      R)

Tactic:
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Premises used: Polynomial.coeff_derivative, one_add_one_eq_two, Fin.cast, Polynomial.sylvester, mul_comm, Polynomial.sylvesterDeriv
-- 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 ⋯
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) :
      R)

Tactic:
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Premises used: Polynomial.coeff_derivative, one_add_one_eq_two, Fin.cast, Polynomial.sylvester, mul_comm, Polynomial.sylvesterDeriv
-- 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 ⋯
⊢ 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 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) :
      R)

Tactic:
simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Premises used: Polynomial.coeff_derivative, one_add_one_eq_two, Fin.cast, Polynomial.sylvester, mul_comm, Polynomial.sylvesterDeriv
-- 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 ⋯
⊢ 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:
have : f.sylvesterDeriv.reindex e e =
    !![f.coeff 0,     f.coeff 1,         0;
        f.coeff 1, 2 * f.coeff 2, f.coeff 1;
        1,                     0,         2] := by
    ext i j
    fin_cases i <;> fin_cases j <;>
      simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]
-- 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 ⋯
this :
  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)
simp :
  (f.coeff 0 * (2 * f.coeff 2) * 2 - f.coeff 0 * f.coeff 1 * 0 - f.coeff 1 * f.coeff 1 * 2 + f.coeff 1 * f.coeff 1 * 1 +
          0 * f.coeff 1 * 0 -
        0 * (2 * f.coeff 2) * 1) *
      HPow.hPow (α := R) (-1) (2 * HSub.hSub (α := ℕ) 2 1 / 2) =
    HPow.hPow (β := ℕ) (f.coeff 1) 2 - 4 * f.coeff 0 * f.coeff 2
⊢ 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

Tactic:
simp only [this, Matrix.det_fin_three, Matrix.of_apply, Matrix.cons_val', Matrix.cons_val_zero,
    Matrix.cons_val_fin_one, Matrix.cons_val_one, Matrix.cons_val, hf]

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val_fin_one, Matrix.of_apply, Matrix.cons_val, Matrix.det_fin_three, Matrix.cons_val'
-- 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 ⋯
this :
  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)
⊢ (f.coeff 0 * (2 * f.coeff 2) * 2 - f.coeff 0 * f.coeff 1 * 0 - f.coeff 1 * f.coeff 1 * 2 + f.coeff 1 * f.coeff 1 * 1 +
          0 * f.coeff 1 * 0 -
        0 * (2 * f.coeff 2) * 1) *
      HPow.hPow (α := R) (-1) (2 * HSub.hSub (α := ℕ) 2 1 / 2) =
    HPow.hPow (β := ℕ) (f.coeff 1) 2 - 4 * f.coeff 0 * f.coeff 2

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : 0 < f.degree
⊢ 0 < f.natDegree

Tactic:
rw [← natDegree_pos_iff_degree_pos] at hf

Premises used: Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : 0 < f.natDegree
rw :
  HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree) * (f.leadingCoeff * f.sylvesterDeriv.det) =
    HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree / 2) * f.leadingCoeff *
      (f.sylvesterDeriv.det * HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree / 2))
⊢ f.resultant ((derivative : (a : R[X]) → R[X]) f) f.natDegree (f.natDegree - 1) =
    HPow.hPow (α := R) (-1) (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff * f.discr

Tactic:
rw [resultant_comm, resultant, ← sylvesterDeriv_updateRow f hf, Matrix.det_updateRow_smul,
    Matrix.updateRow_eq_self, discr, mul_comm f.natDegree]

Premises used: Polynomial.resultant, Polynomial.resultant_comm, Polynomial.sylvesterDeriv_updateRow, Polynomial.discr, mul_comm, Matrix.updateRow_eq_self, Matrix.det_updateRow_smul, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : 0 < f.natDegree
ring_nf :
  f.leadingCoeff * f.sylvesterDeriv.det * HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree) =
    f.leadingCoeff * f.sylvesterDeriv.det * HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree / 2 * 2)
⊢ HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree) * (f.leadingCoeff * f.sylvesterDeriv.det) =
    HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree / 2) * f.leadingCoeff *
      (f.sylvesterDeriv.det * HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree / 2))

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ 2 ∣ (f.natDegree - 1) * (f.natDegree - 1 + 1)

Tactic:
Nat.two_dvd_mul_add_one (f.natDegree - 1)

Premises used: HSub.hSub, Nat.two_dvd_mul_add_one, Polynomial.natDegree, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : 0 < f.natDegree
h : f.natDegree = f.natDegree - 1 + 1
⊢ 2 ∣ (f.natDegree - 1) * f.natDegree

Tactic:
convert! Nat.two_dvd_mul_add_one (f.natDegree - 1) using 2

Premises used: HSub.hSub, Nat.two_dvd_mul_add_one, Polynomial.natDegree, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ f.natDegree = f.natDegree - 1 + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : 0 < f.natDegree
rw rw₁ :
  f.leadingCoeff * f.sylvesterDeriv.det * HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree) =
    f.leadingCoeff * f.sylvesterDeriv.det * HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree)
⊢ f.leadingCoeff * f.sylvesterDeriv.det * HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree) =
    f.leadingCoeff * f.sylvesterDeriv.det * HPow.hPow (α := R) (-1) ((f.natDegree - 1) * f.natDegree / 2 * 2)

Tactic:
rw [Nat.div_mul_cancel (by convert! Nat.two_dvd_mul_add_one (f.natDegree - 1) using 2; lia)]

Premises used: Nat.div_mul_cancel
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
rw rw₁ : HSub.hSub (α := ℕ) 3 1 + 3 = 5
⊢ f.natDegree - 1 + f.natDegree = 5

Tactic:
rw [hf]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 3
a :
  ∀ (i : ℕ) (hi : i < 5) (j : ℕ) (hj : j < 5),
    Eq (α := R)
      (((Matrix.reindex (finCongr ⋯) (finCongr ⋯) :
              Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R ≃
                Matrix (Fin 5) (Fin 5) R) :
            (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
              Matrix (Fin 5) (Fin 5) R)
          f.sylvesterDeriv ⟨i, hi⟩ ⟨j, hj⟩ :
        R)
      (!![f.coeff 0, 0, 1 * f.coeff 1, 0, 0;
            f.coeff 1, f.coeff 0, 2 * f.coeff 2, 1 * f.coeff 1, 0;
            f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, 1 * f.coeff 1;
            f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2;
            0, 1, 0, 0, 3]
          ⟨i, hi⟩ ⟨j, hj⟩ :
        R)
⊢ Eq (α := Matrix (Fin 5) (Fin 5) R)
    (((Matrix.reindex (finCongr ⋯) (finCongr ⋯) :
            Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R ≃
              Matrix (Fin 5) (Fin 5) R) :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 5) (Fin 5) R)
        f.sylvesterDeriv :
      Matrix (Fin 5) (Fin 5) R)
    (!![f.coeff 0, 0, 1 * f.coeff 1, 0, 0;
        f.coeff 1, f.coeff 0, 2 * f.coeff 2, 1 * f.coeff 1, 0;
        f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, 1 * f.coeff 1;
        f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2;
        0, 1, 0, 0, 3] :
      Matrix (Fin 5) (Fin 5) R)

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩