Theorem: DividedPowerAlgebra.dp_add (DividedPowers/DPAlgebra/Init.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ dp R n (x + y) = ∑ k ∈ antidiagonal n, dp R k.1 x * dp R k.2 y
Tactic:
simp only [dp_def]
State after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (X (n, x + y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (X (n, x + y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Tactic:
rw [mkAlgHom_rel (A := MvPolynomial (ℕ × M) R) R Rel.add]
State after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (∑ k ∈ antidiagonal n, X (k.1, x) * X (k.2, y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (∑ k ∈ antidiagonal n, X (k.1, x) * X (k.2, y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Tactic:
rw [AlgHom.map_sum]
State after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x) * X (x_1.2, y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x) * X (x_1.2, y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Tactic:
apply Finset.sum_congr rfl
State after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ∀ x_1 ∈ antidiagonal n,
    (mkAlgHom R (Rel R M)) (X (x_1.1, x) * X (x_1.2, y)) =
      (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ∀ x_1 ∈ antidiagonal n,
    (mkAlgHom R (Rel R M)) (X (x_1.1, x) * X (x_1.2, y)) =
      (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Tactic:
intro k _
State after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
k : ℕ × ℕ
a✝ : k ∈ antidiagonal n
⊢ (mkAlgHom R (Rel R M)) (X (k.1, x) * X (k.2, y)) =
    (mkAlgHom R (Rel R M)) (X (k.1, x)) * (mkAlgHom R (Rel R M)) (X (k.2, y))

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
k : ℕ × ℕ
a✝ : k ∈ antidiagonal n
⊢ (mkAlgHom R (Rel R M)) (X (k.1, x) * X (k.2, y)) =
    (mkAlgHom R (Rel R M)) (X (k.1, x)) * (mkAlgHom R (Rel R M)) (X (k.2, y))
Tactic:
rw [AlgHom.map_mul]
State after:
no goals