Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
⊢ (if 0 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 0 ∧ 0 ≤ j + 3 then f.coeff (0 - j) else 0
      else if j ≤ 0 + 2 ∧ 0 ≤ j - 2 + 2 then f.coeff (0 - (j - 2) + 1) * (↑(0 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨0, hi⟩

pp: case «1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
⊢ (if 1 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 1 ∧ 1 ≤ j + 3 then f.coeff (1 - j) else 0
      else if j ≤ 1 + 2 ∧ 1 ≤ j - 2 + 2 then f.coeff (1 - (j - 2) + 1) * (↑(1 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨1, hi⟩

pp: case «2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 2 < 5
⊢ (if 2 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 2 ∧ 2 ≤ j + 3 then f.coeff (2 - j) else 0
      else if j ≤ 2 + 2 ∧ 2 ≤ j - 2 + 2 then f.coeff (2 - (j - 2) + 1) * (↑(2 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨2, hi⟩

pp: case «3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 3 < 5
⊢ (if 3 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 3 ∧ 3 ≤ j + 3 then f.coeff (3 - j) else 0
      else if j ≤ 3 + 2 ∧ 3 ≤ j - 2 + 2 then f.coeff (3 - (j - 2) + 1) * (↑(3 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨3, hi⟩

pp: case «4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 4 < 5
⊢ (if 4 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 4 ∧ 4 ≤ j + 3 then f.coeff (4 - j) else 0
      else if j ≤ 4 + 2 ∧ 4 ≤ j - 2 + 2 then f.coeff (4 - (j - 2) + 1) * (↑(4 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨4, hi⟩

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
⊢ (if 0 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 0 ∧ 0 ≤ j + 3 then f.coeff (0 - j) else 0
      else if j ≤ 0 + 2 ∧ 0 ≤ j - 2 + 2 then f.coeff (0 - (j - 2) + 1) * (↑(0 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨0, hi⟩

case «1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
⊢ (if 1 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 1 ∧ 1 ≤ j + 3 then f.coeff (1 - j) else 0
      else if j ≤ 1 + 2 ∧ 1 ≤ j - 2 + 2 then f.coeff (1 - (j - 2) + 1) * (↑(1 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨1, hi⟩

case «2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 2 < 5
⊢ (if 2 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 2 ∧ 2 ≤ j + 3 then f.coeff (2 - j) else 0
      else if j ≤ 2 + 2 ∧ 2 ≤ j - 2 + 2 then f.coeff (2 - (j - 2) + 1) * (↑(2 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨2, hi⟩

case «3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 3 < 5
⊢ (if 3 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 3 ∧ 3 ≤ j + 3 then f.coeff (3 - j) else 0
      else if j ≤ 3 + 2 ∧ 3 ≤ j - 2 + 2 then f.coeff (3 - (j - 2) + 1) * (↑(3 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨3, hi⟩

case «4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 4 < 5
⊢ (if 4 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 4 ∧ 4 ≤ j + 3 then f.coeff (4 - j) else 0
      else if j ≤ 4 + 2 ∧ 4 ≤ j - 2 + 2 then f.coeff (4 - (j - 2) + 1) * (↑(4 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨4, hi⟩