-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom
    (↑(universalFactorizationMap R n m k hn) :
      MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)
H :
  ∀ (i : Fin m ⊕ Fin k),
    Eq (α := 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)
          ((f :
              (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X i)) :
        MvPolynomial (Fin m ⊕ Fin k) R)
      (X i : MvPolynomial (Fin m ⊕ Fin k) R)
p : MvPolynomial (Fin n) R
i : Fin n
IH :
  Membership.mem (γ := Ideal (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
    (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))))
    (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)) p :
        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)
            ((f :
                (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                  MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              ((C : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) p))) :
        MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
⊢ Membership.mem (γ := Ideal (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
    (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))))
    (HMul.hMul (α := 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)) p :
          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)) -
      HMul.hMul (α := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (β :=
        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)
              ((f :
                  (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                    MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                ((C : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) p))) :
          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)
              ((f :
                  (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                    MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) 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)))

Tactic:
exact Ideal.mul_sub_mul_mem _ IH (Ideal.subset_span ⟨i, by simp [f]⟩)

Premises used: Ideal.subset_span, Exists.intro, Ideal.mul_sub_mul_mem