-- Mathlib/LinearAlgebra/Span/Defs.lean
lemma span_range_update_add_smul (hij : i ≠ j) (v : ι → M) (r : R) :
    span R (Set.range (Function.update v j (v j + r • v i))) = span R (Set.range v)

Proof state:
case refine_1.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ update v j (v j + r • v i) k ∈ span R (range v)

Tactic:
exact subset_span ⟨k, (update_of_ne hjk.symm ..).symm⟩

Result:
no goals

Proof state:
case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ update v j (v j + r • v i) j ∈ span R (range v)

Tactic:
rw [update_self]

Result:
case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i ∈ span R (range v)

Proof state:
case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i ∈ span R (range v)

Tactic:
exact add_mem (subset_span ⟨j, rfl⟩) <| smul_mem _ _ <| subset_span ⟨i, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ span R (range (update v j (v j + r • v i))) = span R (range v)

Tactic:
refine le_antisymm ?_ ?_ <;> simp only [span_le, Set.range_subset_iff, SetLike.mem_coe] <;>
  intro k <;> obtain rfl | hjk := eq_or_ne j k

Result:
case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ update v j (v j + r • v i) j ∈ span R (range v)

case refine_1.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ update v j (v j + r • v i) k ∈ span R (range v)

case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j ∈ span R (range (update v j (v j + r • v i)))

case refine_2.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ v k ∈ span R (range (update v j (v j + r • v i)))

Proof state:
case refine_2.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ v k ∈ span R (range (update v j (v j + r • v i)))

Tactic:
exact subset_span ⟨k, update_of_ne hjk.symm ..⟩

Result:
no goals

Proof state:
case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j ∈ span R (range (update v j (v j + r • v i)))

Tactic:
nth_rw 2 [← add_sub_cancel_right (v j) (r • v i)]

Result:
case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i - r • v i ∈ span R (range (update v j (v j + r • v i)))

Proof state:
case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i - r • v i ∈ span R (range (update v j (v j + r • v i)))

Tactic:
exact sub_mem (subset_span ⟨j, update_self ..⟩)
  (smul_mem _ _ (subset_span ⟨i, update_of_ne hij ..⟩))

Result:
no goals