case a
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ span R (r • s) ≤ span R s

case a
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ span R s ≤ span R (r • s)
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ span R (r • s) = span R s
apply le_antisymm
no goals
case a
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ span R (r • s) ≤ span R s
apply span_smul_le
case h.e'_3.h.e'_6
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ s = ↑(IsUnit.unit hr)⁻¹ • r • s
case a
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ span R s ≤ span R (r • s)
convert span_smul_le (r • s) ((hr.unit⁻¹ : _) : R)
case h.e'_3.h.e'_6
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ s = (↑(IsUnit.unit hr)⁻¹ * r) • s
case h.e'_3.h.e'_6
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ s = ↑(IsUnit.unit hr)⁻¹ • r • s
rw [smul_smul]
case h.e'_3.h.e'_6
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ s = 1 • s
case h.e'_3.h.e'_6
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ s = (↑(IsUnit.unit hr)⁻¹ * r) • s
erw [hr.unit.inv_val]
no goals
case h.e'_3.h.e'_6
R : Type u_2
R₂ : Type ?u.69448
K : Type ?u.69451
M : Type u_1
M₂ : Type ?u.69457
V : Type ?u.69460
S : Type ?u.69463
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
r : R
hr : IsUnit r
⊢ s = 1 • s
rw [one_smul]