-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_subsingleton [Subsingleton R] : Module.rank R M = 1

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
⊢ Module.rank R M = 1

Tactic:
rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]

Result:
case h₁
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ 1

case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
⊢ ∀ w < 1, ∃ i, w < #↑↑i

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this : Subsingleton M
⊢ Module.rank R M = 1

Tactic:
have : Nonempty { s : Set M // LinearIndepOn R id s} := ⟨⟨∅, linearIndepOn_empty _ _⟩⟩

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
⊢ Module.rank R M = 1

Proof state:
case h₁
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ 1

Tactic:
rintro ⟨s, hs⟩

Result:
case h₁.mk
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
s : Set M
hs : LinearIndepOn R id s
⊢ #↑↑⟨s, hs⟩ ≤ 1

Proof state:
case h₁.mk
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
s : Set M
hs : LinearIndepOn R id s
⊢ (↑⟨s, hs⟩).Subsingleton

Tactic:
apply subsingleton_of_subsingleton

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ Module.rank R M = 1

Tactic:
haveI := Module.subsingleton R M

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this : Subsingleton M
⊢ Module.rank R M = 1

Proof state:
case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
⊢ ∀ w < 1, ∃ i, w < #↑↑i

Tactic:
intro w hw

Result:
case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
w : Cardinal.{v}
hw : w < 1
⊢ ∃ i, w < #↑↑i

Proof state:
case h₁.mk
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
s : Set M
hs : LinearIndepOn R id s
⊢ #↑↑⟨s, hs⟩ ≤ 1

Tactic:
rw [Cardinal.mk_le_one_iff_set_subsingleton]

Result:
case h₁.mk
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
s : Set M
hs : LinearIndepOn R id s
⊢ (↑⟨s, hs⟩).Subsingleton

Proof state:
case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
this✝ : Subsingleton M
this : Nonempty { s // LinearIndepOn R id s }
w : Cardinal.{v}
hw : w < 1
⊢ ∃ i, w < #↑↑i

Tactic:
exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩

Result:
no goals