-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial.{v, u} (↥s) D
ha :
  Ne (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    (0 : MvPolynomial σ D)
w : Multiset (MvPolynomial.{v, u} (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial.{v, u} (↥s) D)ˣ
hw : w.prod * (↑u : MvPolynomial (↥s) D) = a'
rw :
  HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
        MvPolynomial σ D)
      ((↑((Units.map
                  (↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
                    MvPolynomial (↥s) D →* MvPolynomial σ D) :
                (a : (MvPolynomial (↥s) D)ˣ) → (MvPolynomial σ D)ˣ)
              u) :
          MvPolynomial σ D) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
rw₁ :
  HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
        MvPolynomial σ D)
      (((↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
              MvPolynomial (↥s) D →* MvPolynomial σ D) :
            (a : MvPolynomial (↥s) D) → MvPolynomial σ D)
          (↑u : MvPolynomial (↥s) D) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
rw₂ :
  HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
        MvPolynomial σ D)
      (((↑(↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) : MvPolynomial (↥s) D →+* MvPolynomial σ D) :
              MvPolynomial (↥s) D →* MvPolynomial σ D) :
            (a : MvPolynomial (↥s) D) → MvPolynomial σ D)
          (↑u : MvPolynomial (↥s) D) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
rw₃ :
  HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
        MvPolynomial σ D)
      (((↑(↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) : MvPolynomial (↥s) D →+* MvPolynomial σ D) :
              MvPolynomial (↥s) D →* MvPolynomial σ D) :
            (a : MvPolynomial (↥s) D) → MvPolynomial σ D)
          (↑u : MvPolynomial (↥s) D) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
rw₄ :
  HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
        MvPolynomial σ D)
      (((↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) : MvPolynomial (↥s) D →* MvPolynomial σ D) :
            (a : MvPolynomial (↥s) D) → MvPolynomial σ D)
          (↑u : MvPolynomial (↥s) D) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
rw₅ :
  HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
        MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D)
          (↑u : MvPolynomial (↥s) D) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
rw₆ :
  Eq (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D)
        (w.prod * (↑u : MvPolynomial (↥s) D)) :
      MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
rw₇ rw₈ :
  Eq (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
⊢ HMul.hMul (α := MvPolynomial σ D)
      (Multiset.prod
        (Multiset.map
          (⇑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w))
      (↑((Units.map
                (↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
                  MvPolynomial (↥s) D →* MvPolynomial σ D) :
              (a : (MvPolynomial (↥s) D)ˣ) → (MvPolynomial σ D)ˣ)
            u) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'

Tactic:
rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
        AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]

Premises used: Units.coe_map, RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe, map_mul, AlgHom.toRingHom_eq_coe, Multiset.prod_hom, AlgHom.toRingHom_toMonoidHom