-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x y : M
rw :
  Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (k.1, x)) (X (k.2, y))))
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.1, x)) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.2, y)) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))
rw₁ :
  Eq (α := DividedPowerAlgebra R M)
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      (mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (x_1.1, x)) (X (x_1.2, y))))
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.1, x)) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.2, y)) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))
rw₂ rw₃ :
  Eq (α := DividedPowerAlgebra R M)
    (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (k.1, x)) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (k.2, y)) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.1, x)) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.2, y)) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, x + y)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
          ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.1, x)) :
            RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
          ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.2, y)) :
            RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
      DividedPowerAlgebra R M)

Tactic:
rw [mkAlgHom_rel (A := MvPolynomial (ℕ × M) R) R Rel.add, map_sum,
    Finset.sum_congr rfl (fun k _ ↦ by rw [_root_.map_mul])]

Premises used: map_sum, DividedPowerAlgebra.Rel.add, RingQuot.mkAlgHom_rel, Finset.sum_congr, rfl