Theorem: DividedPowerAlgebra.toTrivSqZeroExt_apply_dp_of_two_le (DividedPowers/DPAlgebra/Graded/GradeOne.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
n : ℕ
m : M
hn : 2 ≤ n
⊢ (toTrivSqZeroExt R M) (dp R n m) = 0
Tactic:
rw [toTrivSqZeroExt, liftAlgHom_apply_dp, DividedPowers.OfSquareZero.dpow_of_two_le]
State after:
case hn
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
n : ℕ
m : M
hn : 2 ≤ n
⊢ 2 ≤ n

State before:
case hn
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
n : ℕ
m : M
hn : 2 ≤ n
⊢ 2 ≤ n
Tactic:
exact hn
State after:
no goals