-- Mathlib/Algebra/Module/Submodule/Ker.lean
@[simp] lemma injective_domRestrict_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
    Injective (f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
⊢ Injective ⇑(f.domRestrict S) ↔ S ⊓ ker f = ⊥

Tactic:
rw [← LinearMap.ker_eq_bot]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
⊢ ker (f.domRestrict S) = ⊥ ↔ S ⊓ ker f = ⊥

Proof state:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : ker (f.domRestrict S) = ⊥
x : M
hx : x ∈ ↑S
h'x : x ∈ ↑(ker f)
this : ⟨x, hx⟩ ∈ ker (f.domRestrict S)
⊢ x ∈ ⊥

Tactic:
rw [h] at this

Result:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : ker (f.domRestrict S) = ⊥
x : M
hx : x ∈ ↑S
h'x : x ∈ ↑(ker f)
this : ⟨x, hx⟩ ∈ ⊥
⊢ x ∈ ⊥

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
⊢ ker (f.domRestrict S) = ⊥ ↔ S ⊓ ker f = ⊥

Tactic:
refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩

Result:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : ker (f.domRestrict S) = ⊥
⊢ S ⊓ ker f ≤ ⊥

case refine_2
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ ker f = ⊥
⊢ ker (f.domRestrict S) ≤ ⊥

Proof state:
case refine_2.mk
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ ker f = ⊥
x : M
hx : x ∈ S
h'x : ⟨x, hx⟩ ∈ ker (f.domRestrict S)
this : x ∈ S ⊓ ker f
⊢ ⟨x, hx⟩ ∈ ⊥

Tactic:
rw [h] at this

Result:
case refine_2.mk
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ ker f = ⊥
x : M
hx : x ∈ S
h'x : ⟨x, hx⟩ ∈ ker (f.domRestrict S)
this : x ∈ ⊥
⊢ ⟨x, hx⟩ ∈ ⊥

Proof state:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : ker (f.domRestrict S) = ⊥
⊢ S ⊓ ker f ≤ ⊥

Tactic:
intro x ⟨hx, h'x⟩

Result:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : ker (f.domRestrict S) = ⊥
x : M
hx : x ∈ ↑S
h'x : x ∈ ↑(ker f)
⊢ x ∈ ⊥

Proof state:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : ker (f.domRestrict S) = ⊥
x : M
hx : x ∈ ↑S
h'x : x ∈ ↑(ker f)
⊢ x ∈ ⊥

Tactic:
have : ⟨x, hx⟩ ∈ LinearMap.ker (LinearMap.domRestrict f S) := by simpa using h'x

Result:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : ker (f.domRestrict S) = ⊥
x : M
hx : x ∈ ↑S
h'x : x ∈ ↑(ker f)
this : ⟨x, hx⟩ ∈ ker (f.domRestrict S)
⊢ x ∈ ⊥

Proof state:
case refine_2.mk
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ ker f = ⊥
x : M
hx : x ∈ S
h'x : ⟨x, hx⟩ ∈ ker (f.domRestrict S)
this : x ∈ ⊥
⊢ ⟨x, hx⟩ ∈ ⊥

Tactic:
simpa [mk_eq_zero] using this

Result:
no goals

Proof state:
case refine_2
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ ker f = ⊥
⊢ ker (f.domRestrict S) ≤ ⊥

Tactic:
rintro ⟨x, hx⟩ h'x

Result:
case refine_2.mk
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ ker f = ⊥
x : M
hx : x ∈ S
h'x : ⟨x, hx⟩ ∈ ker (f.domRestrict S)
⊢ ⟨x, hx⟩ ∈ ⊥

Proof state:
case refine_2.mk
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ ker f = ⊥
x : M
hx : x ∈ S
h'x : ⟨x, hx⟩ ∈ ker (f.domRestrict S)
⊢ ⟨x, hx⟩ ∈ ⊥

Tactic:
have : x ∈ S ⊓ LinearMap.ker f := ⟨hx, h'x⟩

Result:
case refine_2.mk
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊓ ker f = ⊥
x : M
hx : x ∈ S
h'x : ⟨x, hx⟩ ∈ ker (f.domRestrict S)
this : x ∈ S ⊓ ker f
⊢ ⟨x, hx⟩ ∈ ⊥

Proof state:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : ker (f.domRestrict S) = ⊥
x : M
hx : x ∈ ↑S
h'x : x ∈ ↑(ker f)
this : ⟨x, hx⟩ ∈ ⊥
⊢ x ∈ ⊥

Tactic:
simpa [mk_eq_zero] using this

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : ker (f.domRestrict S) = ⊥
x : M
hx : x ∈ ↑S
h'x : x ∈ ↑(ker f)
⊢ ⟨x, hx⟩ ∈ ker (f.domRestrict S)

Tactic:
simpa using h'x

Result:
no goals