Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
⊢ (if j = f.natDegree - 2 then f.coeff f.natDegree
    else if j = 2 * f.natDegree - 2 then f.coeff f.natDegree * ↑f.natDegree else 0) =
    if j < f.natDegree - 1 then
      if j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2 then f.coeff (2 * f.natDegree - 2 - j) else 0
    else
      if
          j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧
            2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2 then
        f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
          (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + 1)
      else 0

Tactic:
split_ifs

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝² : j = f.natDegree - 2
h✝¹ : j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2
⊢ f.coeff f.natDegree = f.coeff (2 * f.natDegree - 2 - j)

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝² : j = f.natDegree - 2
h✝¹ : j < f.natDegree - 1
h✝ : ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2)
⊢ f.coeff f.natDegree = 0

case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝² : j = f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) * (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + 1)

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝² : j = f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : ¬(j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2)
⊢ f.coeff f.natDegree = 0

case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : j = 2 * f.natDegree - 2
h✝¹ : j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2
⊢ f.coeff f.natDegree * ↑f.natDegree = f.coeff (2 * f.natDegree - 2 - j)

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : j = 2 * f.natDegree - 2
h✝¹ : j < f.natDegree - 1
h✝ : ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2)
⊢ f.coeff f.natDegree * ↑f.natDegree = 0

case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : j = 2 * f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree * ↑f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) * (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + 1)

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : j = 2 * f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : ¬(j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2)
⊢ f.coeff f.natDegree * ↑f.natDegree = 0

case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : ¬j = 2 * f.natDegree - 2
h✝¹ : j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2
⊢ 0 = f.coeff (2 * f.natDegree - 2 - j)

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : ¬j = 2 * f.natDegree - 2
h✝¹ : j < f.natDegree - 1
h✝ : ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2)
⊢ 0 = 0

case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : ¬j = 2 * f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ 0 =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) * (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + 1)

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : ¬j = 2 * f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : ¬(j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2)
⊢ 0 = 0