-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mem_ideal_smul_span_iff_exists_sum {ι : Type*} (f : ι → M) (x : M) :
    x ∈ I • span R (Set.range f) ↔
      ∃ (a : ι →₀ R) (_ : ∀ i, a i ∈ I), (a.sum fun i c => c • f i) = x

Proof state:
case mp.refine_1.intro.intro.intro.intro.intro.refine_1
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
⊢ (Finsupp.single i y) j ∈ I

Tactic:
letI := Classical.decEq ι

Result:
case mp.refine_1.intro.intro.intro.intro.intro.refine_1
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
⊢ (Finsupp.single i y) j ∈ I

Proof state:
case neg
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : ¬i = j
⊢ 0 ∈ I

Tactic:
exact I.zero_mem

Result:
no goals

Proof state:
case mp
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x

Tactic:
refine fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)

Result:
case mp.refine_1
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ x ∈ ⋃ a ∈ I, ⋃ b ∈ Set.range f, {a • b}, ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x

case mp.refine_2
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = 0

case mp.refine_3
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x y : M),
    x ∈ span R (⋃ a ∈ I, ⋃ b ∈ Set.range f, {a • b}) →
      y ∈ span R (⋃ a ∈ I, ⋃ b ∈ Set.range f, {a • b}) →
        (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x) →
          (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = y) →
            ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x + y

case mp.refine_4
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (a : R),
    ∀ x ∈ span R (⋃ a ∈ I, ⋃ b ∈ Set.range f, {a • b}),
      (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x) →
        ∃ a_2, ∃ (_ : ∀ (i : ι), a_2 i ∈ I), (a_2.sum fun i c => c • f i) = a • x

Proof state:
case mp.refine_3
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (x y : M),
    x ∈ span R (⋃ a ∈ I, ⋃ b ∈ Set.range f, {a • b}) →
      y ∈ span R (⋃ a ∈ I, ⋃ b ∈ Set.range f, {a • b}) →
        (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x) →
          (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = y) →
            ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x + y

Tactic:
rintro x y - - ⟨ax, hax, rfl⟩ ⟨ay, hay, rfl⟩

Result:
case mp.refine_3.intro.intro.intro.intro
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = (ax.sum fun i c => c • f i) + ay.sum fun i c => c • f i

Proof state:
case mpr.intro.intro
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i c => c • f i) ∈ I • span R (Set.range f)

Tactic:
exact Submodule.sum_mem _ fun c _ => smul_mem_smul (ha c) <| subset_span <| Set.mem_range_self _

Result:
no goals

Proof state:
case mp.refine_1.intro.intro.intro.intro.intro.refine_2
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i : ι
⊢ (fun i y => y • f i) i 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case mp
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x

case mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x) → x ∈ I • span R (Set.range f)

Tactic:
swap

Result:
case mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x) → x ∈ I • span R (Set.range f)

case mp
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x

Tactic:
constructor

Result:
case mp
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x

case mpr
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x) → x ∈ I • span R (Set.range f)

Proof state:
case mp.refine_1.intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i : ι
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = y • f i

Tactic:
refine ⟨Finsupp.single i y, fun j => ?_, ?_⟩

Result:
case mp.refine_1.intro.intro.intro.intro.intro.refine_1
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i j : ι
⊢ (Finsupp.single i y) j ∈ I

case mp.refine_1.intro.intro.intro.intro.intro.refine_2
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ I
i : ι
⊢ ((Finsupp.single i y).sum fun i c => c • f i) = y • f i