awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
trans :
  Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
    ((pderiv (Sum.inl 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 h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
        else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0 :
      MvPolynomial (Fin m ⊕ Fin k) R)
⊢ Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
    ((pderiv (Sum.inl 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 : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
        else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0 :
      MvPolynomial (Fin m ⊕ Fin k) R)
have trans₁ : Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
  (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
    if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
    else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
  (if (↑j : ℕ) < (↑i : ℕ) then 0
  else
    if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
    else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
Tactic: trans ∑ x ∈ Finset.antidiagonal ↑j,
    if h : x.2 < k then if x.1 < m ∧ x.1 = ↑i then X (Sum.inr ⟨x.2, h⟩) else 0
    else if x.2 = k ∧ x.1 < m ∧ x.1 = ↑i then 1 else 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
      else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
have inl : ∀ (h : (↑j : ℕ) < (↑i : ℕ)),
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
      else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
Tactic: obtain h | h := lt_or_ge j.1 i.1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
inl :
  ∀ (h : (↑j : ℕ) < (↑i : ℕ)),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
      (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
        if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
        else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
      (if (↑j : ℕ) < (↑i : ℕ) then 0
      else
        if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
        else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
      else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
have inr : ∀ (h : (↑i : ℕ) ≤ (↑j : ℕ)),
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
      else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
Tactic: obtain h | h := lt_or_ge j.1 i.1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
      else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
have inl : ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
    else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
    0
Tactic: rw [Finset.sum_eq_zero, if_pos h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
⊢ ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
      (if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
      0
have inl : ∀ (a b : ℕ),
  a + b = (↑j : ℕ) →
    Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
      (if h : b < k then if a < m ∧ a = (↑i : ℕ) then X (Sum.inr ⟨b, sorry⟩) else 0
      else if b = k ∧ a < m ∧ a = (↑i : ℕ) then 1 else 0)
      0
Tactic: simp only [Finset.mem_antidiagonal, Prod.forall]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : (↑i : ℕ) ≤ (↑j : ℕ)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
      else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
have inr : Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
  (if h : ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2 < k then
    if ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 < m ∧ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 = (↑i : ℕ) then
      X (Sum.inr ⟨((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2, h⟩)
    else 0
  else
    if
        ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2 = k ∧
          ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 < m ∧ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 = (↑i : ℕ) then
      1
    else 0)
  (if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
  else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
Tactic: rw [Finset.sum_eq_single ⟨i.1, j.1 - i.1⟩, if_neg h.not_gt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : (↑i : ℕ) ≤ (↑j : ℕ)
inr :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (if h : ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2 < k then
      if ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 < m ∧ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 = (↑i : ℕ) then
        X (Sum.inr ⟨((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2, h⟩)
      else 0
    else
      if
          ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2 = k ∧
            ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 < m ∧ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 = (↑i : ℕ) then
        1
      else 0)
    (if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
    else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
      else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
have inr₁ : ∀ b ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
  b ≠ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)) →
    Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
      (if h : b.2 < k then if b.1 < m ∧ b.1 = (↑i : ℕ) then X (Sum.inr ⟨b.2, h⟩) else 0
      else if b.2 = k ∧ b.1 < m ∧ b.1 = (↑i : ℕ) then 1 else 0)
      0
Tactic: rw [Finset.sum_eq_single ⟨i.1, j.1 - i.1⟩, if_neg h.not_gt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : (↑i : ℕ) ≤ (↑j : ℕ)
inr :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (if h : ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2 < k then
      if ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 < m ∧ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 = (↑i : ℕ) then
        X (Sum.inr ⟨((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2, h⟩)
      else 0
    else
      if
          ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2 = k ∧
            ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 < m ∧ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 = (↑i : ℕ) then
        1
      else 0)
    (if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
    else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
inr₁ :
  ∀ b ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
    b ≠ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)) →
      Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
        (if h : b.2 < k then if b.1 < m ∧ b.1 = (↑i : ℕ) then X (Sum.inr ⟨b.2, h⟩) else 0
        else if b.2 = k ∧ b.1 < m ∧ b.1 = (↑i : ℕ) then 1 else 0)
        0
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
      if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
    (if (↑j : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
      else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
have inr₂ : ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ) →
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (if h : ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2 < k then
      if ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 < m ∧ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 = (↑i : ℕ) then
        X (Sum.inr ⟨((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2, h⟩)
      else 0
    else
      if
          ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).2 = k ∧
            ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 < m ∧ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)).1 = (↑i : ℕ) then
        1
      else 0)
    0
Tactic: rw [Finset.sum_eq_single ⟨i.1, j.1 - i.1⟩, if_neg h.not_gt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : (↑i : ℕ) ≤ (↑j : ℕ)
⊢ ∀ b ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
    b ≠ ((↑i : ℕ), (↑j : ℕ) - (↑i : ℕ)) →
      Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
        (if h : b.2 < k then if b.1 < m ∧ b.1 = (↑i : ℕ) then X (Sum.inr ⟨b.2, h⟩) else 0
        else if b.2 = k ∧ b.1 < m ∧ b.1 = (↑i : ℕ) then 1 else 0)
        0
have inr : ∀ (a b : ℕ),
  a + b = (↑j : ℕ) →
    (a = (↑i : ℕ) → ¬b = (↑j : ℕ) - (↑i : ℕ)) →
      Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
        (if h : b < k then if a < m ∧ a = (↑i : ℕ) then X (Sum.inr ⟨b, sorry⟩) else 0
        else if b = k ∧ a < m ∧ a = (↑i : ℕ) then 1 else 0)
        0
Tactic: simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
⊢ Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
    ((pderiv (Sum.inl 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 : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
        else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0 :
      MvPolynomial (Fin m ⊕ Fin k) R)
have trans : Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
  ((pderiv (Sum.inl 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 h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
      else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0 :
    MvPolynomial (Fin m ⊕ Fin k) R)
Tactic: classical
  trans ∑ x ∈ Finset.antidiagonal ↑j,
    if h : x.2 < k then if x.1 < m ∧ x.1 = ↑i then X (Sum.inr ⟨x.2, h⟩) else 0
    else if x.2 = k ∧ x.1 < m ∧ x.1 = ↑i then 1 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, Prod.forall]
      intro a b hab
      simp [show a ≠ i by lia]
    rw [Finset.sum_eq_single ⟨i.1, j.1 - i.1⟩, if_neg h.not_gt]
    · simp
    · simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
      intro a b e h
      simp [show a ≠ i by lia]
    · simp [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
trans :
  Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
    ((pderiv (Sum.inl 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 h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
        else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0 :
      MvPolynomial (Fin m ⊕ Fin k) R)
⊢ Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
    ((pderiv (Sum.inl 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 : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
        else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0 :
      MvPolynomial (Fin m ⊕ Fin k) R)
have trans₁ : Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
  (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
    if h : x.2 < k then if x.1 < m ∧ x.1 = (↑i : ℕ) then X (Sum.inr ⟨x.2, h⟩) else 0
    else if x.2 = k ∧ x.1 < m ∧ x.1 = (↑i : ℕ) then 1 else 0)
  (if (↑j : ℕ) < (↑i : ℕ) then 0
  else
    if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
    else if (↑j : ℕ) - (↑i : ℕ) = k then 1 else 0)
Tactic: classical
  trans ∑ x ∈ Finset.antidiagonal ↑j,
    if h : x.2 < k then if x.1 < m ∧ x.1 = ↑i then X (Sum.inr ⟨x.2, h⟩) else 0
    else if x.2 = k ∧ x.1 < m ∧ x.1 = ↑i then 1 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, Prod.forall]
      intro a b hab
      simp [show a ≠ i by lia]
    rw [Finset.sum_eq_single ⟨i.1, j.1 - i.1⟩, if_neg h.not_gt]
    · simp
    · simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
      intro a b e h
      simp [show a ≠ i by lia]
    · simp [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
⊢ 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)
have 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)
Tactic: 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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)
⊢ 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)
have 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)
Tactic: 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
⊢ 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)
have inl : ∀ (h : (↑j : ℕ) < (↑i : ℕ)),
  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)
Tactic: obtain h | h := lt_or_ge j.1 i.1