R : Type u
M : Type v
F : Type ?u.87328
G : Type ?u.87331
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
r : R
N : Submodule R M
this : span R (⋃ (t : M) (_ : t ∈ N), {r • t}) = r • N
⊢ Ideal.span {r} • N = r • N
R : Type u
M : Type v
F : Type ?u.87328
G : Type ?u.87331
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
r : R
N : Submodule R M
⊢ Ideal.span {r} • N = r • N
have : span R (⋃ (t : M) (_ : t ∈ N), {r • t}) = r • N := by
  convert span_eq (r • N)
  exact (Set.image_eq_iUnion _ (N : Set M)).symm
R : Type u
M : Type v
F : Type ?u.87328
G : Type ?u.87331
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
r : R
N : Submodule R M
this : span R (⋃ (t : M) (_ : t ∈ N), {r • t}) = r • N
⊢ span R (⋃ (s : R) (_ : s ∈ {r}) (t : M) (_ : t ∈ ↑N), {s • t}) = r • N
R : Type u
M : Type v
F : Type ?u.87328
G : Type ?u.87331
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
r : R
N : Submodule R M
this : span R (⋃ (t : M) (_ : t ∈ N), {r • t}) = r • N
⊢ Ideal.span {r} • N = r • N
conv_lhs => rw [← span_eq N, span_smul_span]
no goals
R : Type u
M : Type v
F : Type ?u.87328
G : Type ?u.87331
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
r : R
N : Submodule R M
this : span R (⋃ (t : M) (_ : t ∈ N), {r • t}) = r • N
⊢ span R (⋃ (s : R) (_ : s ∈ {r}) (t : M) (_ : t ∈ ↑N), {s • t}) = r • N
simpa
case h.e'_2.h.e'_6
R : Type u
M : Type v
F : Type ?u.87328
G : Type ?u.87331
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
r : R
N : Submodule R M
⊢ (⋃ (t : M) (_ : t ∈ N), {r • t}) = ↑(r • N)
R : Type u
M : Type v
F : Type ?u.87328
G : Type ?u.87331
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
r : R
N : Submodule R M
⊢ span R (⋃ (t : M) (_ : t ∈ N), {r • t}) = r • N
convert span_eq (r • N)
no goals
case h.e'_2.h.e'_6
R : Type u
M : Type v
F : Type ?u.87328
G : Type ?u.87331
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N✝ P : Submodule R M
S : Set R
T : Set M
r : R
N : Submodule R M
⊢ (⋃ (t : M) (_ : t ∈ N), {r • t}) = ↑(r • N)
exact (Set.image_eq_iUnion _ (N : Set M)).symm