Theorem: DividedPowerAlgebra.lift'AlgHom_apply_dp (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)
n : ℕ
m : M
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (dp R n m) = f (n, m)
Tactic:
rw [dp_def, ← mk, lift'AlgHom_apply f hf_zero hf_smul hf_mul hf_add, aeval_X]
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)
n : ℕ
m : M
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) ((mkAlgHom R (Rel R M)) (X (n, m))) = f (n, m)