case intro
S : Type ?u.666424
R : Type u_1
R₁ : Type ?u.666430
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticForm R M
hB₁✝ hB₁ : ↑(QuadraticForm.associatedHom ℕ) Q ≠ 0
⊢ ∃ x, ¬IsOrtho (↑(QuadraticForm.associatedHom ℕ) Q) x x
S : Type ?u.666424
R : Type u_1
R₁ : Type ?u.666430
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
hB₁ : B ≠ 0
hB₂ : IsSymm B
⊢ ∃ x, ¬IsOrtho B x x
lift B to QuadraticForm R M using hB₂ with Q
case intro.intro
S : Type ?u.666424
R : Type u_1
R₁ : Type ?u.666430
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticForm R M
hB₁✝ hB₁ : ↑(QuadraticForm.associatedHom ℕ) Q ≠ 0
x : M
hx : ↑Q x ≠ 0
⊢ ∃ x, ¬IsOrtho (↑(QuadraticForm.associatedHom ℕ) Q) x x
case intro
S : Type ?u.666424
R : Type u_1
R₁ : Type ?u.666430
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticForm R M
hB₁✝ hB₁ : ↑(QuadraticForm.associatedHom ℕ) Q ≠ 0
⊢ ∃ x, ¬IsOrtho (↑(QuadraticForm.associatedHom ℕ) Q) x x
obtain ⟨x, hx⟩ := QuadraticForm.exists_quadraticForm_ne_zero hB₁
no goals
case intro.intro
S : Type ?u.666424
R : Type u_1
R₁ : Type ?u.666430
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
Q : QuadraticForm R M
hB₁✝ hB₁ : ↑(QuadraticForm.associatedHom ℕ) Q ≠ 0
x : M
hx : ↑Q x ≠ 0
⊢ ∃ x, ¬IsOrtho (↑(QuadraticForm.associatedHom ℕ) Q) x x
exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩