internlm/Lean-Github huggingface dataset:
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]
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
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)
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
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 = []
p : ℕ
hp : p ∈ f
hp2 : Nat.Prime p
⊢ Fact (Nat.Prime p)
Tactic:
exact { out := hp2 }
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
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
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)
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
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)
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
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)
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
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)
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
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)
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
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)
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
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)
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
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski2
Proof 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
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)
⊢ HasseMinkowski F
Tactic:
exact HasseMinkowski_of_degenerate F hF
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof_finite
Proof state before:
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.180812
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module.Finite ℚ V
F : QuadraticForm ℚ V
⊢ HasseMinkowski F
Tactic:
match h : FiniteDimensional.finrank ℚ V with
| 0       => sorry
| 1       => sorry
| 2       => exact HasseMinkowski2 h F
| 3       => sorry
| 4       => sorry
| (n + 5) => sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof_finite
Proof state before:
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.180812
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module.Finite ℚ V
F : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 0
⊢ HasseMinkowski F
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof_finite
Proof state before:
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.180812
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module.Finite ℚ V
F : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 1
⊢ HasseMinkowski F
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof_finite
Proof state before:
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.180812
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module.Finite ℚ V
F : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
⊢ HasseMinkowski F
Tactic:
exact HasseMinkowski2 h F
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof_finite
Proof state before:
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.180812
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module.Finite ℚ V
F : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 3
⊢ HasseMinkowski F
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof_finite
Proof state before:
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.180812
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module.Finite ℚ V
F : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 4
⊢ HasseMinkowski F
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof_finite
Proof state before:
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.180812
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module.Finite ℚ V
F : QuadraticForm ℚ V
n : ℕ
h : FiniteDimensional.finrank ℚ V = Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ n))))
⊢ HasseMinkowski F
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof_infinite
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.183933
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
h : ¬Module.Finite ℚ V
F : QuadraticForm ℚ V
⊢ HasseMinkowski F
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.186171
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
⊢ HasseMinkowski F
Tactic:
cases em (Module.Finite ℚ V) with
| inl finite   => exact HasseMinkowski_proof_finite F
| inr infinite => exact HasseMinkowski_proof_infinite infinite F
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof
Proof state before:
case inl
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.186171
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
finite : Module.Finite ℚ V
⊢ HasseMinkowski F
Tactic:
exact HasseMinkowski_proof_finite F
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_proof
Proof state before:
case inr
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.186171
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
infinite : ¬Module.Finite ℚ V
⊢ HasseMinkowski F
Tactic:
exact HasseMinkowski_proof_infinite infinite F
Proof state after:
no goals
Theorem: QuadraticForm.anisotropic_of_Equivalent
Proof state before:
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
h : Equivalent Q S
⊢ Anisotropic Q → Anisotropic S
Tactic:
rcases h with ⟨val⟩
Proof state after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ Anisotropic Q → Anisotropic S
Theorem: QuadraticForm.anisotropic_of_Equivalent
Proof state before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ Anisotropic Q → Anisotropic S
Tactic:
intro h
Proof state after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : Anisotropic Q
⊢ Anisotropic S
Theorem: QuadraticForm.anisotropic_of_Equivalent
Proof state before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : Anisotropic Q
⊢ Anisotropic S
Tactic:
simp only [Anisotropic] at *
Proof state after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : ∀ (x : M), ↑Q x = 0 → x = 0
⊢ ∀ (x : M₂), ↑S x = 0 → x = 0
Theorem: QuadraticForm.anisotropic_of_Equivalent
Proof state before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : ∀ (x : M), ↑Q x = 0 → x = 0
⊢ ∀ (x : M₂), ↑S x = 0 → x = 0
Tactic:
intro x hx
Proof state after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : ∀ (x : M), ↑Q x = 0 → x = 0
x : M₂
hx : ↑S x = 0
⊢ x = 0
Theorem: QuadraticForm.anisotropic_of_Equivalent
Proof state before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : ∀ (x : M), ↑Q x = 0 → x = 0
x : M₂
hx : ↑S x = 0
⊢ x = 0
Tactic:
specialize h (val.symm x)
Proof state after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : ↑Q (↑(Isometry.symm val) x) = 0 → ↑(Isometry.symm val) x = 0
⊢ x = 0