G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : ι → M
x : M
N : Submodule R M
ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0
hx : x ∈ N
⊢ False
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : ι → M
x : M
N : Submodule R M
ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0
⊢ ¬x ∈ N
intro hx
no goals
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : ι → M
x : M
N : Submodule R M
ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0
hx : x ∈ N
⊢ False
simpa using ortho (-1) x hx