internlm/Lean-Github huggingface dataset:
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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
h : ∃ x, ↑F x = 0 ∧ x ≠ 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
Tactic:
obtain ⟨x, hx, hne⟩ := h
Proof state after:
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
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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
Tactic:
constructor
Proof state after:
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
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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
Tactic:
. intro p hp
  use (1 ⊗ₜ x)
  simp only [baseChange_eval, mul_one, hx, _root_.map_zero, mul_zero, true_and]
  sorry
Proof state after:
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
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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
Tactic:
. use (1 ⊗ₜ x)
  simp only [baseChange_eval, mul_one, hx, _root_.map_zero, mul_zero, true_and]
  sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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
Tactic:
intro p hp
Proof state after:
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 : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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 : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0
Tactic:
use (1 ⊗ₜ x)
Proof state after:
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 : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(baseChange ℚ_[p] F) (1 ⊗ₜ[ℚ] x) = 0 ∧ ¬1 ⊗ₜ[ℚ] x = 0
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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 : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(baseChange ℚ_[p] F) (1 ⊗ₜ[ℚ] x) = 0 ∧ ¬1 ⊗ₜ[ℚ] x = 0
Tactic:
simp only [baseChange_eval, mul_one, hx, _root_.map_zero, mul_zero, true_and]
Proof state after:
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 : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬1 ⊗ₜ[ℚ] x = 0
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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 : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬1 ⊗ₜ[ℚ] x = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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
Tactic:
use (1 ⊗ₜ x)
Proof state after:
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
⊢ ↑(baseChange ℝ F) (1 ⊗ₜ[ℚ] x) = 0 ∧ ¬1 ⊗ₜ[ℚ] x = 0
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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
⊢ ↑(baseChange ℝ F) (1 ⊗ₜ[ℚ] x) = 0 ∧ ¬1 ⊗ₜ[ℚ] x = 0
Tactic:
simp only [baseChange_eval, mul_one, hx, _root_.map_zero, mul_zero, true_and]
Proof state after:
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
⊢ ¬1 ⊗ₜ[ℚ] x = 0
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
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
⊢ ¬1 ⊗ₜ[ℚ] x = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_of_Equivalent
Proof state before:
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
Tactic:
simp only [HasseMinkowski, Isotropic, EverywhereLocallyIsotropic] at *
Proof state after:
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))
Theorem: QuadraticForm.HasseMinkowski_of_Equivalent
Proof state before:
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))
Tactic:
simp only [anisotropic_iff _ _ h]
Proof state after:
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 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))
Theorem: QuadraticForm.HasseMinkowski_of_Equivalent
Proof state before:
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 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)]
Proof state after:
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 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))
Theorem: QuadraticForm.HasseMinkowski_of_Equivalent
Proof state before:
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 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)]
Proof state after:
no goals
Theorem: QuadraticForm.anisotropic_of_quadForm_dim_zero
Proof state before:
V : Type ?u.62236
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.62778
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h : Module.rank k W = 0
⊢ Anisotropic Q
Tactic:
intro (w : W) _
Proof state after:
V : Type ?u.62236
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.62778
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h : Module.rank k W = 0
w : W
a✝ : ↑Q w = 0
⊢ w = 0
Theorem: QuadraticForm.anisotropic_of_quadForm_dim_zero
Proof state before:
V : Type ?u.62236
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.62778
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h : Module.rank k W = 0
w : W
a✝ : ↑Q w = 0
⊢ w = 0
Tactic:
rw [rank_zero_iff_forall_zero] at h
Proof state after:
V : Type ?u.62236
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.62778
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h : ∀ (x : W), x = 0
w : W
a✝ : ↑Q w = 0
⊢ w = 0
Theorem: QuadraticForm.anisotropic_of_quadForm_dim_zero
Proof state before:
V : Type ?u.62236
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.62778
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h : ∀ (x : W), x = 0
w : W
a✝ : ↑Q w = 0
⊢ w = 0
Tactic:
exact h w
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
⊢ ∀ (F : QuadraticForm ℚ V), HasseMinkowski F
Tactic:
intro F
Proof state after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ HasseMinkowski F
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ HasseMinkowski F
Tactic:
rw [HasseMinkowski]
Proof state after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Isotropic F ↔ EverywhereLocallyIsotropic F
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Isotropic F ↔ EverywhereLocallyIsotropic F
Tactic:
constructor
Proof state after:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Isotropic F → EverywhereLocallyIsotropic F

case mpr
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ EverywhereLocallyIsotropic F → Isotropic F
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Isotropic F → EverywhereLocallyIsotropic F
Tactic:
contrapose
Proof state after:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ ¬EverywhereLocallyIsotropic F → ¬Isotropic F
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ ¬EverywhereLocallyIsotropic F → ¬Isotropic F
Tactic:
intro
Proof state after:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬Isotropic F
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬Isotropic F
Tactic:
rw [QuadraticForm.Isotropic]
Proof state after:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬¬Anisotropic F
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬¬Anisotropic F
Tactic:
simp only [not_not]
Proof state after:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ Anisotropic F
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
case mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ Anisotropic F
Tactic:
apply anisotropic_of_quadForm_dim_zero _ _ F hV
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
case mpr
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ EverywhereLocallyIsotropic F → Isotropic F
Tactic:
contrapose
Proof state after:
case mpr
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ ¬Isotropic F → ¬EverywhereLocallyIsotropic F
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
case mpr
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ ¬Isotropic F → ¬EverywhereLocallyIsotropic F
Tactic:
intro
Proof state after:
case mpr
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
⊢ ¬EverywhereLocallyIsotropic F
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
case mpr
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
⊢ ¬EverywhereLocallyIsotropic F
Tactic:
rw [QuadraticForm.EverywhereLocallyIsotropic]
Proof state after:
case mpr
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.68408
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
⊢ ¬((∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) ∧ Isotropic (baseChange ℝ F))