case refine'_1
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T

case refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ 0 ∈ span R ↑T

case refine'_3
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (x y : M), (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T

case refine'_4
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (a : R) (x : M), (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T
refine' span_induction hx (fun x hx => _) _ _ _
case refine'_1.refine'_1
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ↑{x} ⊆ S

case refine'_1.refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ span R ↑{x}
case refine'_1
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T
refine' ⟨{x}, _, _⟩
no goals
case refine'_1.refine'_1
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ↑{x} ⊆ S
rwa [Finset.coe_singleton, Set.singleton_subset_iff]
case refine'_1.refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ span R {x}
case refine'_1.refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ span R ↑{x}
rw [Finset.coe_singleton]
no goals
case refine'_1.refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ span R {x}
exact Submodule.mem_span_singleton_self x
case refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x : M
hx : x ∈ span R S
⊢ ↑∅ ⊆ S ∧ 0 ∈ span R ↑∅
case refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ 0 ∈ span R ↑T
use ∅
no goals
case refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x : M
hx : x ∈ span R S
⊢ ↑∅ ⊆ S ∧ 0 ∈ span R ↑∅
simp
case refine'_3.intro.intro.intro.intro
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T
case refine'_3
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (x y : M), (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → (∃ T, ↑T ⊆ S ∧ y ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T
rintro x y ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩
case refine'_3.intro.intro.intro.intro.refine'_1
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑(X ∪ Y) ⊆ S

case refine'_3.intro.intro.intro.intro.refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ x + y ∈ span R ↑(X ∪ Y)
case refine'_3.intro.intro.intro.intro
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T
refine' ⟨X ∪ Y, _, _⟩
case refine'_3.intro.intro.intro.intro.refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ∃ y_1, y_1 ∈ span R ↑X ∧ ∃ z, z ∈ span R ↑Y ∧ y_1 + z = x + y
case refine'_3.intro.intro.intro.intro.refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ x + y ∈ span R ↑(X ∪ Y)
rw [Finset.coe_union, span_union, mem_sup]
no goals
case refine'_3.intro.intro.intro.intro.refine'_2
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ∃ y_1, y_1 ∈ span R ↑X ∧ ∃ z, z ∈ span R ↑Y ∧ y_1 + z = x + y
exact ⟨x, hxX, y, hyY, rfl⟩
case refine'_3.intro.intro.intro.intro.refine'_1
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑X ∪ ↑Y ⊆ S
case refine'_3.intro.intro.intro.intro.refine'_1
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑(X ∪ Y) ⊆ S
rw [Finset.coe_union]
no goals
case refine'_3.intro.intro.intro.intro.refine'_1
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑X ∪ ↑Y ⊆ S
exact Set.union_subset hX hY
case refine'_4.intro.intro
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
a : R
x : M
T : Finset M
hT : ↑T ⊆ S
h2 : x ∈ span R ↑T
⊢ ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T
case refine'_4
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x : M
hx : x ∈ span R S
⊢ ∀ (a : R) (x : M), (∃ T, ↑T ⊆ S ∧ x ∈ span R ↑T) → ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T
rintro a x ⟨T, hT, h2⟩
no goals
case refine'_4.intro.intro
R : Type u_2
R₂ : Type ?u.238888
K : Type ?u.238891
M : Type u_1
M₂ : Type ?u.238897
V : Type ?u.238900
S✝ : Type ?u.238903
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 S : Set M
x✝ : M
hx : x✝ ∈ span R S
a : R
x : M
T : Finset M
hT : ↑T ⊆ S
h2 : x ∈ span R ↑T
⊢ ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T
exact ⟨T, hT, smul_mem _ _ h2⟩