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

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
⊢ HasseMinkowski F
Tactic:
by_cases hF : (associated (R₁ := ℚ) F).Nondegenerate
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)
⊢ HasseMinkowski F

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)
⊢ HasseMinkowski F

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)
⊢ HasseMinkowski F
Tactic:
have hV0 : 0 < FiniteDimensional.finrank ℚ V := by rw [hV]; norm_num
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
⊢ HasseMinkowski F

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
⊢ HasseMinkowski F
Tactic:
obtain ⟨w, hw1, hw0, hEF⟩ := equivalent_weightedSumSquares_units_of_nondegenerate'' F hV0 hV.symm hF
State after:
case pos.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)
⊢ HasseMinkowski F

State before:
case pos.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)
⊢ HasseMinkowski F
Tactic:
rw [HasseMinkowski_of_Equivalent (V := V) hEF, HasseMinkowski]
State after:
case pos.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)
⊢ Isotropic (weightedSumSquares ℚ w) ↔ EverywhereLocallyIsotropic (weightedSumSquares ℚ w)

State before:
case pos.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)
⊢ Isotropic (weightedSumSquares ℚ w) ↔ EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
Tactic:
constructor
State after:
case pos.intro.intro.intro.mp
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)
⊢ Isotropic (weightedSumSquares ℚ w) → EverywhereLocallyIsotropic (weightedSumSquares ℚ w)

case pos.intro.intro.intro.mpr
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)
⊢ EverywhereLocallyIsotropic (weightedSumSquares ℚ w) → Isotropic (weightedSumSquares ℚ w)

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)
⊢ 0 < FiniteDimensional.finrank ℚ V
Tactic:
rw [hV]
State after:
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)
⊢ 0 < 2

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)
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
case pos.intro.intro.intro.mp
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)
⊢ Isotropic (weightedSumSquares ℚ w) → EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
Tactic:
intro h
State after:
case pos.intro.intro.intro.mp
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)
h : Isotropic (weightedSumSquares ℚ w)
⊢ EverywhereLocallyIsotropic (weightedSumSquares ℚ w)

State before:
case pos.intro.intro.intro.mp
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)
h : Isotropic (weightedSumSquares ℚ w)
⊢ EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
Tactic:
exact HasseMinkowski_global_to_local _ h
State after:
no goals

State before:
case pos.intro.intro.intro.mpr
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)
⊢ EverywhereLocallyIsotropic (weightedSumSquares ℚ w) → Isotropic (weightedSumSquares ℚ w)
Tactic:
intro hl
State after:
case pos.intro.intro.intro.mpr
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)
⊢ Isotropic (weightedSumSquares ℚ w)

State before:
case pos.intro.intro.intro.mpr
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)
⊢ Isotropic (weightedSumSquares ℚ w)
Tactic:
by_cases hw : w ⟨1, (by norm_num)⟩ = -1
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
⊢ Isotropic (weightedSumSquares ℚ w)

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)

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
State after:
no goals

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]
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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⟩
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

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
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

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
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

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
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

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
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

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 = []
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

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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⟩
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

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
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

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 }
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

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
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

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
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

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
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

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⟩ ⟩
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

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
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

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]
hx2 : x ≠ 0
hx1 : ↑(w 0) * (x 0 * x 0) + ↑(w 1) * (x 1 * x 1) = 0
⊢ False
Tactic:
by_cases hx3 : x 0 = 0
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)
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
hx3 : x 0 = 0
⊢ 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)
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
hx3 : ¬x 0 = 0
⊢ False

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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
⊢ Fact (Nat.Prime p)
Tactic:
exact { out := hp2 }
State after:
no goals

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)
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
hx3 : x 0 = 0
⊢ False
Tactic:
have : x = 0 := by
  simp?
  sorry
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)
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
hx3 : x 0 = 0
this : x = 0
⊢ False

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)
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
hx3 : x 0 = 0
this : x = 0
⊢ False
Tactic:
exact hx2 this
State after:
no goals

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)
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
hx3 : x 0 = 0
⊢ x = 0
Tactic:
sorry
State after:
no goals

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)
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
hx3 : ¬x 0 = 0
⊢ False
Tactic:
have : (w 1 : ℚ_[p]) * (x 1 * x 1) = -(x 0 * x 0) := by sorry
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)
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
hx3 : ¬x 0 = 0
this : ↑(w 1) * (x 1 * x 1) = -(x 0 * x 0)
⊢ False

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)
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
hx3 : ¬x 0 = 0
this : ↑(w 1) * (x 1 * x 1) = -(x 0 * x 0)
⊢ False
Tactic:
sorry
State after:
no goals

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)
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
hx3 : ¬x 0 = 0
⊢ ↑(w 1) * (x 1 * x 1) = -(x 0 * x 0)
Tactic:
sorry
State after:
no goals

State before:
case neg.h.intro.inr
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
hpos : a > 0
⊢ False
Tactic:
sorry
State after:
no goals

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)
⊢ HasseMinkowski F
Tactic:
exact HasseMinkowski_of_degenerate F hF
State after:
no goals