case a
R : Type ?u.438555
inst✝⁹ : Ring R
E : Type ?u.438561
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.439120
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.439636
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : { x // x ∈ m }
⊢ ↑(↑(codRestrict h) ↑x) = ↑x
R : Type ?u.438555
inst✝⁹ : Ring R
E : Type ?u.438561
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.439120
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.439636
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : { x // x ∈ m }
⊢ ↑(codRestrict h) ↑x = x
ext
case a
R : Type ?u.438555
inst✝⁹ : Ring R
E : Type ?u.438561
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.439120
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.439636
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : { x // x ∈ m }
⊢ ↑f ↑x = ↑x
case a
R : Type ?u.438555
inst✝⁹ : Ring R
E : Type ?u.438561
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.439120
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.439636
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : { x // x ∈ m }
⊢ ↑(↑(codRestrict h) ↑x) = ↑x
rw [codRestrict_apply]
no goals
case a
R : Type ?u.438555
inst✝⁹ : Ring R
E : Type ?u.438561
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.439120
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.439636
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : { x // x ∈ m }
⊢ ↑f ↑x = ↑x
exact h.map_id x x.2