internlm/Lean-Github huggingface dataset:
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ Isotropic (weightedSumSquares ℚ w)
Tactic:
rw [Isotropic, Anisotropic]
Proof state after:
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ ¬∀ (x : Fin 2 → ℚ), ↑(weightedSumSquares ℚ w) x = 0 → x = 0
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ ¬∀ (x : Fin 2 → ℚ), ↑(weightedSumSquares ℚ w) x = 0 → x = 0
Tactic:
push_neg
Proof state after:
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ ∃ x, ↑(weightedSumSquares ℚ w) x = 0 ∧ x ≠ 0
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ ∃ x, ↑(weightedSumSquares ℚ w) x = 0 ∧ x ≠ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ Isotropic (weightedSumSquares ℚ w)
Tactic:
exfalso
Proof state after:
case neg.h
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.h
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ False
Tactic:
rw [EverywhereLocallyIsotropic, Isotropic, Anisotropic] at hl
Proof state after:
case neg.h
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl :
  (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
    ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.h
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl :
  (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
    ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ False
Tactic:
let a := w 1
Proof state after:
case neg.h
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl :
  (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
    ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.h
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl :
  (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
    ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
⊢ False
Tactic:
have ha : Squarefree a := hw0 1
Proof state after:
case neg.h
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl :
  (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
    ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree a
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.h
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hl :
  (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
    ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree a
⊢ False
Tactic:
rcases hl with ⟨hlf, hli⟩
Proof state after:
case neg.h.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree a
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.h.intro.inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree a
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
⊢ False
Tactic:
let n := a.natAbs
Proof state after:
case neg.h.intro.inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree a
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.h.intro.inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree a
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
⊢ False
Tactic:
have ngt1 : n > 1 := by sorry
Proof state after:
case neg.h.intro.inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree a
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
ngt1 : n > 1
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.h.intro.inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree a
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
ngt1 : n > 1
⊢ False
Tactic:
rw [← squarefree_natAbs] at ha
Proof state after:
case neg.h.intro.inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree (natAbs a)
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
ngt1 : n > 1
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.h.intro.inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree (natAbs a)
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
ngt1 : n > 1
⊢ False
Tactic:
let f := n.factors
Proof state after:
case neg.h.intro.inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree (natAbs a)
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
ngt1 : n > 1
f : List ℕ := Nat.factors n
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.h.intro.inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree (natAbs a)
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
ngt1 : n > 1
f : List ℕ := Nat.factors n
⊢ False
Tactic:
by_cases hf : f = []
Proof state after:
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree (natAbs a)
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
ngt1 : n > 1
f : List ℕ := Nat.factors n
hf : f = []
⊢ False

case neg
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree (natAbs a)
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
ngt1 : n > 1
f : List ℕ := Nat.factors n
hf : ¬f = []
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
a : ℤ := w 1
ha : Squarefree a
hlf : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
hli : ¬∀ (x : TensorProduct ℚ ℝ (Fin 2 → ℚ)), ↑(baseChange ℝ (weightedSumSquares ℚ w)) x = 0 → x = 0
hneg : a < 0
n : ℕ := natAbs a
⊢ n > 1
Tactic:
sorry
Proof state after:
no goals