R : Type u_2
R₂ : Type ?u.162771
K : Type ?u.162774
M : Type u_1
M₂ : Type ?u.162780
V : Type ?u.162783
S : Type ?u.162786
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
y : M
⊢ (∃ y_1, y_1 ∈ span R s ∧ ∃ a, y_1 + a • y = x) ↔ ∃ a z, z ∈ span R s ∧ x = a • y + z
R : Type u_2
R₂ : Type ?u.162771
K : Type ?u.162774
M : Type u_1
M₂ : Type ?u.162780
V : Type ?u.162783
S : Type ?u.162786
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
y : M
⊢ x ∈ span R (insert y s) ↔ ∃ a z, z ∈ span R s ∧ x = a • y + z
simp only [← union_singleton, span_union, mem_sup, mem_span_singleton, exists_prop,
  exists_exists_eq_and]
R : Type u_2
R₂ : Type ?u.162771
K : Type ?u.162774
M : Type u_1
M₂ : Type ?u.162780
V : Type ?u.162783
S : Type ?u.162786
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
y : M
⊢ (∃ y_1, y_1 ∈ span R s ∧ ∃ a, y_1 + a • y = x) ↔ ∃ b a, b ∈ span R s ∧ x = a • y + b
R : Type u_2
R₂ : Type ?u.162771
K : Type ?u.162774
M : Type u_1
M₂ : Type ?u.162780
V : Type ?u.162783
S : Type ?u.162786
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
y : M
⊢ (∃ y_1, y_1 ∈ span R s ∧ ∃ a, y_1 + a • y = x) ↔ ∃ a z, z ∈ span R s ∧ x = a • y + z
rw [exists_comm]
no goals
R : Type u_2
R₂ : Type ?u.162771
K : Type ?u.162774
M : Type u_1
M₂ : Type ?u.162780
V : Type ?u.162783
S : Type ?u.162786
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
y : M
⊢ (∃ y_1, y_1 ∈ span R s ∧ ∃ a, y_1 + a • y = x) ↔ ∃ b a, b ∈ span R s ∧ x = a • y + b
simp only [eq_comm, add_comm, exists_and_left]