Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «2».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 2 then f.coeff (2 - 0) else 0
    else if 0 ≤ 4 then f.coeff (2 - (0 - 2) + 1) * (↑(2 - (0 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨0, hj⟩

pp: case «2».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 2 then f.coeff (2 - 1) else 0
    else if 1 ≤ 4 then f.coeff (2 - (1 - 2) + 1) * (↑(2 - (1 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨1, hj⟩

pp: case «2».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 2 then f.coeff (2 - 2) else 0
    else if 2 ≤ 4 then f.coeff (2 - (2 - 2) + 1) * (↑(2 - (2 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨2, hj⟩

pp: case «2».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 2 then f.coeff (2 - 3) else 0
    else if 3 ≤ 4 then f.coeff (2 - (3 - 2) + 1) * (↑(2 - (3 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨3, hj⟩

pp: case «2».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 2 then f.coeff (2 - 4) else 0
    else if 4 ≤ 4 then f.coeff (2 - (4 - 2) + 1) * (↑(2 - (4 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨4, hj⟩

Tactic:
<;>

Goal state after:
case «2».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 2 then f.coeff (2 - 0) else 0
    else if 0 ≤ 4 then f.coeff (2 - (0 - 2) + 1) * (↑(2 - (0 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨0, hj⟩

case «2».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 2 then f.coeff (2 - 1) else 0
    else if 1 ≤ 4 then f.coeff (2 - (1 - 2) + 1) * (↑(2 - (1 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨1, hj⟩

case «2».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 2 then f.coeff (2 - 2) else 0
    else if 2 ≤ 4 then f.coeff (2 - (2 - 2) + 1) * (↑(2 - (2 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨2, hj⟩

case «2».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 2 then f.coeff (2 - 3) else 0
    else if 3 ≤ 4 then f.coeff (2 - (3 - 2) + 1) * (↑(2 - (3 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨3, hj⟩

case «2».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 2 then f.coeff (2 - 4) else 0
    else if 4 ≤ 4 then f.coeff (2 - (4 - 2) + 1) * (↑(2 - (4 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨4, hj⟩