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

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ (⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) ((algebraMapInv R M) ↑x) = x
Tactic:
ext
State after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑((⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) ((algebraMapInv R M) ↑x)) = ↑x

State before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑((⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) ((algebraMapInv R M) ↑x)) = ↑x
Tactic:
simp only [proj', proj, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply]
State after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑(((DirectSum.decompose (grade R M)) ((algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x))) 0) = ↑x

State before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑(((DirectSum.decompose (grade R M)) ((algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x))) 0) = ↑x
Tactic:
conv_rhs => rw [← DirectSum.decompose_of_mem_same _ x.2]
State after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑(((DirectSum.decompose (grade R M)) ((algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x))) 0) =
    ↑(((DirectSum.decompose (grade R M)) ↑x) 0)

State before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑(((DirectSum.decompose (grade R M)) ((algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x))) 0) =
    ↑(((DirectSum.decompose (grade R M)) ↑x) 0)
Tactic:
simp only [algebraMap_right_inv_of_degree_zero R M x, decompose_coe, of_eq_same]
State after:
no goals