K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
⊢ (#↑(range ↑v)) ≤ (#↑J)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
⊢ (#↑(range ↑v)) ≤ (#↑J)
haveI := nontrivial_of_invariantBasisNumber R
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ (#↑(range ↑v)) ≤ (#↑J)

case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
⊢ (#↑(range ↑v)) ≤ (#↑J)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
⊢ (#↑(range ↑v)) ≤ (#↑J)
cases fintypeOrInfinite J
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift (#ι) ≤ lift ↑(Fintype.card ↑J)
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ (#↑(range ↑v)) ≤ (#↑J)
rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]
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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift ↑(Fintype.card ↑J) = lift ↑(Fintype.card ↑J)
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift (#ι) ≤ lift ↑(Fintype.card ↑J)
convert Cardinal.lift_le.{w, v}.2 (basis_le_span' v hJ)
no goals
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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift ↑(Fintype.card ↑J) = lift ↑(Fintype.card ↑J)
simp
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
⊢ (#↑(range ↑v)) ≤ (#↑J)
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
⊢ (#↑(range ↑v)) ≤ (#↑J)
let S : J → Set ι := fun j => ↑(v.repr j).support
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
⊢ (#↑(range ↑v)) ≤ (#↑J)
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
⊢ (#↑(range ↑v)) ≤ (#↑J)
let S' : J → Set M := fun j => v '' S j
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
IJ : (#↑J) < (#↑(range ↑v))
⊢ False
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
⊢ (#↑(range ↑v)) ≤ (#↑J)
refine' le_of_not_lt fun IJ => _
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
IJ : (#↑J) < (#↑(range ↑v))
⊢ (#↑(⋃ (j : ↑J), S' j)) < (#↑(range ↑v))
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
IJ : (#↑J) < (#↑(range ↑v))
⊢ False
suffices (#⋃ j, S' j) < (#range v) by exact not_le_of_lt this ⟨Set.embeddingOfSubset _ _ hs⟩
case inr.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
IJ : (#↑J) < (#↑(range ↑v))
⊢ ∀ (i : ↑J), (#↑(S' i)) ≤ (fun x => ℵ₀) i

case inr.refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
IJ : (#↑J) < (#↑(range ↑v))
⊢ (sum fun x => ℵ₀) < (#↑(range ↑v))
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
IJ : (#↑J) < (#↑(range ↑v))
⊢ (#↑(⋃ (j : ↑J), S' j)) < (#↑(range ↑v))
refine' lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
  (Cardinal.sum_le_sum _ (fun _ => ℵ₀) _)) _
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
⊢ b ∈ ⋃ (j : ↑J), S' j
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
⊢ range ↑v ⊆ ⋃ (j : ↑J), S' j
intro b hb
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
⊢ b ∈ ⋃ (j : ↑J), S' j
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
⊢ b ∈ ⋃ (j : ↑J), S' j
rcases mem_range.1 hb with ⟨i, hi⟩
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
this : span R J ≤ comap (↑v.repr) (Finsupp.supported R R (⋃ (j : ↑J), S j))
⊢ b ∈ ⋃ (j : ↑J), S' j
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
⊢ b ∈ ⋃ (j : ↑J), S' j
have : span R J ≤ comap v.repr.toLinearMap (Finsupp.supported R R (⋃ j, S j)) :=
  span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
this : ⊤ ≤ comap (↑v.repr) (Finsupp.supported R R (⋃ (j : ↑J), S j))
⊢ b ∈ ⋃ (j : ↑J), S' j
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
this : span R J ≤ comap (↑v.repr) (Finsupp.supported R R (⋃ (j : ↑J), S j))
⊢ b ∈ ⋃ (j : ↑J), S' j
rw [hJ] at this
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
this : ↑v.repr (↑v i) ∈ Finsupp.supported R R (⋃ (j : ↑J), S j)
⊢ b ∈ ⋃ (j : ↑J), S' j
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
this : ⊤ ≤ comap (↑v.repr) (Finsupp.supported R R (⋃ (j : ↑J), S j))
⊢ b ∈ ⋃ (j : ↑J), S' j
replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
this : ↑{i} ⊆ ⋃ (j : ↑J), S j
⊢ b ∈ ⋃ (j : ↑J), S' j
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
this : ↑v.repr (↑v i) ∈ Finsupp.supported R R (⋃ (j : ↑J), S j)
⊢ b ∈ ⋃ (j : ↑J), S' j
rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single_ne_zero _ one_ne_zero] at this
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
i : ι
this : ↑{i} ⊆ ⋃ (j : ↑J), S j
hb : ↑v i ∈ range ↑v
⊢ ↑v i ∈ ⋃ (j : ↑J), S' j
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
b : M
hb : b ∈ range ↑v
i : ι
hi : ↑v i = b
this : ↑{i} ⊆ ⋃ (j : ↑J), S j
⊢ b ∈ ⋃ (j : ↑J), S' j
subst b
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
i : ι
this : ↑{i} ⊆ ⋃ (j : ↑J), S j
hb : ↑v i ∈ range ↑v
j : ↑J
hj : i ∈ S j
⊢ ↑v i ∈ ⋃ (j : ↑J), S' j
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
i : ι
this : ↑{i} ⊆ ⋃ (j : ↑J), S j
hb : ↑v i ∈ range ↑v
⊢ ↑v i ∈ ⋃ (j : ↑J), S' j
rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
no goals
case 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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
i : ι
this : ↑{i} ⊆ ⋃ (j : ↑J), S j
hb : ↑v i ∈ range ↑v
j : ↑J
hj : i ∈ S j
⊢ ↑v i ∈ ⋃ (j : ↑J), S' j
exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩
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.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
IJ : (#↑J) < (#↑(range ↑v))
this : (#↑(⋃ (j : ↑J), S' j)) < (#↑(range ↑v))
⊢ False
exact not_le_of_lt this ⟨Set.embeddingOfSubset _ _ hs⟩
no goals
case inr.refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
IJ : (#↑J) < (#↑(range ↑v))
⊢ ∀ (i : ↑J), (#↑(S' i)) ≤ (fun x => ℵ₀) i
exact fun j => (Cardinal.lt_aleph0_of_finite _).le
no goals
case inr.refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.310827
R : Type u
inst✝³ : Ring R
inst✝² : RankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(↑v.repr ↑j).support
S' : ↑J → Set M := fun j => ↑v '' S j
hs : range ↑v ⊆ ⋃ (j : ↑J), S' j
IJ : (#↑J) < (#↑(range ↑v))
⊢ (sum fun x => ℵ₀) < (#↑(range ↑v))
simpa