R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.442039
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
S : Submodule R E
x : { x // x ∈ S ⊓ f.domain }
y : { x // x ∈ f.domain }
h : ↑x = ↑y
this : ↑(Submodule.ofLe (_ : S ⊓ f.domain ≤ f.domain)) x = y
⊢ ↑(domRestrict f S) x = ↑f y
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.442039
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
S : Submodule R E
x : { x // x ∈ S ⊓ f.domain }
y : { x // x ∈ f.domain }
h : ↑x = ↑y
⊢ ↑(domRestrict f S) x = ↑f y
have : Submodule.ofLe (by simp) x = y := by
  ext
  simp [h]
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.442039
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
S : Submodule R E
x : { x // x ∈ S ⊓ f.domain }
y : { x // x ∈ f.domain }
h : ↑x = ↑y
this : ↑(Submodule.ofLe (_ : S ⊓ f.domain ≤ f.domain)) x = y
⊢ ↑(domRestrict f S) x = ↑f (↑(Submodule.ofLe (_ : S ⊓ f.domain ≤ f.domain)) x)
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.442039
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
S : Submodule R E
x : { x // x ∈ S ⊓ f.domain }
y : { x // x ∈ f.domain }
h : ↑x = ↑y
this : ↑(Submodule.ofLe (_ : S ⊓ f.domain ≤ f.domain)) x = y
⊢ ↑(domRestrict f S) x = ↑f y
rw [← this]
no goals
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.442039
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
S : Submodule R E
x : { x // x ∈ S ⊓ f.domain }
y : { x // x ∈ f.domain }
h : ↑x = ↑y
this : ↑(Submodule.ofLe (_ : S ⊓ f.domain ≤ f.domain)) x = y
⊢ ↑(domRestrict f S) x = ↑f (↑(Submodule.ofLe (_ : S ⊓ f.domain ≤ f.domain)) x)
exact LinearPMap.mk_apply _ _ _
no goals
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.442039
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
S : Submodule R E
x : { x // x ∈ S ⊓ f.domain }
y : { x // x ∈ f.domain }
h : ↑x = ↑y
⊢ S ⊓ f.domain ≤ f.domain
simp
case a
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.442039
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
S : Submodule R E
x : { x // x ∈ S ⊓ f.domain }
y : { x // x ∈ f.domain }
h : ↑x = ↑y
⊢ ↑(↑(Submodule.ofLe (_ : S ⊓ f.domain ≤ f.domain)) x) = ↑y
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.442039
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
S : Submodule R E
x : { x // x ∈ S ⊓ f.domain }
y : { x // x ∈ f.domain }
h : ↑x = ↑y
⊢ ↑(Submodule.ofLe (_ : S ⊓ f.domain ≤ f.domain)) x = y
ext
no goals
case a
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.442039
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
S : Submodule R E
x : { x // x ∈ S ⊓ f.domain }
y : { x // x ∈ f.domain }
h : ↑x = ↑y
⊢ ↑(↑(Submodule.ofLe (_ : S ⊓ f.domain ≤ f.domain)) x) = ↑y
simp [h]