-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
trans :
  Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
    ((pderiv (Sum.inr i) : (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
        ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((universalFactorizationMap R n m k hn :
              (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X j))) :
      MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
        if x.2 < k then
          if h : x.1 < m then if x.2 = (↑i : ℕ) then X (Sum.inl ⟨x.1, h⟩) else 0
          else if x.1 = m ∧ x.2 = (↑i : ℕ) then 1 else 0
        else 0 :
      MvPolynomial (Fin m ⊕ Fin k) R)
trans₁ trans₂ :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if x.2 < k then
        if h : x.1 < m then if x.2 = (↑i : ℕ) then X (Sum.inl ⟨x.1, h⟩) else 0
        else if x.1 = m ∧ x.2 = (↑i : ℕ) then 1 else 0
      else 0)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑j : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
      else if (↑j : ℕ) - (↑i : ℕ) = m then 1 else 0)
⊢ Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
    ((pderiv (Sum.inr i) : (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
        ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((universalFactorizationMap R n m k hn :
              (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X j))) :
      MvPolynomial (Fin m ⊕ Fin k) R)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
      else
        if h : (↑j : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
        else if (↑j : ℕ) - (↑i : ℕ) = m then 1 else 0 :
      MvPolynomial (Fin m ⊕ Fin k) R)

Tactic:
classical
  trans ∑ x ∈ Finset.antidiagonal ↑j, if x.2 < k then if h : x.1 < m then if x.2 = ↑i then
    X (Sum.inl ⟨x.1, h⟩) else 0 else if x.1 = m ∧ x.2 = ↑i then 1 else 0 else 0
  · simp [universalFactorizationMap, mapEquivMonic, Polynomial.coeff_mul, coeff_freeMonic,
      apply_dite, apply_ite, ← Algebra.TensorProduct.one_def,
      Pi.single_apply, Fin.ext_iff, ← ite_and]
  · obtain h | h := lt_or_ge j.1 i.1
    · rw [Finset.sum_eq_zero, if_pos h]
      simp only [Finset.mem_antidiagonal]
      lia
    rw [Finset.sum_eq_single ⟨j.1 - i.1, i.1⟩, if_neg h.not_gt]
    · simp
    · simp only [Finset.mem_antidiagonal, ne_eq, ite_eq_right_iff, Prod.forall, Prod.mk.injEq]
      intro a b _ _ _
      simp [show b ≠ i by lia]
    · simp [h]

Premises used: apply_dite, Fin.ext_iff, Pi.single_apply, Finset.sum_eq_zero, MvPolynomial.X, apply_ite, Polynomial.coeff_mul, Sum.inl, Fin.val, ne_eq, Finset.sum_eq_single, MvPolynomial.universalFactorizationMap, Finset.HasAntidiagonal.mem_antidiagonal, ite_eq_right_iff, Prod.mk.injEq, MvPolynomial.mapEquivMonic, Prod.forall, lt_or_ge, ite_and, Finset.HasAntidiagonal.antidiagonal, Algebra.TensorProduct.one_def, Polynomial.coeff_freeMonic