-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem iSupIndep.subtype_ne_bot_le_rank [Nontrivial R]
    {V : ι → Submodule R M} (hV : iSupIndep V) :
    Cardinal.lift.{v} #{ i : ι // V i ≠ ⊥ } ≤ Cardinal.lift.{w} (Module.rank R M)

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
v : I → M
hvV : ∀ (i : I), v i ∈ V ↑i
hv : ∀ (i : I), v i ≠ 0
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Tactic:
have : LinearIndependent R v := (hV.comp Subtype.coe_injective).linearIndependent _ hvV hv

Result:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
v : I → M
hvV : ∀ (i : I), v i ∈ V ↑i
hv : ∀ (i : I), v i ≠ 0
this : LinearIndependent R v
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
⊢ lift.{v, w} #{ i // V i ≠ ⊥ } ≤ lift.{w, v} (Module.rank R M)

Tactic:
set I := { i : ι // V i ≠ ⊥ }

Result:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ ∃ v ∈ V ↑i, v ≠ 0

Tactic:
rw [← Submodule.ne_bot_iff]

Result:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ V ↑i ≠ ⊥

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Tactic:
have hI : ∀ i : I, ∃ v ∈ V i, v ≠ (0 : M) := by
  intro i
  rw [← Submodule.ne_bot_iff]
  exact i.prop

Result:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
hI : ∀ (i : I), ∃ v ∈ V ↑i, v ≠ 0
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
⊢ ∀ (i : I), ∃ v ∈ V ↑i, v ≠ 0

Tactic:
intro i

Result:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ ∃ v ∈ V ↑i, v ≠ 0

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
v : I → M
hvV : ∀ (i : I), v i ∈ V ↑i
hv : ∀ (i : I), v i ≠ 0
this : LinearIndependent R v
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Tactic:
exact this.cardinal_lift_le_rank

Result:
no goals

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
hI : ∀ (i : I), ∃ v ∈ V ↑i, v ≠ 0
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Tactic:
choose v hvV hv using hI

Result:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
v : I → M
hvV : ∀ (i : I), v i ∈ V ↑i
hv : ∀ (i : I), v i ≠ 0
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ V ↑i ≠ ⊥

Tactic:
exact i.prop

Result:
no goals