case intro.intro.intro
F : Type u_5
R : Type u_1
R₁ : Type ?u.928463
R₂ : Type u_2
R₃ : Type ?u.928469
R₄ : Type ?u.928472
S : Type ?u.928475
K : Type ?u.928478
K₂ : Type ?u.928481
M : Type u_3
M' : Type ?u.928487
M₁ : Type ?u.928490
M₂ : Type u_4
M₃ : Type ?u.928496
M₄ : Type ?u.928499
N : Type ?u.928502
N₂ : Type ?u.928505
ι : Type ?u.928508
V : Type ?u.928511
V₂ : Type ?u.928514
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₂
inst✝ : RingHomSurjective σ₁₂
f : F
p : Submodule R M
p' : Submodule R₂ M₂
x : M
h₁ : x ∈ ↑p
h₂ : ↑f x ∈ ↑p'
⊢ ↑f x ∈ map f (p ⊓ comap f p')
F : Type u_5
R : Type u_1
R₁ : Type ?u.928463
R₂ : Type u_2
R₃ : Type ?u.928469
R₄ : Type ?u.928472
S : Type ?u.928475
K : Type ?u.928478
K₂ : Type ?u.928481
M : Type u_3
M' : Type ?u.928487
M₁ : Type ?u.928490
M₂ : Type u_4
M₃ : Type ?u.928496
M₄ : Type ?u.928499
N : Type ?u.928502
N₂ : Type ?u.928505
ι : Type ?u.928508
V : Type ?u.928511
V₂ : Type ?u.928514
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₂
inst✝ : RingHomSurjective σ₁₂
f : F
p : Submodule R M
p' : Submodule R₂ M₂
⊢ map f p ⊓ p' ≤ map f (p ⊓ comap f p')
rintro _ ⟨⟨x, h₁, rfl⟩, h₂⟩
no goals
case intro.intro.intro
F : Type u_5
R : Type u_1
R₁ : Type ?u.928463
R₂ : Type u_2
R₃ : Type ?u.928469
R₄ : Type ?u.928472
S : Type ?u.928475
K : Type ?u.928478
K₂ : Type ?u.928481
M : Type u_3
M' : Type ?u.928487
M₁ : Type ?u.928490
M₂ : Type u_4
M₃ : Type ?u.928496
M₄ : Type ?u.928499
N : Type ?u.928502
N₂ : Type ?u.928505
ι : Type ?u.928508
V : Type ?u.928511
V₂ : Type ?u.928514
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₂
inst✝ : RingHomSurjective σ₁₂
f : F
p : Submodule R M
p' : Submodule R₂ M₂
x : M
h₁ : x ∈ ↑p
h₂ : ↑f x ∈ ↑p'
⊢ ↑f x ∈ map f (p ⊓ comap f p')
exact ⟨_, ⟨h₁, h₂⟩, rfl⟩