K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.44308
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'
p : Submodule R M
h :
  lift (Module.rank R { x // x ∈ LinearMap.range (LinearMap.comp f (Submodule.subtype p)) }) ≤
    lift (Module.rank R { x // x ∈ p })
⊢ lift (Module.rank R { x // x ∈ Submodule.map f p }) ≤ lift (Module.rank R { x // x ∈ p })
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.44308
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'
p : Submodule R M
⊢ lift (Module.rank R { x // x ∈ Submodule.map f p }) ≤ lift (Module.rank R { x // x ∈ p })
have h := lift_rank_range_le (f.comp (Submodule.subtype p))
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.44308
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'
p : Submodule R M
h :
  lift (Module.rank R { x // x ∈ LinearMap.range (LinearMap.comp f (Submodule.subtype p)) }) ≤
    lift (Module.rank R { x // x ∈ p })
⊢ lift (Module.rank R { x // x ∈ Submodule.map f p }) ≤ lift (Module.rank R { x // x ∈ p })
rwa [LinearMap.range_comp, range_subtype] at h