R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
⊢ ↑(iSup S) ⊆ ⋃ (i : ι), ↑(S i)
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
⊢ ↑(iSup S) = ⋃ (i : ι), ↑(S i)
refine' Subset.antisymm _ (iUnion_subset <| le_iSup S)
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
⊢ ↑(span R (⋃ (i : ι), ↑(S i))) ⊆ ⋃ (i : ι), ↑(S i)
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
⊢ ↑(iSup S) ⊆ ⋃ (i : ι), ↑(S i)
suffices (span R (⋃ i, (S i : Set M)) : Set M) ⊆ ⋃ i : ι, ↑(S i) by
  simpa only [span_iUnion, span_eq] using this
case refine'_1
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
⊢ ∃ i, 0 ∈ ↑(S i)

case refine'_2
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
⊢ ∀ (x y : M) (x_1 : ι), x ∈ ↑(S x_1) → ∀ (x_2 : ι), y ∈ ↑(S x_2) → ∃ i, x + y ∈ ↑(S i)

case refine'_3
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
⊢ ∀ (a : R) (x : M) (x_1 : ι), x ∈ ↑(S x_1) → ∃ i, a • x ∈ ↑(S i)
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
⊢ ↑(span R (⋃ (i : ι), ↑(S i))) ⊆ ⋃ (i : ι), ↑(S i)
refine' fun x hx => span_induction hx (fun _ => id) _ _ _ <;> simp only [mem_iUnion, exists_imp]
no goals
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
this : ↑(span R (⋃ (i : ι), ↑(S i))) ⊆ ⋃ (i : ι), ↑(S i)
⊢ ↑(iSup S) ⊆ ⋃ (i : ι), ↑(S i)
simpa only [span_iUnion, span_eq] using this
no goals
case refine'_1
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
⊢ ∃ i, 0 ∈ ↑(S i)
exact hι.elim fun i => ⟨i, (S i).zero_mem⟩
case refine'_2
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
x y : M
i : ι
hi : x ∈ ↑(S i)
j : ι
hj : y ∈ ↑(S j)
⊢ ∃ i, x + y ∈ ↑(S i)
case refine'_2
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
⊢ ∀ (x y : M) (x_1 : ι), x ∈ ↑(S x_1) → ∀ (x_2 : ι), y ∈ ↑(S x_2) → ∃ i, x + y ∈ ↑(S i)
intro x y i hi j hj
case refine'_2.intro.intro
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
x y : M
i : ι
hi : x ∈ ↑(S i)
j : ι
hj : y ∈ ↑(S j)
k : ι
ik : S i ≤ S k
jk : S j ≤ S k
⊢ ∃ i, x + y ∈ ↑(S i)
case refine'_2
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
x y : M
i : ι
hi : x ∈ ↑(S i)
j : ι
hj : y ∈ ↑(S j)
⊢ ∃ i, x + y ∈ ↑(S i)
rcases H i j with ⟨k, ik, jk⟩
no goals
case refine'_2.intro.intro
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
x y : M
i : ι
hi : x ∈ ↑(S i)
j : ι
hj : y ∈ ↑(S j)
k : ι
ik : S i ≤ S k
jk : S j ≤ S k
⊢ ∃ i, x + y ∈ ↑(S i)
exact ⟨k, add_mem (ik hi) (jk hj)⟩
no goals
case refine'_3
R : Type u_2
R₂ : Type ?u.86611
K : Type ?u.86614
M : Type u_3
M₂ : Type ?u.86620
V : Type ?u.86623
S✝ : Type ?u.86626
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
ι : Sort u_1
hι : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ ↑(span R (⋃ (i : ι), ↑(S i)))
⊢ ∀ (a : R) (x : M) (x_1 : ι), x ∈ ↑(S x_1) → ∃ i, a • x ∈ ↑(S i)
exact fun a x i hi => ⟨i, smul_mem _ a hi⟩