awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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
⊢ 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:
rw [Finset.sum_eq_single ⟨j.1 - i.1, i.1⟩, if_neg h.not_gt]

Premises used: Finset.sum_eq_single, LE.le.not_gt, if_neg
-- 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
h : (↑i : ℕ) ≤ (↑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)
    (if h : (↑j : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
    else if (↑j : ℕ) - (↑i : ℕ) = m then 1 else 0)

Tactic:
simp
-- 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
h : (↑i : ℕ) ≤ (↑j : ℕ)
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, ⋯⟩) else 0
            else if a = m ∧ b = (↑i : ℕ) then 1 else 0)
            0
⊢ ∀ 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:
simp only [Finset.mem_antidiagonal, ne_eq, ite_eq_right_iff, Prod.forall, Prod.mk.injEq]

Premises used: ne_eq, Finset.HasAntidiagonal.mem_antidiagonal, ite_eq_right_iff, Prod.mk.injEq, Prod.forall
-- 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
h : (↑i : ℕ) ≤ (↑j : ℕ)
a b : ℕ
inr :
  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, ⋯⟩) else 0 else if a = m ∧ b = (↑i : ℕ) then 1 else 0)
          0
⊢ 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, ⋯⟩) else 0 else if a = m ∧ b = (↑i : ℕ) then 1 else 0)
          0

Tactic:
_
-- 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
h : (↑i : ℕ) ≤ (↑j : ℕ)
a b : ℕ
h_1 : a + b = (↑j : ℕ)
inr :
  ¬(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, ⋯⟩) else 0 else if a = m ∧ b = (↑i : ℕ) then 1 else 0) 0
⊢ ¬(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, ⋯⟩) else 0 else if a = m ∧ b = (↑i : ℕ) then 1 else 0) 0

Tactic:
_
-- 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
h : (↑i : ℕ) ≤ (↑j : ℕ)
a b : ℕ
h_1 : a + b = (↑j : ℕ)
h_2 : ¬(a = (↑j : ℕ) - (↑i : ℕ) ∧ b = (↑i : ℕ))
inr :
  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, ⋯⟩) else 0 else if a = m ∧ b = (↑i : ℕ) then 1 else 0) 0
⊢ 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, ⋯⟩) else 0 else if a = m ∧ b = (↑i : ℕ) then 1 else 0) 0

Tactic:
_
-- 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
h : (↑i : ℕ) ≤ (↑j : ℕ)
a b : ℕ
h_1 : a + b = (↑j : ℕ)
h_2 : ¬(a = (↑j : ℕ) - (↑i : ℕ) ∧ b = (↑i : ℕ))
h_3 : b < k
⊢ b ≠ (↑i : ℕ)

Tactic:
lia
-- 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
h : (↑i : ℕ) ≤ (↑j : ℕ)
a b : ℕ
h_1 : a + b = (↑j : ℕ)
h_2 : ¬(a = (↑j : ℕ) - (↑i : ℕ) ∧ b = (↑i : ℕ))
h_3 : 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, ⋯⟩) else 0 else if a = m ∧ b = (↑i : ℕ) then 1 else 0) 0

Tactic:
simp [show b ≠ i by lia]
-- 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
h : (↑i : ℕ) ≤ (↑j : ℕ)
⊢ ((↑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:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
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))
⊢ m + k = n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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))
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 ⋯)))))
    (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)))
⊢ 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)))

Tactic:
subst hn
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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 ⋯))
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 ⋯))))
      (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)
⊢ 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)))

Tactic:
ext i j : 1
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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)
a :
  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)
    (-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)
⊢ 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)

Tactic:
dsimp [Polynomial.sylvester]

Premises used: Polynomial.sylvester
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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 i_1 : Fin m
⊢ Eq.{u_1 + 1} (α :=
    Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
      (Algebra.Presentation.toGenerators
        (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k ⋯))))
    (if i_1 < i then 0
    else
      if h : (↑i_1 : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑i_1 : ℕ) - (↑i : ℕ), ⋯⟩)
      else if (↑i_1 : ℕ) - (↑i : ℕ) = k then 1 else 0)
    (if i ≤ i_1 ∧ (↑i_1 : ℕ) ≤ (↑i : ℕ) + k then
      if h : (↑i_1 : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑i_1 : ℕ) - (↑i : ℕ), ⋯⟩)
      else if (↑i_1 : ℕ) - (↑i : ℕ) = k then 1 else 0
    else 0)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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 : Fin m
i_1 : Fin k
⊢ Eq.{u_1 + 1} (α :=
    Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
      (Algebra.Presentation.toGenerators
        (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k ⋯))))
    (if m + (↑i_1 : ℕ) < (↑i : ℕ) then 0
    else
      if h : m + (↑i_1 : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨m + (↑i_1 : ℕ) - (↑i : ℕ), ⋯⟩)
      else if m + (↑i_1 : ℕ) - (↑i : ℕ) = k then 1 else 0)
    (if (↑i : ℕ) ≤ m + (↑i_1 : ℕ) ∧ m + (↑i_1 : ℕ) ≤ (↑i : ℕ) + k then
      if h : m + (↑i_1 : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨m + (↑i_1 : ℕ) - (↑i : ℕ), ⋯⟩)
      else if m + (↑i_1 : ℕ) - (↑i : ℕ) = k then 1 else 0
    else 0)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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 : Fin k
i_1 : Fin m
⊢ Eq.{u_1 + 1} (α :=
    Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
      (Algebra.Presentation.toGenerators
        (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k ⋯))))
    (if (↑i_1 : ℕ) < (↑i : ℕ) then 0
    else
      if h : (↑i_1 : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨(↑i_1 : ℕ) - (↑i : ℕ), ⋯⟩)
      else if (↑i_1 : ℕ) - (↑i : ℕ) = m then 1 else 0)
    (if (↑i : ℕ) ≤ (↑i_1 : ℕ) ∧ (↑i_1 : ℕ) ≤ (↑i : ℕ) + m then
      if h : (↑i_1 : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨(↑i_1 : ℕ) - (↑i : ℕ), ⋯⟩)
      else if (↑i_1 : ℕ) - (↑i : ℕ) = m then 1 else 0
    else 0)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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 i_1 : Fin k
⊢ Eq.{u_1 + 1} (α :=
    Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
      (Algebra.Presentation.toGenerators
        (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k ⋯))))
    (if m + (↑i_1 : ℕ) < (↑i : ℕ) then 0
    else
      if h : m + (↑i_1 : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨m + (↑i_1 : ℕ) - (↑i : ℕ), ⋯⟩)
      else if m + (↑i_1 : ℕ) - (↑i : ℕ) = m then 1 else 0)
    (if (↑i : ℕ) ≤ m + (↑i_1 : ℕ) ∧ m + (↑i_1 : ℕ) ≤ (↑i : ℕ) + m then
      if h : m + (↑i_1 : ℕ) - (↑i : ℕ) < m then X (Sum.inl ⟨m + (↑i_1 : ℕ) - (↑i : ℕ), ⋯⟩)
      else if m + (↑i_1 : ℕ) - (↑i : ℕ) = m then 1 else 0
    else 0)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
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))
inr :
  Nontrivial 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))
⊢ 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

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
h : 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:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
h : 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:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim