Theorem: DividedPowerAlgebra.lift'AlgHom_apply (unused_files/Init_copy.lean)

State before:
R : Type u_3
M : Type u_1
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ range (n + 1), f (x, u) * f (n - x, v)
p : MvPolynomial (ℕ × M) R
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (mk p) = (aeval f) p
Tactic:
rw [mk, lift', RingQuot.liftAlgHom_mkAlgHom_apply, coe_eval₂AlgHom]
State after:
R : Type u_3
M : Type u_1
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ range (n + 1), f (x, u) * f (n - x, v)
p : MvPolynomial (ℕ × M) R
⊢ (sorryAx (DividedPowerAlgebra R M →ₐ[R] A) true)
      ((sorryAx (MvPolynomial (ℕ × M) R →ₐ[R] DividedPowerAlgebra R M) true) p) =
    (aeval f) p