-- Mathlib/LinearAlgebra/Dimension/Finite.lean
/-- See `rank_zero_iff` for a stronger version with `NoZeroSMulDivisor R M`. -/
lemma rank_eq_zero_iff :
    Module.rank R M = 0 ↔ ∀ x : M, ∃ a : R, a ≠ 0 ∧ a • x = 0

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : ↑s
a : R
ha : a ≠ 0
ha' : a • ↑i = 0
⊢ (Finsupp.linearCombination R fun x => id ↑x) (Finsupp.single i a) = 0

Tactic:
simpa

Result:
no goals

Proof state:
case mp.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
⊢ 1 ≤ Module.rank R M

Tactic:
have : LinearIndependent R (fun _ : Unit ↦ x) :=
  linearIndependent_iff.mpr (fun l hl ↦ Finsupp.unique_ext <| not_not.mp fun H ↦
    hx _ H ((Finsupp.linearCombination_unique _ _ _).symm.trans hl))

Result:
case mp.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
this : LinearIndependent R fun x_1 => x
⊢ 1 ≤ Module.rank R M

Proof state:
case mp
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ Module.rank R M = 0 → ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

Tactic:
contrapose!

Result:
case mp
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ (∃ x, ∀ (a : R), a ≠ 0 → a • x ≠ 0) → Module.rank R M ≠ 0

Proof state:
case mp.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
⊢ Module.rank R M ≠ 0

Tactic:
rw [← Cardinal.one_le_iff_ne_zero]

Result:
case mp.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
⊢ 1 ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Module.rank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

Tactic:
nontriviality R

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ Module.rank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

Proof state:
case mpr.h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ ¬Nonempty ↑↑⟨s, hs⟩

Tactic:
rintro ⟨i : s⟩

Result:
case mpr.h.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : ↑s
⊢ False

Proof state:
case mpr.h.intro.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : ↑s
a : R
ha : a ≠ 0
ha' : a • ↑i = 0
⊢ a = 0

Tactic:
simpa using DFunLike.congr_fun (linearIndependent_iff.mp hs (Finsupp.single i a) (by simpa)) i

Result:
no goals

Proof state:
case mpr
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0) → Module.rank R M = 0

Tactic:
intro h

Result:
case mpr
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ Module.rank R M = 0

Proof state:
case mpr
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ ⨆ ι, #↑↑ι ≤ 0

Tactic:
apply ciSup_le'

Result:
case mpr.h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ 0

Proof state:
case mp
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ (∃ x, ∀ (a : R), a ≠ 0 → a • x ≠ 0) → Module.rank R M ≠ 0

Tactic:
rintro ⟨x, hx⟩

Result:
case mp.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
⊢ Module.rank R M ≠ 0

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ Module.rank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

Tactic:
constructor

Result:
case mp
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ Module.rank R M = 0 → ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

case mpr
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0) → Module.rank R M = 0

Proof state:
case mpr.h.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : ↑s
⊢ False

Tactic:
obtain ⟨a, ha, ha'⟩ := h i

Result:
case mpr.h.intro.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : ↑s
a : R
ha : a ≠ 0
ha' : a • ↑i = 0
⊢ False

Proof state:
case mpr.h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ #↑↑⟨s, hs⟩ ≤ 0

Tactic:
rw [nonpos_iff_eq_zero, Cardinal.mk_eq_zero_iff, ← not_nonempty_iff]

Result:
case mpr.h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ ¬Nonempty ↑↑⟨s, hs⟩

Proof state:
case mpr.h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ 0

Tactic:
intro ⟨s, hs⟩

Result:
case mpr.h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ #↑↑⟨s, hs⟩ ≤ 0

Proof state:
case mp.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
this : LinearIndependent R fun x_1 => x
⊢ 1 ≤ Module.rank R M

Tactic:
simpa using this.cardinal_lift_le_rank

Result:
no goals

Proof state:
case mpr.h.intro.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : ↑s
a : R
ha : a ≠ 0
ha' : a • ↑i = 0
⊢ False

Tactic:
apply ha

Result:
case mpr.h.intro.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : ↑s
a : R
ha : a ≠ 0
ha' : a • ↑i = 0
⊢ a = 0

Proof state:
case mpr
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ Module.rank R M = 0

Tactic:
rw [← le_zero_iff, Module.rank_def]

Result:
case mpr
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ ⨆ ι, #↑↑ι ≤ 0