R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : CompleteLattice.Independent 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
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : CompleteLattice.Independent fun i => Submodule.span R {v i}
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
⊢ LinearIndependent R v
refine' linearIndependent_iff_not_smul_mem_span.mpr fun i r hi => _
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : CompleteLattice.Independent 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
replace hv := CompleteLattice.independent_def.mp hv i
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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
simp only [iSup_subtype', ← Submodule.span_range_eq_iSup, disjoint_iff] at hv
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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
have : r • v i ∈ ⊥ := by
  rw [← hv, Submodule.mem_inf]
  refine' ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, _⟩
  convert hi
  ext
  simp
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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)
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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
rw [← Submodule.mem_bot R, ← h_ne_zero i]
no goals
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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)
simpa using this
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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)
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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 ∈ ⊥
rw [← hv, Submodule.mem_inf]
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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)
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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)
refine' ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, _⟩
case h.e'_5.h.e'_6
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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})
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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)
convert hi
case h.e'_5.h.e'_6.h
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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})
case h.e'_5.h.e'_6
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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})
ext
no goals
case h.e'_5.h.e'_6.h
R✝ : Type ?u.12249
M✝ : Type ?u.12252
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
ι : Type u_1
R : Type u_2
M : Type u_3
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})
simp