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 k
j : Fin n
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)
⊢ 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 inr : ∀ (h : (↑i : ℕ) ≤ (↑j : ℕ)),
  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
-- 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
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)
have inl : ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (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)
    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 k
j : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
⊢ ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
      (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)
      0
have inl : ∀ (x : ℕ × ℕ),
  x.1 + x.2 = (↑j : ℕ) →
    Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
      (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)
      0
Tactic: simp only [Finset.mem_antidiagonal]
-- 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
h : (↑i : ℕ) ≤ (↑j : ℕ)
⊢ 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 inr : Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
  (if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 < k then
    if h : ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1 < m then
      if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 = (↑i : ℕ) then X (Sum.inl ⟨((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1, h⟩) else 0
    else if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1 = m ∧ ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 = (↑i : ℕ) then 1 else 0
  else 0)
  (if h : (↑j : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
  else if (↑j : ℕ) - (↑i : ℕ) = m then 1 else 0)
Tactic: rw [Finset.sum_eq_single ⟨j.1 - i.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 k
j : Fin n
h : (↑i : ℕ) ≤ (↑j : ℕ)
inr :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 < k then
      if h : ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1 < m then
        if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 = (↑i : ℕ) then X (Sum.inl ⟨((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1, h⟩) else 0
      else if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1 = m ∧ ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 = (↑i : ℕ) then 1 else 0
    else 0)
    (if h : (↑j : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
    else if (↑j : ℕ) - (↑i : ℕ) = m then 1 else 0)
⊢ 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 inr₁ : ∀ b ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
  b ≠ ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)) →
    Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
      (if b.2 < k then
        if h : b.1 < m then if b.2 = (↑i : ℕ) then X (Sum.inl ⟨b.1, h⟩) else 0
        else if b.1 = m ∧ b.2 = (↑i : ℕ) then 1 else 0
      else 0)
      0
Tactic: rw [Finset.sum_eq_single ⟨j.1 - i.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 k
j : Fin n
h : (↑i : ℕ) ≤ (↑j : ℕ)
inr :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 < k then
      if h : ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1 < m then
        if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 = (↑i : ℕ) then X (Sum.inl ⟨((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1, h⟩) else 0
      else if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1 = m ∧ ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 = (↑i : ℕ) then 1 else 0
    else 0)
    (if h : (↑j : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
    else if (↑j : ℕ) - (↑i : ℕ) = m then 1 else 0)
inr₁ :
  ∀ b ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
    b ≠ ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)) →
      Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
        (if b.2 < k then
          if h : b.1 < m then if b.2 = (↑i : ℕ) then X (Sum.inl ⟨b.1, h⟩) else 0
          else if b.1 = m ∧ b.2 = (↑i : ℕ) then 1 else 0
        else 0)
        0
⊢ 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 inr₂ : ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ) →
  Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
    (if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 < k then
      if h : ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1 < m then
        if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 = (↑i : ℕ) then X (Sum.inl ⟨((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1, h⟩) else 0
      else if ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).1 = m ∧ ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)).2 = (↑i : ℕ) then 1 else 0
    else 0)
    0
Tactic: rw [Finset.sum_eq_single ⟨j.1 - i.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 k
j : Fin n
h : (↑i : ℕ) ≤ (↑j : ℕ)
⊢ ∀ b ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (↑j : ℕ),
    b ≠ ((↑j : ℕ) - (↑i : ℕ), (↑i : ℕ)) →
      Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
        (if b.2 < k then
          if h : b.1 < m then if b.2 = (↑i : ℕ) then X (Sum.inl ⟨b.1, h⟩) else 0
          else if b.1 = m ∧ b.2 = (↑i : ℕ) then 1 else 0
        else 0)
        0
have inr : ∀ (a b : ℕ),
  a + b = (↑j : ℕ) →
    ¬(a = (↑j : ℕ) - (↑i : ℕ) ∧ b = (↑i : ℕ)) →
      b < k →
        Eq.{u_1 + 1} (α := MvPolynomial (Fin m ⊕ Fin k) R)
          (if h : a < m then if b = (↑i : ℕ) then X (Sum.inl ⟨a, sorry⟩) else 0 else if a = m ∧ b = (↑i : ℕ) then 1 else 0)
          0
Tactic: simp only [Finset.mem_antidiagonal, ne_eq, ite_eq_right_iff, Prod.forall, Prod.mk.injEq]
-- 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: 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]
-- 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: 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]
-- 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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
⊢ Eq (α :=
    Matrix (Fin n) (Fin n)
      (Algebra.Generators.Ring (R := MvPolynomial (Fin n) R)
        (Algebra.Presentation.toGenerators
          (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R n m k hn)))))
    (Algebra.PreSubmersivePresentation.jacobiMatrix (universalFactorizationMapPresentation R n m k hn))
    (-Matrix.transpose
        ((Matrix.reindex (finCongr ⋯) (finCongr ⋯) :
            (a : Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))) →
              Matrix (Fin n) (Fin n) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
          (sylvester
            (Polynomial.map (R := MvPolynomial (Fin m) R)
              (AlgHom.toRingHom (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inl)))
              (freeMonic R m))
            (Polynomial.map (R := MvPolynomial (Fin k) R)
              (AlgHom.toRingHom (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inr)))
              (freeMonic R k))
            m k)))
have subst : Eq (α :=
  Matrix (Fin (m + k)) (Fin (m + k))
    (Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
      (Algebra.Presentation.toGenerators
        (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k sorry)))))
  (Algebra.PreSubmersivePresentation.jacobiMatrix (universalFactorizationMapPresentation R (m + k) m k sorry))
  (-Matrix.transpose
      ((Matrix.reindex (finCongr sorry) (finCongr sorry) :
          (a : Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))) →
            Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R)))
        (sylvester
          (Polynomial.map (R := MvPolynomial (Fin m) R)
            (AlgHom.toRingHom
              (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inl)))
            (freeMonic R m))
          (Polynomial.map (R := MvPolynomial (Fin k) R)
            (AlgHom.toRingHom
              (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inr)))
            (freeMonic R k))
          m k)))
Tactic: subst hn
Cleared hypotheses: n, hn, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
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) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R (m + k) m k ⋯))
⊢ Eq (α :=
    Matrix (Fin (m + k)) (Fin (m + k))
      (Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
        (Algebra.Presentation.toGenerators
          (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k ⋯)))))
    (Algebra.PreSubmersivePresentation.jacobiMatrix (universalFactorizationMapPresentation R (m + k) m k ⋯))
    (-Matrix.transpose
        ((Matrix.reindex (finCongr ⋯) (finCongr ⋯) :
            (a : Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))) →
              Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R)))
          (sylvester
            (Polynomial.map (R := MvPolynomial (Fin m) R)
              (AlgHom.toRingHom
                (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inl)))
              (freeMonic R m))
            (Polynomial.map (R := MvPolynomial (Fin k) R)
              (AlgHom.toRingHom
                (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inr)))
              (freeMonic R k))
            m k)))
have a : ∀ (i j : Fin (m + k)),
  Eq (α :=
    Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
      (Algebra.Presentation.toGenerators
        (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k sorry))))
    (Algebra.PreSubmersivePresentation.jacobiMatrix (universalFactorizationMapPresentation R (m + k) m k sorry) i j)
    ((-Matrix.transpose
          ((Matrix.reindex (finCongr sorry) (finCongr sorry) :
              (a : Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))) →
                Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R)))
            (sylvester
              (Polynomial.map (R := MvPolynomial (Fin m) R)
                (AlgHom.toRingHom
                  (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inl)))
                (freeMonic R m))
              (Polynomial.map (R := MvPolynomial (Fin k) R)
                (AlgHom.toRingHom
                  (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inr)))
                (freeMonic R k))
              m k)))
      i j)
Tactic: ext i j : 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
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) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R (m + k) m k ⋯))
i j : Fin (m + k)
⊢ Eq (α :=
    Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
      (Algebra.Presentation.toGenerators
        (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k ⋯))))
    (Algebra.PreSubmersivePresentation.jacobiMatrix (universalFactorizationMapPresentation R (m + k) m k ⋯) i j)
    ((-Matrix.transpose
          ((Matrix.reindex (finCongr ⋯) (finCongr ⋯) :
              (a : Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))) →
                Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R)))
            (sylvester
              (Polynomial.map (R := MvPolynomial (Fin m) R)
                (AlgHom.toRingHom
                  (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inl)))
                (freeMonic R m))
              (Polynomial.map (R := MvPolynomial (Fin k) R)
                (AlgHom.toRingHom
                  (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inr)))
                (freeMonic R k))
              m k)))
      i j)
have a : Eq (α :=
  Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
    (Algebra.Presentation.toGenerators
      (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k sorry))))
  (Algebra.PreSubmersivePresentation.jacobiMatrix (universalFactorizationMapPresentation R (m + k) m k sorry) i j)
  (-Fin.addCases (motive := fun (x : Fin (m + k)) ↦ MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
      (fun (j₁ : Fin m) ↦
        if (↑j : ℕ) ∈ Set.Icc (↑j₁ : ℕ) ((↑j₁ : ℕ) + k) then
          Polynomial.coeff
            (Polynomial.map
              (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inr)) :
                MvPolynomial (Fin k) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
              (freeMonic R k))
            ((↑j : ℕ) - (↑j₁ : ℕ))
        else 0)
      (fun (j₁ : Fin k) ↦
        if (↑j : ℕ) ∈ Set.Icc (↑j₁ : ℕ) ((↑j₁ : ℕ) + m) then
          Polynomial.coeff
            (Polynomial.map
              (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inl)) :
                MvPolynomial (Fin m) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
              (freeMonic R m))
            ((↑j : ℕ) - (↑j₁ : ℕ))
        else 0)
      i)
Tactic: dsimp [Polynomial.sylvester]
-- 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
⊢ Algebra.PreSubmersivePresentation.jacobian (universalFactorizationMapPresentation R n m k hn) =
    HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n *
      resultant (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
        (Polynomial.map (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (freeMonic R k))
have inl : Subsingleton R →
  Algebra.PreSubmersivePresentation.jacobian (universalFactorizationMapPresentation R n m k hn) =
    HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n *
      resultant (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
        (Polynomial.map (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (freeMonic R k))
Tactic: cases subsingleton_or_nontrivial R