R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x}) = ⊥
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K {x} ⊓ orthogonal B (Submodule.span K {x}) = ⊥
rw [← Finset.coe_singleton]
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
y : V
h : y ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
⊢ y ∈ ⊥
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x}) = ⊥
refine' eq_bot_iff.2 fun y h => _
case intro
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
⊢ ∑ i in {x}, μ i • i ∈ ⊥
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
y : V
h : y ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
⊢ y ∈ ⊥
rcases mem_span_finset.1 h.1 with ⟨μ, rfl⟩
case intro.refine_2
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : IsOrtho B x (∑ i in {x}, μ i • i)
⊢ ∑ i in {x}, μ i • i ∈ ⊥

case intro.refine_1
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
⊢ x ∈ Submodule.span K ↑{x}
case intro
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
⊢ ∑ i in {x}, μ i • i ∈ ⊥
have := h.2 x ?_
case intro.refine_2
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : IsOrtho B x (μ x • x)
⊢ μ x • x ∈ ⊥
case intro.refine_2
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : IsOrtho B x (∑ i in {x}, μ i • i)
⊢ ∑ i in {x}, μ i • i ∈ ⊥
rw [Finset.sum_singleton] at this⊢
case intro.refine_2
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : IsOrtho B x (μ x • x)
hμzero : μ x = 0
⊢ μ x • x ∈ ⊥

case hμzero
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : IsOrtho B x (μ x • x)
⊢ μ x = 0
case intro.refine_2
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : IsOrtho B x (μ x • x)
⊢ μ x • x ∈ ⊥
suffices hμzero : μ x = 0
case hμzero
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : bilin B x (μ x • x) = 0
⊢ μ x = 0
case hμzero
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : IsOrtho B x (μ x • x)
⊢ μ x = 0
change B x (μ x • x) = 0 at this
case hμzero
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : μ x * bilin B x x = 0
⊢ μ x = 0
case hμzero
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : bilin B x (μ x • x) = 0
⊢ μ x = 0
rw [smul_right] at this
no goals
case hμzero
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : μ x * bilin B x x = 0
⊢ μ x = 0
exact eq_zero_of_ne_zero_of_mul_right_eq_zero hx this
no goals
case intro.refine_2
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
this : IsOrtho B x (μ x • x)
hμzero : μ x = 0
⊢ μ x • x ∈ ⊥
rw [hμzero, zero_smul, Submodule.mem_bot]
case intro.refine_1
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
⊢ ∀ (p : Submodule K V), ↑{x} ⊆ ↑p → x ∈ p
case intro.refine_1
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
⊢ x ∈ Submodule.span K ↑{x}
rw [Submodule.mem_span]
no goals
case intro.refine_1
R : Type ?u.1282529
M : Type ?u.1282532
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1282568
M₁ : Type ?u.1282571
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1283180
M₂ : Type ?u.1283183
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1283370
M₃ : Type ?u.1283373
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
μ : V → K
h : ∑ i in {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ orthogonal B (Submodule.span K ↑{x})
⊢ ∀ (p : Submodule K V), ↑{x} ⊆ ↑p → x ∈ p
exact fun _ hp => hp <| Finset.mem_singleton_self _