no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.83941
R : Type u
inst✝⁶ : Ring R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type v'
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
M₁ : Type v
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
f : M →ₗ[R] M'
h : Surjective ↑f
⊢ Module.rank R { x // x ∈ LinearMap.range f } = Module.rank R M'
rw [LinearMap.range_eq_top.2 h, rank_top]