-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem Basis.mem_span_iff_repr_mem (m : M) :
    m ∈ span R (Set.range b) ↔ ∀ i, b.repr m i ∈ Set.range (algebraMap R S)

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ ((b.repr m).sum fun i a => a • b i) ∈ span R (range ⇑b)

Tactic:
refine sum_mem fun i _ => ?_

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
⊢ (fun i a => a • b i) i ((b.repr m) i) ∈ span R (range ⇑b)

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ m ∈ span R (range ⇑b)

Tactic:
rw [← b.linearCombination_repr m, Finsupp.linearCombination_apply S _]

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ ((b.repr m).sum fun i a => a • b i) ∈ span R (range ⇑b)

Proof state:
case intro
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ w✝ • b i ∈ span R (range ⇑b)

Tactic:
exact smul_mem _ _ (subset_span (Set.mem_range_self i))

Result:
no goals

Proof state:
case intro
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ (fun i a => a • b i) i ((b.repr m) i) ∈ span R (range ⇑b)

Tactic:
simp_rw [← h, algebraMap_smul]

Result:
case intro
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ w✝ • b i ∈ span R (range ⇑b)

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
⊢ (fun i a => a • b i) i ((b.repr m) i) ∈ span R (range ⇑b)

Tactic:
obtain ⟨_, h⟩ := h i

Result:
case intro
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ (fun i a => a • b i) i ((b.repr m) i) ∈ span R (range ⇑b)

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
⊢ m ∈ span R (range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)

Tactic:
refine
  ⟨fun hm i => ⟨(b.restrictScalars R).repr ⟨m, hm⟩ i, b.restrictScalars_repr_apply R ⟨m, hm⟩ i⟩,
    fun h => ?_⟩

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ m ∈ span R (range ⇑b)