R✝ : Type ?u.1110533
R₁ : Type ?u.1110536
R₂✝ : Type ?u.1110539
R₃ : Type ?u.1110542
R₄ : Type ?u.1110545
S : Type ?u.1110548
K : Type ?u.1110551
K₂ : Type ?u.1110554
M✝ : Type ?u.1110557
M' : Type ?u.1110560
M₁ : Type ?u.1110563
M₂✝ : Type ?u.1110566
M₃ : Type ?u.1110569
M₄ : Type ?u.1110572
N : Type ?u.1110575
N₂ : Type ?u.1110578
ι : Type ?u.1110581
V : Type ?u.1110584
V₂ : Type ?u.1110587
inst✝¹⁷ : Semiring R✝
inst✝¹⁶ : Semiring R₂✝
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : AddCommMonoid M₂✝
inst✝¹² : AddCommMonoid M₃
σ₁₂ : R✝ →+* R₂✝
σ₂₃ : R₂✝ →+* R₃
σ₁₃ : R✝ →+* R₃
inst✝¹¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁰ : Module R✝ M✝
inst✝⁹ : Module R₂✝ M₂✝
inst✝⁸ : Module R₃ M₃
σ₂₁ : R₂✝ →+* R✝
τ₁₂✝ : R✝ →+* R₂✝
τ₂₃ : R₂✝ →+* R₃
τ₁₃ : R✝ →+* R₃
inst✝⁷ : RingHomCompTriple τ₁₂✝ τ₂₃ τ₁₃
F : Type ?u.1110997
sc : SemilinearMapClass F τ₁₂✝ M✝ M₂✝
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range (comp (-id) f) = range f
R✝ : Type ?u.1110533
R₁ : Type ?u.1110536
R₂✝ : Type ?u.1110539
R₃ : Type ?u.1110542
R₄ : Type ?u.1110545
S : Type ?u.1110548
K : Type ?u.1110551
K₂ : Type ?u.1110554
M✝ : Type ?u.1110557
M' : Type ?u.1110560
M₁ : Type ?u.1110563
M₂✝ : Type ?u.1110566
M₃ : Type ?u.1110569
M₄ : Type ?u.1110572
N : Type ?u.1110575
N₂ : Type ?u.1110578
ι : Type ?u.1110581
V : Type ?u.1110584
V₂ : Type ?u.1110587
inst✝¹⁷ : Semiring R✝
inst✝¹⁶ : Semiring R₂✝
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : AddCommMonoid M₂✝
inst✝¹² : AddCommMonoid M₃
σ₁₂ : R✝ →+* R₂✝
σ₂₃ : R₂✝ →+* R₃
σ₁₃ : R✝ →+* R₃
inst✝¹¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁰ : Module R✝ M✝
inst✝⁹ : Module R₂✝ M₂✝
inst✝⁸ : Module R₃ M₃
σ₂₁ : R₂✝ →+* R✝
τ₁₂✝ : R✝ →+* R₂✝
τ₂₃ : R₂✝ →+* R₃
τ₁₃ : R✝ →+* R₃
inst✝⁷ : RingHomCompTriple τ₁₂✝ τ₂₃ τ₁₃
F : Type ?u.1110997
sc : SemilinearMapClass F τ₁₂✝ M✝ M₂✝
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range (-f) = range f
change range ((-LinearMap.id : M₂ →ₗ[R₂] M₂).comp f) = _
no goals
R✝ : Type ?u.1110533
R₁ : Type ?u.1110536
R₂✝ : Type ?u.1110539
R₃ : Type ?u.1110542
R₄ : Type ?u.1110545
S : Type ?u.1110548
K : Type ?u.1110551
K₂ : Type ?u.1110554
M✝ : Type ?u.1110557
M' : Type ?u.1110560
M₁ : Type ?u.1110563
M₂✝ : Type ?u.1110566
M₃ : Type ?u.1110569
M₄ : Type ?u.1110572
N : Type ?u.1110575
N₂ : Type ?u.1110578
ι : Type ?u.1110581
V : Type ?u.1110584
V₂ : Type ?u.1110587
inst✝¹⁷ : Semiring R✝
inst✝¹⁶ : Semiring R₂✝
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : AddCommMonoid M₂✝
inst✝¹² : AddCommMonoid M₃
σ₁₂ : R✝ →+* R₂✝
σ₂₃ : R₂✝ →+* R₃
σ₁₃ : R✝ →+* R₃
inst✝¹¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁰ : Module R✝ M✝
inst✝⁹ : Module R₂✝ M₂✝
inst✝⁸ : Module R₃ M₃
σ₂₁ : R₂✝ →+* R✝
τ₁₂✝ : R✝ →+* R₂✝
τ₂₃ : R₂✝ →+* R₃
τ₁₃ : R✝ →+* R₃
inst✝⁷ : RingHomCompTriple τ₁₂✝ τ₂₃ τ₁₃
F : Type ?u.1110997
sc : SemilinearMapClass F τ₁₂✝ M✝ M₂✝
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ range (comp (-id) f) = range f
rw [range_comp, Submodule.map_neg, Submodule.map_id]