Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

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

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

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

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

Tactic:
<;>

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

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

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

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

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