Theorem: Submodule.mem_span_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
ι : Type u_3
f : ι → M
x : M
⊢ x ∈ span R (Set.range f) ↔ ∃ a, (a.sum fun i c => c • f i) = x
Tactic:
rw [← top_smul (span R (Set.range f)), 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
ι : Type u_3
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ ⊤), (a.sum fun i c => c • f i) = x) ↔ ∃ a, (a.sum fun i c => c • f i) = x

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