Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inl
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
j : Fin (m + k)
i : Fin m
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inl 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 ⋯) (finSumFinEquiv (Sum.inl i)))

pp: case inr
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
j : Fin (m + k)
i : Fin k
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inr 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 ⋯) (finSumFinEquiv (Sum.inr i)))

Tactic:
<;>

Goal state after:
case inl
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
j : Fin (m + k)
i : Fin m
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inl 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 ⋯) (finSumFinEquiv (Sum.inl i)))

case inr
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
j : Fin (m + k)
i : Fin k
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inr 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 ⋯) (finSumFinEquiv (Sum.inr i)))