Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «0».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

pp: case «1».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

pp: case «2».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «2».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «0».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

case «1».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

case «2».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «2».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «2».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)