no goals
R : Type ?u.264287
M : Type ?u.264290
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.265303
M₂ : Type ?u.265306
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap 0 q
simp
case h.h
R : Type u_2
M : Type u_1
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) (_ : p ≤ comap 0 q)
x✝ : M
⊢ ↑(comp (mapQ p q 0 h) (mkQ p)) x✝ = ↑(comp 0 (mkQ p)) x✝
R : Type u_2
M : Type u_1
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) (_ : p ≤ comap 0 q)
⊢ mapQ p q 0 h = 0
ext
no goals
case h.h
R : Type u_2
M : Type u_1
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) (_ : p ≤ comap 0 q)
x✝ : M
⊢ ↑(comp (mapQ p q 0 h) (mkQ p)) x✝ = ↑(comp 0 (mkQ p)) x✝
simp