α : Type u_2
M : Type u_3
N : Type ?u.243431
P : Type ?u.243434
R : Type u_4
S : Type ?u.243440
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_1
α'' : Type ?u.243535
f : α → α'
s : Set α'
l : α →₀ M
hl✝ : f '' ↑l.support ⊆ s
hl : ↑(Finset.image f l.support) ⊆ s
⊢ ↑(mapDomain f l).support ⊆ s
α : Type u_2
M : Type u_3
N : Type ?u.243431
P : Type ?u.243434
R : Type u_4
S : Type ?u.243440
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_1
α'' : Type ?u.243535
f : α → α'
s : Set α'
l : α →₀ M
hl : ↑l.support ⊆ f ⁻¹' s
⊢ ↑(mapDomain f l).support ⊆ s
rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
no goals
α : Type u_2
M : Type u_3
N : Type ?u.243431
P : Type ?u.243434
R : Type u_4
S : Type ?u.243440
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_1
α'' : Type ?u.243535
f : α → α'
s : Set α'
l : α →₀ M
hl✝ : f '' ↑l.support ⊆ s
hl : ↑(Finset.image f l.support) ⊆ s
⊢ ↑(mapDomain f l).support ⊆ s
exact Set.Subset.trans mapDomain_support hl