case h
R : Type ?u.955175
R₁ : Type ?u.955178
R₂ : Type ?u.955181
R₃ : Type ?u.955184
R₄ : Type ?u.955187
S : Type ?u.955190
K : Type u_1
K₂ : Type ?u.955196
M : Type ?u.955199
M' : Type ?u.955202
M₁ : Type ?u.955205
M₂ : Type ?u.955208
M₃ : Type ?u.955211
M₄ : Type ?u.955214
N : Type ?u.955217
N₂ : Type ?u.955220
ι : Type ?u.955223
V : Type u_2
V₂ : Type u_3
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
b : V
⊢ b ∈ comap (a • f) p ↔ b ∈ comap f p
R : Type ?u.955175
R₁ : Type ?u.955178
R₂ : Type ?u.955181
R₃ : Type ?u.955184
R₄ : Type ?u.955187
S : Type ?u.955190
K : Type u_1
K₂ : Type ?u.955196
M : Type ?u.955199
M' : Type ?u.955202
M₁ : Type ?u.955205
M₂ : Type ?u.955208
M₃ : Type ?u.955211
M₄ : Type ?u.955214
N : Type ?u.955217
N₂ : Type ?u.955220
ι : Type ?u.955223
V : Type u_2
V₂ : Type u_3
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
⊢ comap (a • f) p = comap f p
ext b
no goals
case h
R : Type ?u.955175
R₁ : Type ?u.955178
R₂ : Type ?u.955181
R₃ : Type ?u.955184
R₄ : Type ?u.955187
S : Type ?u.955190
K : Type u_1
K₂ : Type ?u.955196
M : Type ?u.955199
M' : Type ?u.955202
M₁ : Type ?u.955205
M₂ : Type ?u.955208
M₃ : Type ?u.955211
M₄ : Type ?u.955214
N : Type ?u.955217
N₂ : Type ?u.955220
ι : Type ?u.955223
V : Type u_2
V₂ : Type u_3
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
b : V
⊢ b ∈ comap (a • f) p ↔ b ∈ comap f p
simp only [Submodule.mem_comap, p.smul_mem_iff h, LinearMap.smul_apply]