case intro.refl
R : Type u_3
R₁ : Type ?u.1263750
R₂ : Type u_2
R₃ : Type ?u.1263756
R₄ : Type ?u.1263759
S : Type ?u.1263762
K : Type ?u.1263765
K₂ : Type ?u.1263768
M : Type u_4
M' : Type ?u.1263774
M₁ : Type ?u.1263777
M₂ : Type u_1
M₃ : Type ?u.1263783
M₄ : Type ?u.1263786
N : Type ?u.1263789
N₂ : Type ?u.1263792
ι : Type ?u.1263795
V : Type ?u.1263798
V₂ : Type ?u.1263801
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₂₁ : R₂ →+* R
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
hf : range f = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
y : M
hx : ↑f y ∈ p
⊢ ↑f y ∈ p'
R : Type u_3
R₁ : Type ?u.1263750
R₂ : Type u_2
R₃ : Type ?u.1263756
R₄ : Type ?u.1263759
S : Type ?u.1263762
K : Type ?u.1263765
K₂ : Type ?u.1263768
M : Type u_4
M' : Type ?u.1263774
M₁ : Type ?u.1263777
M₂ : Type u_1
M₃ : Type ?u.1263783
M₄ : Type ?u.1263786
N : Type ?u.1263789
N₂ : Type ?u.1263792
ι : Type ?u.1263795
V : Type ?u.1263798
V₂ : Type ?u.1263801
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₂₁ : R₂ →+* R
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
hf : range f = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
x : M₂
hx : x ∈ p
⊢ x ∈ p'
rcases range_eq_top.1 hf x with ⟨y, hy, rfl⟩
no goals
case intro.refl
R : Type u_3
R₁ : Type ?u.1263750
R₂ : Type u_2
R₃ : Type ?u.1263756
R₄ : Type ?u.1263759
S : Type ?u.1263762
K : Type ?u.1263765
K₂ : Type ?u.1263768
M : Type u_4
M' : Type ?u.1263774
M₁ : Type ?u.1263777
M₂ : Type u_1
M₃ : Type ?u.1263783
M₄ : Type ?u.1263786
N : Type ?u.1263789
N₂ : Type ?u.1263792
ι : Type ?u.1263795
V : Type ?u.1263798
V₂ : Type ?u.1263801
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₂₁ : R₂ →+* R
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
hf : range f = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
y : M
hx : ↑f y ∈ p
⊢ ↑f y ∈ p'
exact H hx