ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ (i : ι), span R ↑(s i)) (span R ↑t) = ⨆ (i : ι), map₂ f (span R ↑(s i)) (span R ↑t)
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ (i : ι), s i) t = ⨆ (i : ι), map₂ f (s i) t
suffices map₂ f (⨆ i, span R (s i : Set M)) (span R t) = ⨆ i, map₂ f (span R (s i)) (span R t) by
  simpa only [span_eq] using this
no goals
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ (i : ι), span R ↑(s i)) (span R ↑t) = ⨆ (i : ι), map₂ f (span R ↑(s i)) (span R ↑t)
simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]
no goals
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
this : map₂ f (⨆ (i : ι), span R ↑(s i)) (span R ↑t) = ⨆ (i : ι), map₂ f (span R ↑(s i)) (span R ↑t)
⊢ map₂ f (⨆ (i : ι), s i) t = ⨆ (i : ι), map₂ f (s i) t
simpa only [span_eq] using this