case intro
R : Type u_2
M : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.range (r ^ n • LinearMap.id) = LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ Nat.succ n • y = r ^ n • 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
x : M
⊢ ∃ n y, r ^ Nat.succ n • y = r ^ n • x
obtain ⟨n, hn⟩ := IsArtinian.range_smul_pow_stabilizes M r
case intro
R : Type u_2
M : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn :
  ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ LinearMap.range (r ^ n • LinearMap.id) ↔ x ∈ LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ Nat.succ n • y = r ^ n • x
case intro
R : Type u_2
M : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.range (r ^ n • LinearMap.id) = LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ Nat.succ n • y = r ^ n • x
simp_rw [SetLike.ext_iff] at hn
no goals
case intro
R : Type u_2
M : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn :
  ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ LinearMap.range (r ^ n • LinearMap.id) ↔ x ∈ LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ Nat.succ n • y = r ^ n • x
exact ⟨n, by simpa using hn n.succ n.le_succ (r ^ n • x)⟩
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
x : M
n : ℕ
hn :
  ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ LinearMap.range (r ^ n • LinearMap.id) ↔ x ∈ LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ y, r ^ Nat.succ n • y = r ^ n • x
simpa using hn n.succ n.le_succ (r ^ n • x)