Theorem: DividedPowerAlgebra.roby_theorem_2 (DividedPowers/DPAlgebra/Dpow.lean)

State before:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ (dividedPowers' R M).isDPMorphism hI ↑(lift hI φ hφ)
Tactic:
apply cond_D_uniqueness
State after:
case hh
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ ∀ (n : ℕ) (x : M), (dividedPowers' R M).dpow n ((ι R M) x) = dp R n x

State before:
case hh
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ ∀ (n : ℕ) (x : M), (dividedPowers' R M).dpow n ((ι R M) x) = dp R n x
Tactic:
intro m n
State after:
case hh
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
m : ℕ
n : M
⊢ (dividedPowers' R M).dpow m ((ι R M) n) = dp R m n

State before:
case hh
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
m : ℕ
n : M
⊢ (dividedPowers' R M).dpow m ((ι R M) n) = dp R m n
Tactic:
rw [dpow_ι]
State after:
no goals