Theorem: DividedPowerAlgebra.lift'_imp (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 q : MvPolynomial (ℕ × M) R
h : Rel R M p q
⊢ (eval₂AlgHom R f) p = (eval₂AlgHom R f) q
Tactic:
cases' h with a r n a m n a n a b <;> 
  simp only [eval₂AlgHom_X', map_one, map_zero, map_smul, AlgHom.map_mul, map_nsmul, AlgHom.map_sum]
State after:
no goals