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

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

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

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