sorry
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w 0 = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
this : HasseMinkowski Q ↔ HasseMinkowski (weightedSumSquares ℚ w)
⊢ ¬Anisotropic (weightedSumSquares ℚ w) ↔
    (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
      ¬Anisotropic (baseChange ℝ (weightedSumSquares ℚ w))
no goals