Theorem: DividedPowerAlgebra.augIdeal_isAugmentationIdeal' (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
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (Ideal.Quotient.mk (augIdeal R M)) ((algebraMap_comp_kerLiftAlg R M) r) = r
Tactic:
dsimp only [algebraMap_comp_kerLiftAlg]
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (Ideal.Quotient.mk (augIdeal R M))
      (((algebraMap R (DividedPowerAlgebra R M)).comp (kerLiftAlg_algebraMapInv R M).toRingHom) r) =
    r

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (Ideal.Quotient.mk (augIdeal R M))
      (((algebraMap R (DividedPowerAlgebra R M)).comp (kerLiftAlg_algebraMapInv R M).toRingHom) r) =
    r
Tactic:
rw [RingHom.coe_comp, Function.comp_apply, Ideal.Quotient.mk_algebraMap]
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (algebraMap R (DividedPowerAlgebra R M ⧸ augIdeal R M)) ((kerLiftAlg_algebraMapInv R M).toRingHom r) = r

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (algebraMap R (DividedPowerAlgebra R M ⧸ augIdeal R M)) ((kerLiftAlg_algebraMapInv R M).toRingHom r) = r
Tactic:
apply kerLiftAlg_rightInverse
State after:
no goals