S : Type ?u.491077
R : Type ?u.491080
R₁ : Type ?u.491083
M : Type u_1
R₂ : Type u
inst✝² : OrderedRing R₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R₂ M
Q₂ : QuadraticForm R₂ M
n : Type ?u.491349
Q : QuadraticForm R₂ M
hQ : PosDef Q
x : M
hQx : ↑Q x = 0
hx : ¬x = 0
this : 0 < ↑Q x
⊢ 0 < 0
S : Type ?u.491077
R : Type ?u.491080
R₁ : Type ?u.491083
M : Type u_1
R₂ : Type u
inst✝² : OrderedRing R₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R₂ M
Q₂ : QuadraticForm R₂ M
n : Type ?u.491349
Q : QuadraticForm R₂ M
hQ : PosDef Q
x : M
hQx : ↑Q x = 0
hx : ¬x = 0
⊢ 0 < 0
have := hQ _ hx
S : Type ?u.491077
R : Type ?u.491080
R₁ : Type ?u.491083
M : Type u_1
R₂ : Type u
inst✝² : OrderedRing R₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R₂ M
Q₂ : QuadraticForm R₂ M
n : Type ?u.491349
Q : QuadraticForm R₂ M
hQ : PosDef Q
x : M
hQx : ↑Q x = 0
hx : ¬x = 0
this : 0 < 0
⊢ 0 < 0
S : Type ?u.491077
R : Type ?u.491080
R₁ : Type ?u.491083
M : Type u_1
R₂ : Type u
inst✝² : OrderedRing R₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R₂ M
Q₂ : QuadraticForm R₂ M
n : Type ?u.491349
Q : QuadraticForm R₂ M
hQ : PosDef Q
x : M
hQx : ↑Q x = 0
hx : ¬x = 0
this : 0 < ↑Q x
⊢ 0 < 0
rw [hQx] at this
no goals
S : Type ?u.491077
R : Type ?u.491080
R₁ : Type ?u.491083
M : Type u_1
R₂ : Type u
inst✝² : OrderedRing R₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R₂ M
Q₂ : QuadraticForm R₂ M
n : Type ?u.491349
Q : QuadraticForm R₂ M
hQ : PosDef Q
x : M
hQx : ↑Q x = 0
hx : ¬x = 0
this : 0 < 0
⊢ 0 < 0
exact this