Theorem: Submodule.mem_span_set_iff_exists_sum (DividedPowers/ForMathlib/RingTheory/SubmoduleMem.lean)

State before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R s ↔ ∃ a, (a.sum fun i c => c • ↑i) = x
Tactic:
conv_lhs => rw [← Set.image_id s]
State after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R (id '' s) ↔ ∃ a, (a.sum fun i c => c • ↑i) = x

State before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R (id '' s) ↔ ∃ a, (a.sum fun i c => c • ↑i) = x
Tactic:
rw [← top_smul (span R (id '' s)), mem_ideal_smul_span_iff_exists_sum']
State after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • id ↑i) = x) ↔ ∃ a, (a.sum fun i c => c • ↑i) = x

State before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • id ↑i) = x) ↔ ∃ a, (a.sum fun i c => c • ↑i) = x
Tactic:
exact exists_congr fun a => ⟨fun ⟨_, h⟩ => h, fun h => ⟨fun i => mem_top, h⟩⟩
State after:
no goals