case intro.intro.intro.intro
ι : 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
p : Submodule R M
q : Submodule R N
i : M
j : N
hi : i ∈ ↑p
hj : j ∈ ↑q
⊢ (fun m n => ↑(↑f m) n) i j ∈ ↑(map₂ f p q)
ι : 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
p : Submodule R M
q : Submodule R N
⊢ image2 (fun m n => ↑(↑f m) n) ↑p ↑q ⊆ ↑(map₂ f p q)
rintro _ ⟨i, j, hi, hj, rfl⟩
no goals
case intro.intro.intro.intro
ι : 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
p : Submodule R M
q : Submodule R N
i : M
j : N
hi : i ∈ ↑p
hj : j ∈ ↑q
⊢ (fun m n => ↑(↑f m) n) i j ∈ ↑(map₂ f p q)
exact apply_mem_map₂ _ hi hj