case intro.mk.intro
F : Type ?u.932648
R : Type u_2
R₁ : Type ?u.932056
R₂ : Type ?u.932059
R₃ : Type ?u.932062
R₄ : Type ?u.932065
S : Type ?u.932068
K : Type ?u.932071
K₂ : Type ?u.932074
M : Type u_1
M' : Type ?u.932080
M₁ : Type ?u.932083
M₂ : Type ?u.932086
M₃ : Type ?u.932089
M₄ : Type ?u.932092
N : Type ?u.932095
N₂ : Type ?u.932098
ι : Type ?u.932101
V : Type ?u.932104
V₂ : Type ?u.932107
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
sc : SemilinearMapClass F σ₁₂ M M₂
val✝ : M
h₁ : val✝ ∈ p
h₂ : { val := val✝, property := h₁ } ∈ ↑(comap (Submodule.subtype p) p')
⊢ ↑(Submodule.subtype p) { val := val✝, property := h₁ } ∈ p ⊓ p'
F : Type ?u.932648
R : Type u_2
R₁ : Type ?u.932056
R₂ : Type ?u.932059
R₃ : Type ?u.932062
R₄ : Type ?u.932065
S : Type ?u.932068
K : Type ?u.932071
K₂ : Type ?u.932074
M : Type u_1
M' : Type ?u.932080
M₁ : Type ?u.932083
M₂ : Type ?u.932086
M₃ : Type ?u.932089
M₄ : Type ?u.932092
N : Type ?u.932095
N₂ : Type ?u.932098
ι : Type ?u.932101
V : Type ?u.932104
V₂ : Type ?u.932107
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x✝ y : M
sc : SemilinearMapClass F σ₁₂ M M₂
x : M
⊢ x ∈ map (Submodule.subtype p) (comap (Submodule.subtype p) p') → x ∈ p ⊓ p'
rintro ⟨⟨_, h₁⟩, h₂, rfl⟩
no goals
case intro.mk.intro
F : Type ?u.932648
R : Type u_2
R₁ : Type ?u.932056
R₂ : Type ?u.932059
R₃ : Type ?u.932062
R₄ : Type ?u.932065
S : Type ?u.932068
K : Type ?u.932071
K₂ : Type ?u.932074
M : Type u_1
M' : Type ?u.932080
M₁ : Type ?u.932083
M₂ : Type ?u.932086
M₃ : Type ?u.932089
M₄ : Type ?u.932092
N : Type ?u.932095
N₂ : Type ?u.932098
ι : Type ?u.932101
V : Type ?u.932104
V₂ : Type ?u.932107
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
sc : SemilinearMapClass F σ₁₂ M M₂
val✝ : M
h₁ : val✝ ∈ p
h₂ : { val := val✝, property := h₁ } ∈ ↑(comap (Submodule.subtype p) p')
⊢ ↑(Submodule.subtype p) { val := val✝, property := h₁ } ∈ p ⊓ p'
exact ⟨h₁, h₂⟩