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.1132953
inst✝¹⁰ : Ring K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V'
inst✝⁴ : Module K V'
inst✝³ : AddCommGroup V''
inst✝² : Module K V''
inst✝¹ : AddCommGroup V'₁
inst✝ : Module K V'₁
g : V →ₗ[K] V'
f : V' →ₗ[K] V'₁
⊢ rank (comp f g) ≤ rank g
simpa only [Cardinal.lift_id] using lift_rank_comp_le_right g f