Theorem: DividedPowerAlgebra.lift_ι_apply (DividedPowers/DPAlgebra/Graded/Basic.lean)

State before:
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
x : M
⊢ (lift hI φ hφ) ((ι R M) x) = φ x
Tactic:
conv_rhs => rw [← ι_comp_lift R hI hφ]
State after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
x : M
⊢ (lift hI φ hφ) ((ι R M) x) = ((lift hI φ hφ).toLinearMap ∘ₗ ι R M) x

State before:
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
x : M
⊢ (lift hI φ hφ) ((ι R M) x) = ((lift hI φ hφ).toLinearMap ∘ₗ ι R M) x
Tactic:
rfl
State after:
no goals