constructor
case intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0

case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0