-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
refine_1 :
  (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
              (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
            Algebra.TensorProduct.includeLeft) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
              (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
            Algebra.TensorProduct.includeRight) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).Monic
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                    (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                  Algebra.TensorProduct.includeLeft) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                    (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                  Algebra.TensorProduct.includeRight) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
        n =
      1 ∧
    ∀ i > n,
      (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                      (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                    Algebra.TensorProduct.includeLeft) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                      (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                    Algebra.TensorProduct.includeRight) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
          i =
        0
have refine_2 : (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
              (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
            Algebra.TensorProduct.includeLeft) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
              (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
            Algebra.TensorProduct.includeRight) :
        (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).natDegree =
  n
Tactic: refine (MonicDegreeEq.mk _ ?_ ?_).2