-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem Basis.le_span {J : Set M} (v : Basis ι R M) (hJ : span R J = ⊤) : #(range v) ≤ #J

Proof state:
case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S' j
IJ : #↑J < #↑(range ⇑v)
⊢ #↑(⋃ j, S' j) < #↑(range ⇑v)

Tactic:
refine lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
  (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_

Result:
case inr.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S' j
IJ : #↑J < #↑(range ⇑v)
⊢ ∀ (i : ↑J), #↑(S' i) ≤ (fun x => ℵ₀) i

case inr.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S' j
IJ : #↑J < #↑(range ⇑v)
⊢ (sum fun x => ℵ₀) < #↑(range ⇑v)

Proof state:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S' j

Tactic:
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⟩

Result:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S j))
⊢ b ∈ ⋃ j, S' j

Proof state:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]

Result:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift.{v, w} #ι ≤ lift.{w, v} ↑(Fintype.card ↑J)

Proof state:
case inr.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S' j
IJ : #↑J < #↑(range ⇑v)
⊢ (sum fun x => ℵ₀) < #↑(range ⇑v)

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
cases fintypeOrInfinite J

Result:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ #↑(range ⇑v) ≤ #↑J

case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
⊢ #↑(range ⇑v) ≤ #↑J

Proof state:
case intro.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S j
hb : v i ∈ range ⇑v
j : ↑J
hj : i ∈ S j
⊢ v i ∈ ⋃ j, S' j

Tactic:
exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩

Result:
no goals

Proof state:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S j
hb : v i ∈ range ⇑v
⊢ v i ∈ ⋃ j, S' j

Tactic:
rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩

Result:
case intro.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S j
hb : v i ∈ range ⇑v
j : ↑J
hj : i ∈ S j
⊢ v i ∈ ⋃ j, S' j

Proof state:
case inr.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S' j
IJ : #↑J < #↑(range ⇑v)
⊢ ∀ (i : ↑J), #↑(S' i) ≤ (fun x => ℵ₀) i

Tactic:
exact fun j => (Cardinal.lt_aleph0_of_finite _).le

Result:
no goals

Proof state:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift.{v, w} #ι ≤ lift.{w, v} ↑(Fintype.card ↑J)

Tactic:
convert Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)

Result:
case h.e'_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift.{w, v} ↑(Fintype.card ↑J) = lift.{v, w} ↑(Fintype.card ↑J)

Proof state:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S j))
⊢ b ∈ ⋃ j, S' j

Tactic:
rw [hJ] at this

Result:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
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, S j))
⊢ b ∈ ⋃ j, S' j