case mp
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ ker f ≤ p → ∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑p

case mpr
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ (∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑p) → ker f ≤ p
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ ker f ≤ p ↔ ∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑p
constructor
case mp
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ ∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑p
case mp
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ ker f ≤ p → ∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑p
intro h
case mp
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ 0 ∈ range f ∧ ↑f ⁻¹' {0} ⊆ ↑p
case mp
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ ∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑p
use 0
case mp
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ 0 ∈ Set.range ↑f ∧ ↑f ⁻¹' {0} ⊆ ↑p
case mp
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ 0 ∈ range f ∧ ↑f ⁻¹' {0} ⊆ ↑p
rw [← SetLike.mem_coe, range_coe]
no goals
case mp
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ 0 ∈ Set.range ↑f ∧ ↑f ⁻¹' {0} ⊆ ↑p
exact ⟨⟨0, map_zero f⟩, h⟩
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ range f
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
⊢ ker f ≤ p
case mpr
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ (∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑p) → ker f ≤ p
rintro ⟨y, h₁, h₂⟩
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ range f
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
⊢ ∀ ⦃x : M⦄, x ∈ ker f → x ∈ p
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ range f
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
⊢ ker f ≤ p
rw [SetLike.le_def]
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ range f
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : z ∈ ker f
⊢ z ∈ p
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ range f
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
⊢ ∀ ⦃x : M⦄, x ∈ ker f → x ∈ p
intro z hz
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ range f
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
⊢ z ∈ p
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ range f
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : z ∈ ker f
⊢ z ∈ p
simp only [mem_ker, SetLike.mem_coe] at hz
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : ∃ y_1, ↑f y_1 = y
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
⊢ z ∈ p
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ range f
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
⊢ z ∈ p
rw [← SetLike.mem_coe, range_coe, Set.mem_range] at h₁
case mpr.intro.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
⊢ z ∈ p
case mpr.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : ∃ y_1, ↑f y_1 = y
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
⊢ z ∈ p
obtain ⟨x, hx⟩ := h₁
case mpr.intro.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
⊢ z ∈ p
case mpr.intro.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
⊢ z ∈ p
have hx' : x ∈ p := h₂ hx
case mpr.intro.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z ∈ p
case mpr.intro.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
⊢ z ∈ p
have hxz : z + x ∈ p := by
  apply h₂
  simp [hx, hz]
case mpr.intro.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z + x - x ∈ p
case mpr.intro.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z ∈ p
suffices z + x - x ∈ p by simpa only [this, add_sub_cancel]
no goals
case mpr.intro.intro.intro
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z + x - x ∈ p
exact p.sub_mem hxz hx'
case a
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
⊢ z + x ∈ ↑f ⁻¹' {y}
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
⊢ z + x ∈ p
apply h₂
no goals
case a
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
⊢ z + x ∈ ↑f ⁻¹' {y}
simp [hx, hz]
no goals
R : Type u_1
R₁ : Type ?u.1458730
R₂ : Type u_2
R₃ : Type ?u.1458736
R₄ : Type ?u.1458739
S : Type ?u.1458742
K : Type ?u.1458745
K₂ : Type ?u.1458748
M : Type u_3
M' : Type ?u.1458754
M₁ : Type ?u.1458757
M₂ : Type u_4
M₃ : Type ?u.1458763
M₄ : Type ?u.1458766
N : Type ?u.1458769
N₂ : Type ?u.1458772
ι : Type ?u.1458775
V : Type ?u.1458778
V₂ : Type ?u.1458781
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ↑f ⁻¹' {y} ⊆ ↑p
z : M
hz : ↑f z = 0
x : M
hx : ↑f x = y
hx' : x ∈ p
hxz : z + x ∈ p
this : z + x - x ∈ p
⊢ z ∈ p
simpa only [this, add_sub_cancel]