internlm/Lean-Github huggingface dataset:
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)
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
Tactic:
have : n = 1 := by 
  sorry
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 = []
this : n = 1
⊢ False
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)
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 = []
this : n = 1
⊢ False
Tactic:
sorry
Proof state after:
no goals
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 (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 = []
⊢ n = 1
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)
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
Tactic:
have hp := List.exists_mem_of_ne_nil f hf
Proof state after:
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 = []
hp : ∃ x, x ∈ f
⊢ False
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)
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 = []
hp : ∃ x, x ∈ f
⊢ False
Tactic:
rcases hp with ⟨p, hp⟩
Proof state after:
case neg.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 (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 = []
p : ℕ
hp : p ∈ f
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.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 (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 = []
p : ℕ
hp : p ∈ f
⊢ False
Tactic:
have hp2 := Nat.prime_of_mem_factors hp
Proof state after:
case neg.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 (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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.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 (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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
⊢ False
Tactic:
have : Fact (p.Prime) := by exact { out := hp2 }
Proof state after:
case neg.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 (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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.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 (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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ False
Tactic:
specialize hlf p
Proof state after:
case neg.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 (natAbs a)
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
hlf : Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.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 (natAbs a)
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
hlf : Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))
⊢ False
Tactic:
rw [Isotropic, weightedSumSquares_basechange_anisotropic_iff w, Anisotropic] at hlf
Proof state after:
case neg.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 (natAbs a)
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
hlf : ¬∀ (x : Fin 2 → ℚ_[p]), ↑(weightedSumSquares ℚ_[p] fun i => ↑(w i)) x = 0 → x = 0
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.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 (natAbs a)
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
hlf : ¬∀ (x : Fin 2 → ℚ_[p]), ↑(weightedSumSquares ℚ_[p] fun i => ↑(w i)) x = 0 → x = 0
⊢ False
Tactic:
push_neg at hlf
Proof state after:
case neg.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 (natAbs a)
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
hlf : ∃ x, ↑(weightedSumSquares ℚ_[p] fun i => ↑(w i)) x = 0 ∧ x ≠ 0
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.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 (natAbs a)
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
hlf : ∃ x, ↑(weightedSumSquares ℚ_[p] fun i => ↑(w i)) x = 0 ∧ x ≠ 0
⊢ False
Tactic:
rcases hlf with ⟨x, ⟨ hx1, hx2⟩ ⟩
Proof state after:
case neg.intro.intro.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 (natAbs a)
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
x : Fin 2 → ℚ_[p]
hx1 : ↑(weightedSumSquares ℚ_[p] fun i => ↑(w i)) x = 0
hx2 : x ≠ 0
⊢ False
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case neg.intro.intro.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 (natAbs a)
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
x : Fin 2 → ℚ_[p]
hx1 : ↑(weightedSumSquares ℚ_[p] fun i => ↑(w i)) x = 0
hx2 : x ≠ 0
⊢ False
Tactic:
simp only [weightedSumSquares_apply, smul_eq_mul, Fin.sum_univ_two] at hx1
Proof state after:
case neg.intro.intro.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 (natAbs a)
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
this : Fact (Nat.Prime p)
x : Fin 2 → ℚ_[p]
hx2 : x ≠ 0
hx1 : ↑(w 0) * (x 0 * x 0) + ↑(w 1) * (x 1 * x 1) = 0
⊢ False