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

State before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
⊢ Isotropic Q
Tactic:
rw [QuadraticForm.Isotropic, QuadraticForm.Anisotropic]
State after:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0

State before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have h : ∃ (w : W), w ≠ 0 := by
  simpa only [ne_eq, rank_zero_iff_forall_zero, not_forall] using h₂
State after:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
h : ∃ w, w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0

State before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
h : ∃ w, w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
obtain ⟨w, hw⟩ := h
State after:
case intro
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
w : W
hw : w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0

State before:
case intro
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
w : W
hw : w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have : Q w = 0 := by 
  rw [h₁]
  simp only [zero_apply]
State after:
case intro
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
w : W
hw : w ≠ 0
this : ↑Q w = 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0

State before:
case intro
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
w : W
hw : w ≠ 0
this : ↑Q w = 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
tauto
State after:
no goals

State before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
⊢ ∃ w, w ≠ 0
Tactic:
simpa only [ne_eq, rank_zero_iff_forall_zero, not_forall] using h₂
State after:
no goals

State before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
w : W
hw : w ≠ 0
⊢ ↑Q w = 0
Tactic:
rw [h₁]
State after:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
w : W
hw : w ≠ 0
⊢ ↑0 w = 0

State before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
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 ≠ 0
w : W
hw : w ≠ 0
⊢ ↑0 w = 0
Tactic:
simp only [zero_apply]
State after:
no goals