R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.446187
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.446703
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.447666
inst✝² : Semiring S
M : Type ?u.447672
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p (ker (codRestrict ?m.449728))

R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.446187
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.446703
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.447666
inst✝² : Semiring S
M : Type ?u.447672
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ IsProj ?m.449469 f

R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.446187
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.446703
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.447666
inst✝² : Semiring S
M : Type ?u.447672
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ Submodule R E
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.446187
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.446703
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.447666
inst✝² : Semiring S
M : Type ?u.447672
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p (ker f)
rw [← codRestrict_ker]
no goals
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.446187
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.446703
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.447666
inst✝² : Semiring S
M : Type ?u.447672
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p (ker (codRestrict ?m.449728))

R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.446187
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.446703
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.447666
inst✝² : Semiring S
M : Type ?u.447672
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ IsProj ?m.449469 f

R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.446187
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.446703
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.447666
inst✝² : Semiring S
M : Type ?u.447672
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ Submodule R E
exact isCompl_of_proj h.codRestrict_apply_cod