R : Type u_1
R₁ : Type ?u.2305340
R₂ : Type u_2
R₃ : Type ?u.2305346
R₄ : Type ?u.2305349
S : Type ?u.2305352
K : Type ?u.2305355
K₂ : Type ?u.2305358
M : Type u_3
M' : Type ?u.2305364
M₁ : Type ?u.2305367
M₂ : Type u_4
M₃ : Type ?u.2305373
M₄ : Type ?u.2305376
N : Type ?u.2305379
N₂ : Type ?u.2305382
ι : Type ?u.2305385
V : Type ?u.2305388
V₂ : Type ?u.2305391
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ ∀ ⦃x : M⦄, x ∈ comap f₁ q ⊓ comap f₂ q → x ∈ comap (f₁ + f₂) q
R : Type u_1
R₁ : Type ?u.2305340
R₂ : Type u_2
R₃ : Type ?u.2305346
R₄ : Type ?u.2305349
S : Type ?u.2305352
K : Type ?u.2305355
K₂ : Type ?u.2305358
M : Type u_3
M' : Type ?u.2305364
M₁ : Type ?u.2305367
M₂ : Type u_4
M₃ : Type ?u.2305373
M₄ : Type ?u.2305376
N : Type ?u.2305379
N₂ : Type ?u.2305382
ι : Type ?u.2305385
V : Type ?u.2305388
V₂ : Type ?u.2305391
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q
rw [SetLike.le_def]
R : Type u_1
R₁ : Type ?u.2305340
R₂ : Type u_2
R₃ : Type ?u.2305346
R₄ : Type ?u.2305349
S : Type ?u.2305352
K : Type ?u.2305355
K₂ : Type ?u.2305358
M : Type u_3
M' : Type ?u.2305364
M₁ : Type ?u.2305367
M₂ : Type u_4
M₃ : Type ?u.2305373
M₄ : Type ?u.2305376
N : Type ?u.2305379
N₂ : Type ?u.2305382
ι : Type ?u.2305385
V : Type ?u.2305388
V₂ : Type ?u.2305391
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : m ∈ comap f₁ q ⊓ comap f₂ q
⊢ m ∈ comap (f₁ + f₂) q
R : Type u_1
R₁ : Type ?u.2305340
R₂ : Type u_2
R₃ : Type ?u.2305346
R₄ : Type ?u.2305349
S : Type ?u.2305352
K : Type ?u.2305355
K₂ : Type ?u.2305358
M : Type u_3
M' : Type ?u.2305364
M₁ : Type ?u.2305367
M₂ : Type u_4
M₃ : Type ?u.2305373
M₄ : Type ?u.2305376
N : Type ?u.2305379
N₂ : Type ?u.2305382
ι : Type ?u.2305385
V : Type ?u.2305388
V₂ : Type ?u.2305391
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ ∀ ⦃x : M⦄, x ∈ comap f₁ q ⊓ comap f₂ q → x ∈ comap (f₁ + f₂) q
intro m h
R : Type u_1
R₁ : Type ?u.2305340
R₂ : Type u_2
R₃ : Type ?u.2305346
R₄ : Type ?u.2305349
S : Type ?u.2305352
K : Type ?u.2305355
K₂ : Type ?u.2305358
M : Type u_3
M' : Type ?u.2305364
M₁ : Type ?u.2305367
M₂ : Type u_4
M₃ : Type ?u.2305373
M₄ : Type ?u.2305376
N : Type ?u.2305379
N₂ : Type ?u.2305382
ι : Type ?u.2305385
V : Type ?u.2305388
V₂ : Type ?u.2305391
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : m ∈ comap f₁ q ⊓ comap f₂ q
⊢ ↑f₁ m + ↑f₂ m ∈ q
R : Type u_1
R₁ : Type ?u.2305340
R₂ : Type u_2
R₃ : Type ?u.2305346
R₄ : Type ?u.2305349
S : Type ?u.2305352
K : Type ?u.2305355
K₂ : Type ?u.2305358
M : Type u_3
M' : Type ?u.2305364
M₁ : Type ?u.2305367
M₂ : Type u_4
M₃ : Type ?u.2305373
M₄ : Type ?u.2305376
N : Type ?u.2305379
N₂ : Type ?u.2305382
ι : Type ?u.2305385
V : Type ?u.2305388
V₂ : Type ?u.2305391
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : m ∈ comap f₁ q ⊓ comap f₂ q
⊢ m ∈ comap (f₁ + f₂) q
change f₁ m + f₂ m ∈ q
R : Type u_1
R₁ : Type ?u.2305340
R₂ : Type u_2
R₃ : Type ?u.2305346
R₄ : Type ?u.2305349
S : Type ?u.2305352
K : Type ?u.2305355
K₂ : Type ?u.2305358
M : Type u_3
M' : Type ?u.2305364
M₁ : Type ?u.2305367
M₂ : Type u_4
M₃ : Type ?u.2305373
M₄ : Type ?u.2305376
N : Type ?u.2305379
N₂ : Type ?u.2305382
ι : Type ?u.2305385
V : Type ?u.2305388
V₂ : Type ?u.2305391
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : ↑f₁ m ∈ q ∧ ↑f₂ m ∈ q
⊢ ↑f₁ m + ↑f₂ m ∈ q
R : Type u_1
R₁ : Type ?u.2305340
R₂ : Type u_2
R₃ : Type ?u.2305346
R₄ : Type ?u.2305349
S : Type ?u.2305352
K : Type ?u.2305355
K₂ : Type ?u.2305358
M : Type u_3
M' : Type ?u.2305364
M₁ : Type ?u.2305367
M₂ : Type u_4
M₃ : Type ?u.2305373
M₄ : Type ?u.2305376
N : Type ?u.2305379
N₂ : Type ?u.2305382
ι : Type ?u.2305385
V : Type ?u.2305388
V₂ : Type ?u.2305391
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : m ∈ comap f₁ q ⊓ comap f₂ q
⊢ ↑f₁ m + ↑f₂ m ∈ q
replace h : f₁ m ∈ q ∧ f₂ m ∈ q := h
no goals
R : Type u_1
R₁ : Type ?u.2305340
R₂ : Type u_2
R₃ : Type ?u.2305346
R₄ : Type ?u.2305349
S : Type ?u.2305352
K : Type ?u.2305355
K₂ : Type ?u.2305358
M : Type u_3
M' : Type ?u.2305364
M₁ : Type ?u.2305367
M₂ : Type u_4
M₃ : Type ?u.2305373
M₄ : Type ?u.2305376
N : Type ?u.2305379
N₂ : Type ?u.2305382
ι : Type ?u.2305385
V : Type ?u.2305388
V₂ : Type ?u.2305391
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ M₂
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N
inst✝² : Module R N₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule R N
qₗ : Submodule R N₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
m : M
h : ↑f₁ m ∈ q ∧ ↑f₂ m ∈ q
⊢ ↑f₁ m + ↑f₂ m ∈ q
apply q.add_mem h.1 h.2