-- 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)
x : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
a :
  ∀ (p q : 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))))
        (HSub.hSub (β := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) p
          ((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)
                  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))))
          (HSub.hSub (β := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) q
            ((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)
                    q)) :
              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))))
          (HSub.hSub (β := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (p + q)
            ((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)
                    (p + q))) :
              MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
a₁ :
  ∀ (p : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (i : Fin m ⊕ Fin k),
    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)) p
          ((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)
                  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))))
        (HSub.hSub (β := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (p * X i)
          ((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)
                  (p * X i))) :
            MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
a₂ :
  ∀ (x : 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))))
      (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 :
          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))) :
          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))))
    (HSub.hSub (β := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) x
      ((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)
              x)) :
        MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))

Tactic:
induction x using MvPolynomial.induction_on with
    | add p q _ _ => simp only [map_add, add_sub_add_comm]; exact add_mem ‹_› ‹_›
    | mul_X p i _ => simp only [map_mul, H, map_X, ← sub_mul]; exact Ideal.mul_mem_right _ _ ‹_›
    | C x =>
    induction x using MvPolynomial.induction_on with
    | C a => simp [f]
    | add p q _ _ => simp only [map_add, add_sub_add_comm]; exact add_mem ‹_› ‹_›
    | mul_X p i IH =>
      simp only [map_mul]
      exact Ideal.mul_sub_mul_mem _ IH (Ideal.subset_span ⟨i, by simp [f]⟩)

Premises used: map_add, MvPolynomial.induction_on, sub_mul, map_mul, Ideal.mul_mem_right, AddMemClass.add_mem, add_sub_add_comm, MvPolynomial.C, MvPolynomial.map_X