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
s : Set ι
f : ι → M
x : M
⊢ x ∈ span R (f '' s) ↔ ∃ a, (a.sum fun i c => c • f ↑i) = x
Tactic:
rw [← top_smul (span R (f '' 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
ι : Type u_3
s : Set ι
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ↑s), 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
s : Set ι
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ ∃ a, (a.sum fun i c => c • f ↑i) = x
Tactic:
apply exists_congr
State after:
case h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
⊢ ∀ (a : ↑s →₀ R), (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ (a.sum fun i c => c • f ↑i) = x

State before:
case h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
⊢ ∀ (a : ↑s →₀ R), (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ (a.sum fun i c => c • f ↑i) = x
Tactic:
intro a
State after:
case h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ (a.sum fun i c => c • f ↑i) = x

State before:
case h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ (a.sum fun i c => c • f ↑i) = x
Tactic:
constructor
State after:
case h.mp
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) → (a.sum fun i c => c • f ↑i) = x

case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x

State before:
case h.mp
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) → (a.sum fun i c => c • f ↑i) = x

case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Tactic:
. rintro ⟨_, h⟩
  exact h
State after:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x

State before:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Tactic:
. intro h
  simp only [mem_top, Subtype.forall, implies_true, exists_prop, true_and]
  exact h
State after:
no goals

State before:
case h.mp
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) → (a.sum fun i c => c • f ↑i) = x
Tactic:
rintro ⟨_, h⟩
State after:
case h.mp.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
w✝ : ∀ (i : ↑s), a i ∈ ⊤
h : (a.sum fun i c => c • f ↑i) = x
⊢ (a.sum fun i c => c • f ↑i) = x

State before:
case h.mp.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
w✝ : ∀ (i : ↑s), a i ∈ ⊤
h : (a.sum fun i c => c • f ↑i) = x
⊢ (a.sum fun i c => c • f ↑i) = x
Tactic:
exact h
State after:
no goals

State before:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Tactic:
intro h
State after:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
h : (a.sum fun i c => c • f ↑i) = x
⊢ ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x

State before:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
h : (a.sum fun i c => c • f ↑i) = x
⊢ ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Tactic:
simp only [mem_top, Subtype.forall, implies_true, exists_prop, true_and]
State after:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
h : (a.sum fun i c => c • f ↑i) = x
⊢ (a.sum fun i c => c • f ↑i) = x

State before:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
h : (a.sum fun i c => c • f ↑i) = x
⊢ (a.sum fun i c => c • f ↑i) = x
Tactic:
exact h
State after:
no goals