R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a z, z ∈ span R s ∧ x = a • y + z) ↔ ∃ a, x + a • y ∈ span R s
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ x ∈ span R (insert y s) ↔ ∃ a, x + a • y ∈ span R s
rw [mem_span_insert]
case mp
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a z, z ∈ span R s ∧ x = a • y + z) → ∃ a, x + a • y ∈ span R s

case mpr
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, x + a • y ∈ span R s) → ∃ a z, z ∈ span R s ∧ x = a • y + z
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a z, z ∈ span R s ∧ x = a • y + z) ↔ ∃ a, x + a • y ∈ span R s
constructor
case mp.intro.intro.intro
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
y : M
s : Set M
a : R
z : M
hz : z ∈ span R s
⊢ ∃ a_1, a • y + z + a_1 • y ∈ span R s
case mp
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a z, z ∈ span R s ∧ x = a • y + z) → ∃ a, x + a • y ∈ span R s
rintro ⟨a, z, hz, rfl⟩
no goals
case mp.intro.intro.intro
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
y : M
s : Set M
a : R
z : M
hz : z ∈ span R s
⊢ ∃ a_1, a • y + z + a_1 • y ∈ span R s
exact ⟨-a, by simp [hz, add_assoc]⟩
no goals
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
y : M
s : Set M
a : R
z : M
hz : z ∈ span R s
⊢ a • y + z + -a • y ∈ span R s
simp [hz, add_assoc]
case mpr.intro
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
a : R
h : x + a • y ∈ span R s
⊢ ∃ a z, z ∈ span R s ∧ x = a • y + z
case mpr
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, x + a • y ∈ span R s) → ∃ a z, z ∈ span R s ∧ x = a • y + z
rintro ⟨a, h⟩
no goals
case mpr.intro
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
a : R
h : x + a • y ∈ span R s
⊢ ∃ a z, z ∈ span R s ∧ x = a • y + z
exact ⟨-a, _, h, by simp [add_comm, add_left_comm]⟩
no goals
R : Type u_2
R₂ : Type ?u.280792
K : Type ?u.280795
M : Type u_1
M₂ : Type ?u.280801
V : Type ?u.280804
S : Type ?u.280807
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
a : R
h : x + a • y ∈ span R s
⊢ x = -a • y + (x + a • y)
simp [add_comm, add_left_comm]