Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i j : Fin (m + k)
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map i))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation j) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑j ∈ Set.Icc (↑j₁) (↑j₁ + k) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inr)))
                  (freeMonic R k)).coeff
              (↑j - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑j ∈ Set.Icc (↑j₁) (↑j₁ + m) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inl)))
                  (freeMonic R m)).coeff
              (↑j - ↑j₁)
          else 0)
        ((finCongr ⋯) i)

Tactic:
obtain ⟨i | i, rfl⟩ := finSumFinEquiv.surjective i <;>
    induction j using Fin.addCases <;>
      simp [pderiv_map, coeff_freeMonic, apply_dite (DFunLike.coe _), apply_ite (DFunLike.coe _),
        pderiv_inl_universalFactorizationMap_X, pderiv_inr_universalFactorizationMap_X]

Goal state after:
case inl.left
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin m
⊢ (if i✝ < i then 0 else if h : ↑i✝ - ↑i < k then X (Sum.inr ⟨↑i✝ - ↑i, ⋯⟩) else if ↑i✝ - ↑i = k then 1 else 0) =
    if i ≤ i✝ ∧ ↑i✝ ≤ ↑i + k then if h : ↑i✝ - ↑i < k then X (Sum.inr ⟨↑i✝ - ↑i, h⟩) else if ↑i✝ - ↑i = k then 1 else 0
    else 0

case inl.right
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin m
i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = k then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + k then
      if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = k then 1 else 0
    else 0

case inr.left
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin k
i✝ : Fin m
⊢ (if ↑i✝ < ↑i then 0 else if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, ⋯⟩) else if ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ ↑i✝ ∧ ↑i✝ ≤ ↑i + m then
      if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, h⟩) else if ↑i✝ - ↑i = m then 1 else 0
    else 0

case inr.right
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + m then
      if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = m then 1 else 0
    else 0