case mk
R : Type u_1
M : Type u_3
r : R
x✝¹ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M ⧸ p
x : M
hx : Quot.mk Setoid.r x ∈ comap (liftQ p f h) q
⊢ Quot.mk Setoid.r x ∈ map (mkQ p) (comap f q)
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ comap (liftQ p f h) q ≤ map (mkQ p) (comap f q)
rintro ⟨x⟩ hx
no goals
case mk
R : Type u_1
M : Type u_3
r : R
x✝¹ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M ⧸ p
x : M
hx : Quot.mk Setoid.r x ∈ comap (liftQ p f h) q
⊢ Quot.mk Setoid.r x ∈ map (mkQ p) (comap f q)
exact ⟨_, hx, rfl⟩
no goals
R : Type u_1
M : Type u_3
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_2
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ map (mkQ p) (comap f q) ≤ comap (liftQ p f h) q
rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ]