awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ Eq.{max (u_1 + 1) 1} (α :=
    Ideal
      (Algebra.Generators.Ring (R := MvPolynomial (Fin n) R) (S := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (ι := Fin m ⊕ Fin k)
        { val := Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x,
          σ' := fun (f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) ↦
            (map C : (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
              ((tensorEquivSum R (Fin m) (Fin k) R :
                  (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
                f),
          aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }))
    (Ideal.span
      (Set.range fun (i : Fin n) ↦
        HSub.hSub (α := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (β :=
          MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
          ((C : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (X i) :
            MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
          ((map C : (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) 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 i))) :
            MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))))
    (Algebra.Generators.ker
      { val := Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x,
        σ' := fun (f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) ↦
          (map C : (a : MvPolynomial (Fin m ⊕ Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
            ((tensorEquivSum R (Fin m) (Fin k) R :
                (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
              f),
        aeval_val_σ' := ⋯, algebraMap_eq := ⋯ })

Tactic:
exact (ker_eval₂Hom_universalFactorizationMap R n m k hn).symm

Premises used: MvPolynomial.ker_eval₂Hom_universalFactorizationMap, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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)
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)
⊢ 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)

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

Premises used: MvPolynomial.X, Sum.inr, Finset.HasAntidiagonal.antidiagonal
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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)
    (∑ 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:
simp [universalFactorizationMap, mapEquivMonic, Polynomial.coeff_mul, coeff_freeMonic,
      apply_dite, apply_ite, ← Algebra.TensorProduct.one_def,
      Pi.single_apply, Fin.ext_iff, ← ite_and]

Premises used: apply_dite, Fin.ext_iff, Pi.single_apply, apply_ite, Polynomial.coeff_mul, MvPolynomial.universalFactorizationMap, MvPolynomial.mapEquivMonic, ite_and, Algebra.TensorProduct.one_def, Polynomial.coeff_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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)
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)
⊢ 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

Premises used: Fin.val, lt_or_ge
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
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
⊢ 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:
rw [Finset.sum_eq_zero, if_pos h]

Premises used: Finset.sum_eq_zero, if_pos
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
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, ⋯⟩) else 0
        else if b = k ∧ a < m ∧ a = (↑i : ℕ) then 1 else 0)
        0
⊢ ∀ 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:
simp only [Finset.mem_antidiagonal, Prod.forall]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Prod.forall
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
a b : ℕ
hab : a + b = (↑j : ℕ)
⊢ a ≠ (↑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 m
j : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
a b : ℕ
hab : 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, ⋯⟩) else 0
    else if b = k ∧ a < m ∧ a = (↑i : ℕ) then 1 else 0)
    0

Tactic:
simp [show a ≠ 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 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
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
⊢ 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:
rw [Finset.sum_eq_single ⟨i.1, j.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 m
j : Fin n
h : (↑i : ℕ) ≤ (↑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)
    (if h : (↑j : ℕ) - (↑i : ℕ) < k then X (Sum.inr ⟨(↑j : ℕ) - (↑i : ℕ), h⟩)
    else if (↑j : ℕ) - (↑i : ℕ) = k 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 m
j : Fin n
h : (↑i : ℕ) ≤ (↑j : ℕ)
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, ⋯⟩) else 0
          else if b = k ∧ a < m ∧ a = (↑i : ℕ) then 1 else 0)
          0
⊢ ∀ 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:
simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]

Premises used: ne_eq, Finset.HasAntidiagonal.mem_antidiagonal, Prod.mk.injEq, Prod.forall, not_and
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h_1 : (↑i : ℕ) ≤ (↑j : ℕ)
a b : ℕ
e : a + b = (↑j : ℕ)
h : a = (↑i : ℕ) → ¬b = (↑j : ℕ) - (↑i : ℕ)
⊢ a ≠ (↑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 m
j : Fin n
h_1 : (↑i : ℕ) ≤ (↑j : ℕ)
a b : ℕ
e : a + b = (↑j : ℕ)
h : 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, ⋯⟩) else 0
    else if b = k ∧ a < m ∧ a = (↑i : ℕ) then 1 else 0)
    0

Tactic:
simp [show a ≠ 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 m
j : Fin n
h : (↑i : ℕ) ≤ (↑j : ℕ)
⊢ ((↑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:
simp [h]
-- 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₁ :
  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:
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

Premises used: MvPolynomial.X, Sum.inl, Finset.HasAntidiagonal.antidiagonal
-- 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
⊢ 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:
simp [universalFactorizationMap, mapEquivMonic, Polynomial.coeff_mul, coeff_freeMonic,
      apply_dite, apply_ite, ← Algebra.TensorProduct.one_def,
      Pi.single_apply, Fin.ext_iff, ← ite_and]

Premises used: apply_dite, Fin.ext_iff, Pi.single_apply, apply_ite, Polynomial.coeff_mul, MvPolynomial.universalFactorizationMap, MvPolynomial.mapEquivMonic, ite_and, Algebra.TensorProduct.one_def, Polynomial.coeff_freeMonic
-- 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
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)
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)
⊢ 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

Premises used: Fin.val, lt_or_ge
-- 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 : (↑j : ℕ) < (↑i : ℕ)
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
⊢ 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_zero, if_pos h]

Premises used: Finset.sum_eq_zero, if_pos
-- 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 : (↑j : ℕ) < (↑i : ℕ)
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
⊢ ∀ 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:
simp only [Finset.mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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 : (↑j : ℕ) < (↑i : ℕ)
⊢ ∀ (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:
lia