case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ↑f
n : ℕ
ne : n ≠ 0
w : LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤
⊢ Surjective ↑f
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ↑f
⊢ Surjective ↑f
obtain ⟨n, ne, w⟩ := exists_endomorphism_iterate_ker_sup_range_eq_top f
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ↑f
n : ℕ
ne : n ≠ 0
w : Surjective ↑(f ^ n)
⊢ Surjective ↑f
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ↑f
n : ℕ
ne : n ≠ 0
w : LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤
⊢ Surjective ↑f
rw [LinearMap.ker_eq_bot.mpr (LinearMap.iterate_injective s n), bot_sup_eq,
  LinearMap.range_eq_top] at w
no goals
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ↑f
n : ℕ
ne : n ≠ 0
w : Surjective ↑(f ^ n)
⊢ Surjective ↑f
exact LinearMap.surjective_of_iterate_surjective ne w