Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inl.left
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) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin m
⊢ (if i✝ < i then 0 else if h : ↑i✝ - ↑i < k then X (Sum.inr ⟨↑i✝ - ↑i, ⋯⟩) else if ↑i✝ - ↑i = k then 1 else 0) =
    if i ≤ i✝ ∧ ↑i✝ ≤ ↑i + k then if h : ↑i✝ - ↑i < k then X (Sum.inr ⟨↑i✝ - ↑i, h⟩) else if ↑i✝ - ↑i = k then 1 else 0
    else 0

pp: case inl.right
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) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin m
i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = k then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + k then
      if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = k then 1 else 0
    else 0

pp: case inr.left
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) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin k
i✝ : Fin m
⊢ (if ↑i✝ < ↑i then 0 else if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, ⋯⟩) else if ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ ↑i✝ ∧ ↑i✝ ≤ ↑i + m then
      if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, h⟩) else if ↑i✝ - ↑i = m then 1 else 0
    else 0

pp: case inr.right
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) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + m then
      if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = m then 1 else 0
    else 0

Tactic:
<;>

Goal state after:
case inl.left
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) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin m
⊢ (if i✝ < i then 0 else if h : ↑i✝ - ↑i < k then X (Sum.inr ⟨↑i✝ - ↑i, ⋯⟩) else if ↑i✝ - ↑i = k then 1 else 0) =
    if i ≤ i✝ ∧ ↑i✝ ≤ ↑i + k then if h : ↑i✝ - ↑i < k then X (Sum.inr ⟨↑i✝ - ↑i, h⟩) else if ↑i✝ - ↑i = k then 1 else 0
    else 0

case inl.right
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) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin m
i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = k then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + k then
      if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = k then 1 else 0
    else 0

case inr.left
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) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin k
i✝ : Fin m
⊢ (if ↑i✝ < ↑i then 0 else if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, ⋯⟩) else if ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ ↑i✝ ∧ ↑i✝ ≤ ↑i + m then
      if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, h⟩) else if ↑i✝ - ↑i = m then 1 else 0
    else 0

case inr.right
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) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + m then
      if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = m then 1 else 0
    else 0