Theorem: QuadraticForm.Hasse_Minkowski_of_Equivalent (AntLorentz/HasseMinkowski2.lean)

State before:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ Hasse_Minkowski Q ↔ Hasse_Minkowski S
Tactic:
simp only [Hasse_Minkowski, Isotropic, EverywhereLocallyIsotropic] at *
State after:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q 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))

State before:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q 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))
Tactic:
simp only [anisotropic_iff _ _ h]
State after:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic S ↔
      (∀ (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))

State before:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic S ↔
      (∀ (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))
Tactic:
rw [anisotropic_iff _ _ (baseChange.Equivalent ℝ _ _ h)]
State after:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)) ∧ ¬Anisotropic (baseChange ℝ S)) ↔
    (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] S)) ∧ ¬Anisotropic (baseChange ℝ S))

State before:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)) ∧ ¬Anisotropic (baseChange ℝ S)) ↔
    (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] S)) ∧ ¬Anisotropic (baseChange ℝ S))
Tactic:
conv in (Anisotropic (baseChange _ Q)) =>
  rw [anisotropic_iff _ _ (baseChange.Equivalent (R := ℚ) ℚ_[p] _ _ h)]
State after:
no goals