R : Type u_1
R₁ : Type ?u.1573042
R₂ : Type u_2
R₃ : Type ?u.1573048
R₄ : Type ?u.1573051
S : Type ?u.1573054
K : Type ?u.1573057
K₂ : Type ?u.1573060
M : Type u_3
M' : Type ?u.1573066
M₁ : Type ?u.1573069
M₂ : Type u_4
M₃ : Type ?u.1573075
M₄ : Type ?u.1573078
N : Type ?u.1573081
N₂ : Type ?u.1573084
ι : Type ?u.1573087
V : Type ?u.1573090
V₂ : Type ?u.1573093
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : { x // x ∈ ker f } →ₗ[R] M), comp f u = comp f v → u = v
h₁ : comp f 0 = 0
⊢ ker f = ⊥
R : Type u_1
R₁ : Type ?u.1573042
R₂ : Type u_2
R₃ : Type ?u.1573048
R₄ : Type ?u.1573051
S : Type ?u.1573054
K : Type ?u.1573057
K₂ : Type ?u.1573060
M : Type u_3
M' : Type ?u.1573066
M₁ : Type ?u.1573069
M₂ : Type u_4
M₃ : Type ?u.1573075
M₄ : Type ?u.1573078
N : Type ?u.1573081
N₂ : Type ?u.1573084
ι : Type ?u.1573087
V : Type ?u.1573090
V₂ : Type ?u.1573093
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : { x // x ∈ ker f } →ₗ[R] M), comp f u = comp f v → u = v
⊢ ker f = ⊥
have h₁ : f.comp (0 : ker f →ₗ[R] M) = 0 := comp_zero _
R : Type u_1
R₁ : Type ?u.1573042
R₂ : Type u_2
R₃ : Type ?u.1573048
R₄ : Type ?u.1573051
S : Type ?u.1573054
K : Type ?u.1573057
K₂ : Type ?u.1573060
M : Type u_3
M' : Type ?u.1573066
M₁ : Type ?u.1573069
M₂ : Type u_4
M₃ : Type ?u.1573075
M₄ : Type ?u.1573078
N : Type ?u.1573081
N₂ : Type ?u.1573084
ι : Type ?u.1573087
V : Type ?u.1573090
V₂ : Type ?u.1573093
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : { x // x ∈ ker f } →ₗ[R] M), comp f u = comp f v → u = v
h₁ : comp f 0 = 0
⊢ range 0 = ⊥
R : Type u_1
R₁ : Type ?u.1573042
R₂ : Type u_2
R₃ : Type ?u.1573048
R₄ : Type ?u.1573051
S : Type ?u.1573054
K : Type ?u.1573057
K₂ : Type ?u.1573060
M : Type u_3
M' : Type ?u.1573066
M₁ : Type ?u.1573069
M₂ : Type u_4
M₃ : Type ?u.1573075
M₄ : Type ?u.1573078
N : Type ?u.1573081
N₂ : Type ?u.1573084
ι : Type ?u.1573087
V : Type ?u.1573090
V₂ : Type ?u.1573093
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : { x // x ∈ ker f } →ₗ[R] M), comp f u = comp f v → u = v
h₁ : comp f 0 = 0
⊢ ker f = ⊥
rw [← Submodule.range_subtype (ker f),
  ← h 0 f.ker.subtype (Eq.trans h₁ (comp_ker_subtype f).symm)]
no goals
R : Type u_1
R₁ : Type ?u.1573042
R₂ : Type u_2
R₃ : Type ?u.1573048
R₄ : Type ?u.1573051
S : Type ?u.1573054
K : Type ?u.1573057
K₂ : Type ?u.1573060
M : Type u_3
M' : Type ?u.1573066
M₁ : Type ?u.1573069
M₂ : Type u_4
M₃ : Type ?u.1573075
M₄ : Type ?u.1573078
N : Type ?u.1573081
N₂ : Type ?u.1573084
ι : Type ?u.1573087
V : Type ?u.1573090
V₂ : Type ?u.1573093
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : { x // x ∈ ker f } →ₗ[R] M), comp f u = comp f v → u = v
h₁ : comp f 0 = 0
⊢ range 0 = ⊥
exact range_zero