Theorem: linearIndependent_subsingleton_index (Matroid/ForMathlib/LinearAlgebra/LinearIndependent.lean)

State before:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic:
obtain (he | he) := isEmpty_or_nonempty ι
State after:
case inl
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : IsEmpty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

case inr
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

State before:
case inr
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic:
obtain ⟨_⟩ := (unique_iff_subsingleton_and_nonempty (α := ι)).2 ⟨by assumption, he⟩
State after:
case inr.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

State before:
case inr.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic:
rw [linearIndependent_unique_iff]
State after:
case inr.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ f default ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

State before:
case inr.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ f default ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
Tactic:
exact ⟨fun h i ↦ by rwa [Unique.eq_default i], fun h ↦ h _⟩
State after:
no goals

State before:
case inl
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : IsEmpty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic:
simp [linearIndependent_empty_type]
State after:
no goals

State before:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ Subsingleton ι
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
h : f default ≠ 0
i : ι
⊢ f i ≠ 0
Tactic:
rwa [Unique.eq_default i]
State after:
no goals