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

State before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
⊢ Anisotropic Q
Tactic:
rw [QuadraticForm.Anisotropic]
State after:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
⊢ ∀ (x : W), ↑Q x = 0 → x = 0

State before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have h: ∃ (w : W), Q w ≠ 0 := by
 rw [ne_eq, ext_iff,not_forall] at h₁
 convert h₁
State after:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
h : ∃ w, ↑Q w ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0

State before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
h : ∃ w, ↑Q w ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
obtain ⟨w, hw⟩ := h
State after:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0

State before:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have h': ∀ (v : W) (h'': v ≠ 0), Q v ≠ 0 := by sorry
State after:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0

State before:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
⊢ ∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
intro
State after:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
x✝ : W
⊢ ↑Q x✝ = 0 → x✝ = 0

State before:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
x✝ : W
⊢ ↑Q x✝ = 0 → x✝ = 0
Tactic:
contrapose
State after:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
x✝ : W
⊢ ¬x✝ = 0 → ¬↑Q x✝ = 0

State before:
case intro
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
h' : ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
x✝ : W
⊢ ¬x✝ = 0 → ¬↑Q x✝ = 0
Tactic:
apply h'
State after:
no goals

State before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
⊢ ∃ w, ↑Q w ≠ 0
Tactic:
rw [ne_eq, ext_iff,not_forall] at h₁
State after:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : ∃ x, ¬↑Q x = ↑0 x
h₂ : Module.rank k W = 1
⊢ ∃ w, ↑Q w ≠ 0

State before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : ∃ x, ¬↑Q x = ↑0 x
h₂ : Module.rank k W = 1
⊢ ∃ w, ↑Q w ≠ 0
Tactic:
convert h₁
State after:
no goals

State before:
V : Type ?u.84490
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.85032
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q ≠ 0
h₂ : Module.rank k W = 1
w : W
hw : ↑Q w ≠ 0
⊢ ∀ (v : W), v ≠ 0 → ↑Q v ≠ 0
Tactic:
sorry
State after:
no goals