R : Type u_2
M : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n => LinearMap.range (r ^ n • LinearMap.id)) m
y : M
hy : r ^ m • y = x
⊢ r ^ n • r ^ (m - n) • y = x
R : Type u_2
M : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n => LinearMap.range (r ^ n • LinearMap.id)) m
y : M
hy : ↑(r ^ m • LinearMap.id) y = x
⊢ ↑(r ^ n • LinearMap.id) (r ^ (m - n) • y) = x
dsimp at hy⊢
no goals
R : Type u_2
M : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
x✝ : x ∈ (fun n => LinearMap.range (r ^ n • LinearMap.id)) m
y : M
hy : r ^ m • y = x
⊢ r ^ n • r ^ (m - n) • y = x
rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]