R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x : M
⊢ x ∈ (⨆ (i : ι), p i).toAddSubmonoid → x ∈ ⨆ (i : ι), (p i).toAddSubmonoid
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
⊢ (⨆ (i : ι), p i).toAddSubmonoid = ⨆ (i : ι), (p i).toAddSubmonoid
refine' le_antisymm (fun x => _) (iSup_le fun i => toAddSubmonoid_mono <| le_iSup _ i)
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x : M
⊢ x ∈ span R (⋃ (i : ι), ↑(p i)) → x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x : M
⊢ x ∈ (⨆ (i : ι), p i).toAddSubmonoid → x ∈ ⨆ (i : ι), (p i).toAddSubmonoid
simp_rw [iSup_eq_span, AddSubmonoid.iSup_eq_closure, mem_toAddSubmonoid, coe_toAddSubmonoid]
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x : M
hx : x ∈ span R (⋃ (i : ι), ↑(p i))
⊢ x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x : M
⊢ x ∈ span R (⋃ (i : ι), ↑(p i)) → x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
intro hx
case refine'_1
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
x : M
hx : x ∈ ⋃ (i : ι), ↑(p i)
⊢ x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))

case refine'_2
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x : M
hx : x ∈ span R (⋃ (i : ι), ↑(p i))
⊢ 0 ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))

case refine'_3
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
x y : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
hy : y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ x + y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))

case refine'_4
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x : M
hx : x ∈ span R (⋃ (i : ι), ↑(p i))
⊢ x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
refine' Submodule.span_induction hx (fun x hx => _) _ (fun x y hx hy => _) fun r x hx => _
no goals
case refine'_1
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
x : M
hx : x ∈ ⋃ (i : ι), ↑(p i)
⊢ x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
exact AddSubmonoid.subset_closure hx
no goals
case refine'_2
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x : M
hx : x ∈ span R (⋃ (i : ι), ↑(p i))
⊢ 0 ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
exact AddSubmonoid.zero_mem _
no goals
case refine'_3
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
x y : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
hy : y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ x + y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
exact AddSubmonoid.add_mem _ hx hy
case refine'_4.refine_1
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ ∀ (x : M), (x ∈ ⋃ (i : ι), ↑(p i)) → r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))

case refine'_4.refine_2
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ r • 0 ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))

case refine'_4.refine_3
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ ∀ (x y : M),
    r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i)) →
      r • y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i)) → r • (x + y) ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
case refine'_4
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
refine AddSubmonoid.closure_induction hx ?_ ?_ ?_
case refine'_4.refine_1.intro.intro.intro
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x✝ : M
hx : x✝ ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
x : M
i : ι
hix : x ∈ p i
⊢ r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
case refine'_4.refine_1
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ ∀ (x : M), (x ∈ ⋃ (i : ι), ↑(p i)) → r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
rintro x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x✝ : M
hx : x✝ ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
x : M
i : ι
hix : x ∈ p i
⊢ r • x ∈ ↑(p i)
case refine'_4.refine_1.intro.intro.intro
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x✝ : M
hx : x✝ ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
x : M
i : ι
hix : x ∈ p i
⊢ r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)
no goals
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x✝ : M
hx : x✝ ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
x : M
i : ι
hix : x ∈ p i
⊢ r • x ∈ ↑(p i)
exact smul_mem _ r hix
case refine'_4.refine_2
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ 0 ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
case refine'_4.refine_2
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ r • 0 ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
rw [smul_zero]
no goals
case refine'_4.refine_2
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ 0 ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
exact AddSubmonoid.zero_mem _
case refine'_4.refine_3
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝¹ : M
hx✝¹ : x✝¹ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
x y : M
hx : r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
hy : r • y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ r • (x + y) ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
case refine'_4.refine_3
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x : M
hx : x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ ∀ (x y : M),
    r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i)) →
      r • y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i)) → r • (x + y) ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
intro x y hx hy
case refine'_4.refine_3
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝¹ : M
hx✝¹ : x✝¹ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
x y : M
hx : r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
hy : r • y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ r • x + r • y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
case refine'_4.refine_3
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝¹ : M
hx✝¹ : x✝¹ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
x y : M
hx : r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
hy : r • y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ r • (x + y) ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
rw [smul_add]
no goals
case refine'_4.refine_3
R : Type u_2
R₂ : Type ?u.211571
K : Type ?u.211574
M : Type u_3
M₂ : Type ?u.211580
V : Type ?u.211583
S : Type ?u.211586
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
p : ι → Submodule R M
x✝¹ : M
hx✝¹ : x✝¹ ∈ span R (⋃ (i : ι), ↑(p i))
r : R
x✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
x y : M
hx : r • x ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
hy : r • y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
⊢ r • x + r • y ∈ AddSubmonoid.closure (⋃ (i : ι), ↑(p i))
exact AddSubmonoid.add_mem _ hx hy