-- Mathlib/Algebra/Module/SpanRank.lean
@[simp]
lemma spanRank_eq_zero_iff_eq_bot {I : Submodule R M} : I.spanRank = 0 ↔ I = ⊥

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
h : I.spanRank = 0
⊢ I.spanRank ≤ 0

Tactic:
rw [h]

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
⊢ I.spanRank = 0 ↔ I = ⊥

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
⊢ I.spanRank = 0 → I = ⊥

case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
⊢ I = ⊥ → I.spanRank = 0

Proof state:
case mp.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
h : I.spanRank = 0
s : Set M
hs₁ : #↑s ≤ 0
hs₂ : span R s = I
⊢ I = ⊥

Tactic:
simp only [nonpos_iff_eq_zero, mk_eq_zero_iff, Set.isEmpty_coe_sort] at hs₁

Result:
case mp.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
h : I.spanRank = 0
s : Set M
hs₂ : span R s = I
hs₁ : s = ∅
⊢ I = ⊥

Proof state:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊥.spanRank = 0

Tactic:
rw [spanRank]

Result:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⨅ s, #↑↑s = 0

Proof state:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
h : I.spanRank = 0
⊢ I = ⊥

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ :=
  (FG.spanRank_le_iff_exists_span_set_card_le I (a := 0)).mp (by rw [h])

Result:
case mp.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
h : I.spanRank = 0
s : Set M
hs₁ : #↑s ≤ 0
hs₂ : span R s = I
⊢ I = ⊥

Proof state:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
⊢ I = ⊥ → I.spanRank = 0

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊥.spanRank = 0

Proof state:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
⊢ I.spanRank = 0 → I = ⊥

Tactic:
intro h

Result:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
h : I.spanRank = 0
⊢ I = ⊥

Proof state:
case mp.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
h : I.spanRank = 0
s : Set M
hs₂ : span R s = I
hs₁ : s = ∅
⊢ I = ⊥

Tactic:
simp_all

Result:
no goals

Proof state:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⨅ s, #↑↑s = 0

Tactic:
exact Cardinal.iInf_eq_zero_iff.mpr (Or.inr ⟨⟨∅, by simp⟩, by simp⟩)

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R ∅ = ⊥

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ #↑↑⟨∅, ⋯⟩ = 0

Tactic:
simp

Result:
no goals