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

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
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inl i))))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation (Fin.castAdd k i✝)) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑(Fin.castAdd k i✝) ∈ 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
              (↑(Fin.castAdd k i✝) - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑(Fin.castAdd k i✝) ∈ 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
              (↑(Fin.castAdd k i✝) - ↑j₁)
          else 0)
        ((finCongr ⋯) (finSumFinEquiv (Sum.inl i)))

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
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inl i))))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation (Fin.natAdd m i✝)) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑(Fin.natAdd m i✝) ∈ 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
              (↑(Fin.natAdd m i✝) - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑(Fin.natAdd m i✝) ∈ 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
              (↑(Fin.natAdd m i✝) - ↑j₁)
          else 0)
        ((finCongr ⋯) (finSumFinEquiv (Sum.inl i)))

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
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inr i))))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation (Fin.castAdd k i✝)) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑(Fin.castAdd k i✝) ∈ 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
              (↑(Fin.castAdd k i✝) - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑(Fin.castAdd k i✝) ∈ 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
              (↑(Fin.castAdd k i✝) - ↑j₁)
          else 0)
        ((finCongr ⋯) (finSumFinEquiv (Sum.inr i)))

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
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inr i))))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation (Fin.natAdd m i✝)) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑(Fin.natAdd m i✝) ∈ 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
              (↑(Fin.natAdd m i✝) - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑(Fin.natAdd m i✝) ∈ 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
              (↑(Fin.natAdd m i✝) - ↑j₁)
          else 0)
        ((finCongr ⋯) (finSumFinEquiv (Sum.inr i)))