no goals
R : Type u_2
inst✝⁹ : Ring R
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.146879
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.147395
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.148358
inst✝² : Semiring S
M : Type ?u.148364
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
⊢ ↑(linearProjOfIsCompl p q h) x = 0 ↔ x ∈ q
simp [linearProjOfIsCompl]