K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.12896
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₁
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) ≤ ↑n
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.12896
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₁
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
⊢ Module.rank R M ≤ ↑n
rw [Module.rank_def]
case h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.12896
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₁
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
⊢ ∀ (i : { s // LinearIndependent R Subtype.val }), (#↑↑i) ≤ ↑n
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.12896
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₁
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) ≤ ↑n
apply ciSup_le'
case h.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.12896
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₁
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ (#↑↑{ val := s, property := li }) ≤ ↑n
case h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.12896
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₁
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
⊢ ∀ (i : { s // LinearIndependent R Subtype.val }), (#↑↑i) ≤ ↑n
rintro ⟨s, li⟩
no goals
case h.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.12896
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₁
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ (#↑↑{ val := s, property := li }) ≤ ↑n
exact linearIndependent_bounded_of_finset_linearIndependent_bounded H _ li