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

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

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

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

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

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

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

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