internlm/Lean-Github huggingface dataset:
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
⊢ ¬((∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) ∧ Isotropic (baseChange ℝ F))
Tactic:
push_neg
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)
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
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) → ¬Isotropic (baseChange ℝ 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
_✝ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)
⊢ ¬Isotropic (baseChange ℝ 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
_✝ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)
⊢ ¬Isotropic (baseChange ℝ F)
Tactic:
simp only [not_not]
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)
⊢ Anisotropic (baseChange ℝ 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
_✝ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)
⊢ Anisotropic (baseChange ℝ F)
Tactic:
apply anisotropic_of_quadForm_dim_zero
Proof state after:
case mpr.h
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)
⊢ Module.rank ℝ (TensorProduct ℚ ℝ V) = 0
Theorem: QuadraticForm.HasseMinkowski0
Proof state before:
case mpr.h
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)
⊢ Module.rank ℝ (TensorProduct ℚ ℝ V) = 0
Tactic:
rw [← base_change_module_rank_preserved, hV]
Proof state after:
no goals
Theorem: QuadraticForm.isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ Isotropic Q
Tactic:
rw [QuadraticForm.Isotropic]
Proof state after:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ ¬Anisotropic Q
Theorem: QuadraticForm.isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ ¬Anisotropic Q
Tactic:
rw [QuadraticForm.Anisotropic]
Proof state after:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have h: ∃ (w : W), w ≠ 0 := by
  simpa only [ne_eq, rank_zero_iff_forall_zero, not_forall] using h₂
Proof state after:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
h : ∃ w, w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
h : ∃ w, w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
obtain ⟨w, hw⟩ := h
Proof state after:
case intro
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.isotropic_of_zero_quadForm_dim_ge1
Proof state before:
case intro
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have : Q w = 0 := by 
  rw [h₁]
  simp only [zero_apply]
Proof state after:
case intro
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
this : ↑Q w = 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.isotropic_of_zero_quadForm_dim_ge1
Proof state before:
case intro
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
this : ↑Q w = 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
tauto
Proof state after:
no goals
Theorem: QuadraticForm.isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ ∃ w, w ≠ 0
Tactic:
simpa only [ne_eq, rank_zero_iff_forall_zero, not_forall] using h₂
Proof state after:
no goals
Theorem: QuadraticForm.isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ↑Q w = 0
Tactic:
rw [h₁]
Proof state after:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ↑0 w = 0
Theorem: QuadraticForm.isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.75923
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.76465
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₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ↑0 w = 0
Tactic:
simp only [zero_apply]
Proof state after:
no goals
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
⊢ Anisotropic Q
Tactic:
rw [QuadraticForm.Anisotropic]
Proof state after:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have h: ∃ (w : W), Q w ≠ 0 := by
 rw [ne_eq, ext_iff,not_forall] at h₁
 convert h₁
Proof state after:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
h : ∃ w, ↑Q w ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
h : ∃ w, ↑Q w ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
obtain ⟨w, hw⟩ := h
Proof state after:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have h': ∀ (v : W) (h'': v ≠ 0), Q v ≠ 0 := by sorry
Proof state after:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
intro
Proof state after:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
x✝ : W
⊢ ↑Q x✝ = 0 → x✝ = 0
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
x✝ : W
⊢ ↑Q x✝ = 0 → x✝ = 0
Tactic:
contrapose
Proof state after:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
x✝ : W
⊢ ¬x✝ = 0 → ¬↑Q x✝ = 0
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
x✝ : W
⊢ ¬x✝ = 0 → ¬↑Q x✝ = 0
Tactic:
apply h'
Proof state after:
no goals
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
⊢ ∃ w, ↑Q w ≠ 0
Tactic:
rw [ne_eq, ext_iff,not_forall] at h₁
Proof state after:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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, ¬↑Q x = ↑0 x
h₂ : Module.rank k W = 1
⊢ ∃ w, ↑Q w ≠ 0
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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, ¬↑Q x = ↑0 x
h₂ : Module.rank k W = 1
⊢ ∃ w, ↑Q w ≠ 0
Tactic:
convert h₁
Proof state after:
no goals
Theorem: QuadraticForm.anisotropic_of_nonzero_quadForm_dim_1
Proof state before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
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₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
⊢ ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_of_degenerate
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q
Tactic:
have degenQ := Q.nondegenerate_of_anisotropic.mt hQ
Proof state after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
⊢ HasseMinkowski Q
Theorem: QuadraticForm.HasseMinkowski_of_degenerate
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
⊢ HasseMinkowski Q
Tactic:
have degenR := (nondegenerate_of_anisotropic _).mt (baseChange_of_degenerate (A := ℝ) _ hQ)
Proof state after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
⊢ HasseMinkowski Q
Theorem: QuadraticForm.HasseMinkowski_of_degenerate
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
⊢ HasseMinkowski Q
Tactic:
simp only [HasseMinkowski, Isotropic, degenQ, not_false_eq_true,
  EverywhereLocallyIsotropic, degenR, and_true, true_iff]
Proof state after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
⊢ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)
Theorem: QuadraticForm.HasseMinkowski_of_degenerate
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
⊢ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)
Tactic:
intro p hp
Proof state after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬Anisotropic (baseChange ℚ_[p] Q)
Theorem: QuadraticForm.HasseMinkowski_of_degenerate
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬Anisotropic (baseChange ℚ_[p] Q)
Tactic:
exact (nondegenerate_of_anisotropic (Q.baseChange ℚ_[p])).mt (baseChange_of_degenerate (A := ℚ_[p]) _ hQ)
Proof state after:
no goals
Theorem: QuadraticForm.ex
Proof state before:
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
⊢ HasseMinkowski Q
Tactic:
by_cases hQ : (associated (R₁ := ℚ) Q).Nondegenerate
Proof state after:
case pos
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)
⊢ HasseMinkowski Q

case neg
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)
⊢ HasseMinkowski Q