case intro.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.566078
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
s b : Set V
hb : b ⊆ s
hsab : span K b = span K s
hlib : LinearIndependent K Subtype.val
⊢ Module.rank K { x // x ∈ span K s } ≤ (#↑s)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.566078
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
s : Set V
⊢ Module.rank K { x // x ∈ span K s } ≤ (#↑s)
obtain ⟨b, hb, hsab, hlib⟩ := exists_linearIndependent K s
case h.e'_3
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.566078
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
s b : Set V
hb : b ⊆ s
hsab : span K b = span K s
hlib : LinearIndependent K Subtype.val
⊢ Module.rank K { x // x ∈ span K s } = (#↑b)
case intro.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.566078
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
s b : Set V
hb : b ⊆ s
hsab : span K b = span K s
hlib : LinearIndependent K Subtype.val
⊢ Module.rank K { x // x ∈ span K s } ≤ (#↑s)
convert Cardinal.mk_le_mk_of_subset hb
no goals
case h.e'_3
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.566078
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
s b : Set V
hb : b ⊆ s
hsab : span K b = span K s
hlib : LinearIndependent K Subtype.val
⊢ Module.rank K { x // x ∈ span K s } = (#↑b)
rw [← hsab, rank_span_set hlib]