Theorem: LinearMap.domRestrict_injective (Matroid/ForMathlib/LinearAlgebra/Submodule.lean)

State before:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
⊢ Function.Injective ⇑(f.domRestrict p)
Tactic:
intro x y h
State after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ x = y

State before:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ x = y
Tactic:
apply_fun (↑) using Subtype.coe_injective
State after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ ↑x = ↑y

State before:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ ↑x = ↑y
Tactic:
apply_fun f using hf
State after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ f ↑x = f ↑y

State before:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ f ↑x = f ↑y
Tactic:
simpa using h
State after:
no goals