simp only [HasseMinkowski, Isotropic, EverywhereLocallyIsotropic] at *
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
S : QuadraticForm ℚ V₂
h : Equivalent Q S
⊢ HasseMinkowski Q ↔ HasseMinkowski S
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
S : QuadraticForm ℚ V₂
h : Equivalent Q S
⊢ (¬Anisotropic Q ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)) ∧ ¬Anisotropic (baseChange ℝ Q)) ↔
    (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] S)) ∧ ¬Anisotropic (baseChange ℝ S))