-- 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 : ι
this : DecidableEq ι := Classical.decEq ι
⊢ (Finsupp.single i y) j ∈ I

Tactic:
rw [Finsupp.single_apply]

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 ι
⊢ (if i = j then y else 0) ∈ I

Proof state:
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

Tactic:
exact ⟨0, fun _ => I.zero_mem, Finsupp.sum_zero_index⟩

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 : ι
⊢ ((Finsupp.single i y).sum fun i c => c • f i) = y • f i

Tactic:
refine @Finsupp.sum_single_index ι R M _ _ i _ (fun i y => y • f i) ?_

Result:
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

Proof state:
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

Tactic:
simp only [Set.mem_iUnion, Set.mem_range, Set.mem_singleton_iff]

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 : M),
    (∃ i, ∃ (_ : i ∈ I), ∃ i_1, ∃ (_ : ∃ y, f y = i_1), x = i • i_1) →
      ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x

Proof state:
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 : M),
    (∃ i, ∃ (_ : i ∈ I), ∃ i_1, ∃ (_ : ∃ y, f y = i_1), x = i • i_1) →
      ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x

Tactic:
rintro x ⟨y, hy, x, ⟨i, rfl⟩, rfl⟩

Result:
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

Proof state:
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:
rintro ⟨a, ha, rfl⟩

Result:
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)

Proof state:
case mp.refine_4.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)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∃ a_1, ∃ (_ : ∀ (i : ι), a_1 i ∈ I), (a_1.sum fun i c => c • f i) = c • a.sum fun i c => c • f i

Tactic:
refine ⟨c • a, fun i => I.mul_mem_left c (ha i), ?_⟩

Result:
case mp.refine_4.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)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ((c • a).sum fun i c => c • f i) = c • a.sum fun i c => c • f i

Proof state:
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

Tactic:
refine ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩ <;>
  intros <;> simp only [zero_smul, add_smul]

Result:
no goals

Proof state:
case mp.refine_4.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)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ((c • a).sum fun i c => c • f i) = c • a.sum fun i c => c • f i

Tactic:
rw [Finsupp.sum_smul_index, Finsupp.smul_sum] <;> intros <;> simp only [zero_smul, mul_smul]

Result:
no goals

Proof state:
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

Tactic:
rintro c x - ⟨a, ha, rfl⟩

Result:
case mp.refine_4.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)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∃ a_1, ∃ (_ : ∀ (i : ι), a_1 i ∈ I), (a_1.sum fun i c => c • f i) = c • a.sum fun i c => c • f i

Proof state:
case pos
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
⊢ y ∈ I

Tactic:
assumption

Result:
no goals

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 : ι
this : DecidableEq ι := Classical.decEq ι
⊢ (if i = j then y else 0) ∈ I

Tactic:
split_ifs

Result:
case pos
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
⊢ y ∈ I

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