-- Mathlib/Algebra/Module/Torsion.lean
theorem iSupIndep.linearIndependent' {ι R M : Type*} {v : ι → M} [Ring R]
    [AddCommGroup M] [Module R M] (hv : iSupIndep fun i => R ∙ v i)
    (h_ne_zero : ∀ i, Ideal.torsionOf R M (v i) = ⊥) : LinearIndependent R v

Proof state:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Disjoint (Submodule.span R {v i}) (⨆ j, ⨆ (_ : j ≠ i), Submodule.span R {v j})
⊢ r = 0

Tactic:
simp only [iSup_subtype', ← Submodule.span_range_eq_iSup (ι := Subtype _), disjoint_iff] at hv

Result:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r = 0

Proof state:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r = 0

Tactic:
have : r • v i ∈ (⊥ : Submodule R M) := by
  rw [← hv, Submodule.mem_inf]
  refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩
  convert hi
  ext
  simp

Result:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r = 0

Proof state:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r • v i ∈ Submodule.span R (Set.range fun i_1 => v ↑i_1)

Tactic:
convert hi

Result:
case h.e'_4.h.e'_6
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ (Set.range fun i_1 => v ↑i_1) = v '' (Set.univ \ {i})

Proof state:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r • v i ∈ ⊥

Tactic:
rw [← hv, Submodule.mem_inf]

Result:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r • v i ∈ Submodule.span R {v i} ∧ r • v i ∈ Submodule.span R (Set.range fun i_1 => v ↑i_1)

Proof state:
case h.e'_4.h.e'_6
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ (Set.range fun i_1 => v ↑i_1) = v '' (Set.univ \ {i})

Tactic:
ext

Result:
case h.e'_4.h.e'_6.h
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
x✝ : M
⊢ (x✝ ∈ Set.range fun i_1 => v ↑i_1) ↔ x✝ ∈ v '' (Set.univ \ {i})

Proof state:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : iSupIndep fun i => Submodule.span R {v i}
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
⊢ LinearIndependent R v

Tactic:
refine linearIndependent_iff_not_smul_mem_span.mpr fun i r hi => ?_

Result:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : iSupIndep fun i => Submodule.span R {v i}
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
⊢ r = 0

Proof state:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : iSupIndep fun i => Submodule.span R {v i}
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
⊢ r = 0

Tactic:
replace hv := iSupIndep_def.mp hv i

Result:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Disjoint (Submodule.span R {v i}) (⨆ j, ⨆ (_ : j ≠ i), Submodule.span R {v j})
⊢ r = 0

Proof state:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r = 0

Tactic:
rw [← Submodule.mem_bot R, ← h_ne_zero i]

Result:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r ∈ torsionOf R M (v i)

Proof state:
case h.e'_4.h.e'_6.h
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
x✝ : M
⊢ (x✝ ∈ Set.range fun i_1 => v ↑i_1) ↔ x✝ ∈ v '' (Set.univ \ {i})

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
this : r • v i ∈ ⊥
⊢ r ∈ torsionOf R M (v i)

Tactic:
simpa using this

Result:
no goals

Proof state:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r • v i ∈ Submodule.span R {v i} ∧ r • v i ∈ Submodule.span R (Set.range fun i_1 => v ↑i_1)

Tactic:
refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩

Result:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥
⊢ r • v i ∈ Submodule.span R (Set.range fun i_1 => v ↑i_1)