-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem ker_le_iff [RingHomSurjective τ₁₂] {p : Submodule R M} :
    ker f ≤ p ↔ ∃ y ∈ range f, f ⁻¹' {y} ⊆ p

Proof state:
case mpr.intro.intro
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : 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

Tactic:
rw [SetLike.le_def]

Result:
case mpr.intro.intro
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : 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

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : 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

Tactic:
simpa only [this, add_sub_cancel_right]

Result:
no goals

Proof state:
case mpr.intro.intro.intro
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : 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

Tactic:
have hxz : z + x ∈ p := by
  apply h₂
  simp [hx, hz]

Result:
case mpr.intro.intro.intro
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : 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

Proof state:
case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ (∃ y ∈ range f, ⇑f ⁻¹' {y} ⊆ ↑p) → ker f ≤ p

Tactic:
rintro ⟨y, h₁, h₂⟩

Result:
case mpr.intro.intro
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : 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

Proof state:
case h
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ 0 ∈ range f ∧ ⇑f ⁻¹' {0} ⊆ ↑p

Tactic:
rw [← SetLike.mem_coe, range_coe]

Result:
case h
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ 0 ∈ Set.range ⇑f ∧ ⇑f ⁻¹' {0} ⊆ ↑p

Proof state:
case mp
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ ∃ y ∈ range f, ⇑f ⁻¹' {y} ⊆ ↑p

Tactic:
use 0

Result:
case h
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ 0 ∈ range f ∧ ⇑f ⁻¹' {0} ⊆ ↑p

Proof state:
case mp
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ ker f ≤ p → ∃ y ∈ range f, ⇑f ⁻¹' {y} ⊆ ↑p

Tactic:
intro h

Result:
case mp
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ ∃ y ∈ range f, ⇑f ⁻¹' {y} ⊆ ↑p

Proof state:
case h
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : ker f ≤ p
⊢ 0 ∈ Set.range ⇑f ∧ ⇑f ⁻¹' {0} ⊆ ↑p

Tactic:
exact ⟨⟨0, map_zero f⟩, h⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : 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

Tactic:
exact p.sub_mem hxz hx'

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : 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

Tactic:
obtain ⟨x, hx⟩ := h₁

Result:
case mpr.intro.intro.intro
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : 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