-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem LinearIndependent.iSupIndep_span_singleton (hv : LinearIndependent R v) :
    iSupIndep fun i => R ∙ v i

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
m : M
hm : m ∈ span R {v i} ⊓ ⨆ j, ⨆ (_ : j ≠ i), span R {v j}
⊢ m ∈ ⊥

Tactic:
simp only [mem_inf, mem_span_singleton, iSup_subtype'] at hm

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
m : M
hm : (∃ a, a • v i = m) ∧ m ∈ ⨆ x, span R {v ↑x}
⊢ m ∈ ⊥

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
m : M
hm : (∃ a, a • v i = m) ∧ m ∈ span R (range fun x => v ↑x)
⊢ m ∈ ⊥

Tactic:
obtain ⟨⟨r, rfl⟩, hm⟩ := hm

Result:
case intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
⊢ r • v i ∈ ⊥

Proof state:
case intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
⊢ r • v i ∈ ⊥

Tactic:
suffices r = 0 by simp [this]

Result:
case intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
⊢ r = 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
⊢ Disjoint (span R {v i}) (⨆ j, ⨆ (_ : j ≠ i), span R {v j})

Tactic:
rw [disjoint_iff_inf_le]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
⊢ span R {v i} ⊓ ⨆ j, ⨆ (_ : j ≠ i), span R {v j} ≤ ⊥

Proof state:
case intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
⊢ r = 0

Tactic:
apply hv.not_smul_mem_span i

Result:
case intro.intro.ha
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
⊢ r • v i ∈ span R (v '' (univ \ {i}))

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
this : r = 0
⊢ r • v i ∈ ⊥

Tactic:
simp [this]

Result:
no goals

Proof state:
case h.e'_4.h.e'_6.h
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
x✝ : M
⊢ x✝ ∈ v '' (univ \ {i}) ↔ x✝ ∈ range fun x => v ↑x

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
m : M
hm : (∃ a, a • v i = m) ∧ m ∈ ⨆ x, span R {v ↑x}
⊢ m ∈ ⊥

Tactic:
rw [← span_range_eq_iSup] at hm

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
m : M
hm : (∃ a, a • v i = m) ∧ m ∈ span R (range fun x => v ↑x)
⊢ m ∈ ⊥

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
⊢ iSupIndep fun i => span R {v i}

Tactic:
refine iSupIndep_def.mp fun i => ?_

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
⊢ Disjoint (span R {v i}) (⨆ j, ⨆ (_ : j ≠ i), span R {v j})

Proof state:
case h.e'_4.h.e'_6
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
⊢ v '' (univ \ {i}) = range fun x => v ↑x

Tactic:
ext

Result:
case h.e'_4.h.e'_6.h
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
x✝ : M
⊢ x✝ ∈ v '' (univ \ {i}) ↔ x✝ ∈ range fun x => v ↑x

Proof state:
case intro.intro.ha
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
⊢ r • v i ∈ span R (v '' (univ \ {i}))

Tactic:
convert hm

Result:
case h.e'_4.h.e'_6
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
r : R
hm : r • v i ∈ span R (range fun x => v ↑x)
⊢ v '' (univ \ {i}) = range fun x => v ↑x

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
⊢ span R {v i} ⊓ ⨆ j, ⨆ (_ : j ≠ i), span R {v j} ≤ ⊥

Tactic:
intro m hm

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
m : M
hm : m ∈ span R {v i} ⊓ ⨆ j, ⨆ (_ : j ≠ i), span R {v j}
⊢ m ∈ ⊥