K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) = Module.rank R M
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
⊢ (#ι) = Module.rank R M
haveI := nontrivial_of_invariantBasisNumber R
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) = ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) = Module.rank R M
rw [Module.rank_def]
case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) ≤ ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι

case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) ≤ (#ι)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) = ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι
apply le_antisymm
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) ≤ ?m.380781

K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ?m.380781 ≤ ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι

K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal
case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) ≤ ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι
trans
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ?m.380781 ≤ ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι

K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) ≤ ?m.380781

K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) ≤ ?m.380781

K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ?m.380781 ≤ ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι

K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal
swap
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ { s // LinearIndependent R Subtype.val }
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ?m.380781 ≤ ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι
apply le_ciSup (Cardinal.bddAbove_range.{v, v} _)
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.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ { s // LinearIndependent R Subtype.val }
exact
  ⟨Set.range v, by
    convert v.reindexRange.linearIndependent
    ext
    simp⟩
case h.e'_4
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ Subtype.val = ↑(reindexRange v)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ LinearIndependent R Subtype.val
convert v.reindexRange.linearIndependent
case h.e'_4.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.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
x✝ : { x // x ∈ range ↑v }
⊢ ↑x✝ = ↑(reindexRange v) x✝
case h.e'_4
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ Subtype.val = ↑(reindexRange v)
ext
no goals
case h.e'_4.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.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
x✝ : { x // x ∈ range ↑v }
⊢ ↑x✝ = ↑(reindexRange v) x✝
simp
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.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (#ι) ≤ (#↑↑{ val := range ↑v, property := (_ : LinearIndependent R Subtype.val) })
exact (Cardinal.mk_range_eq v v.injective).ge
case a.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.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ∀ (i : { s // LinearIndependent R Subtype.val }), (#↑↑i) ≤ (#ι)
case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ (⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι) ≤ (#ι)
apply ciSup_le'
case a.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.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
s : Set M
li : LinearIndependent R Subtype.val
⊢ (#↑↑{ val := s, property := li }) ≤ (#ι)
case a.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.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ∀ (i : { s // LinearIndependent R Subtype.val }), (#↑↑i) ≤ (#ι)
rintro ⟨s, li⟩
no goals
case a.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.378764
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type v
v : Basis ι R M
this : Nontrivial R
s : Set M
li : LinearIndependent R Subtype.val
⊢ (#↑↑{ val := s, property := li }) ≤ (#ι)
apply linearIndependent_le_basis v _ li