Theorem: DividedPowerAlgebra.proj'_zero_comp_algebraMap (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ ↑((⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) x) = (algebraMap R (DividedPowerAlgebra R M)) x
Tactic:
simp only [proj', proj, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
  Algebra.algebraMap_eq_smul_one, decompose_smul, decompose_one]
State after:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ ↑((x • 1) 0) = x • 1

State before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ ↑((x • 1) 0) = x • 1
Tactic:
rfl
State after:
no goals