-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem span_singleton_inf_orthogonal_eq_bot {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :
    (K ∙ x) ⊓ B.orthogonal (K ∙ x) = ⊥

Proof state:
case intro.refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
⊢ ∀ (p : Submodule K V), ↑{x} ⊆ ↑p → x ∈ p

Tactic:
exact fun _ hp => hp <| Finset.mem_singleton_self _

Result:
no goals

Proof state:
case intro.refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
⊢ x ∈ Submodule.span K ↑{x}

Tactic:
rw [Submodule.mem_span]

Result:
case intro.refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
⊢ ∀ (p : Submodule K V), ↑{x} ⊆ ↑p → x ∈ p

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
⊢ Submodule.span K {x} ⊓ B.orthogonal (Submodule.span K {x}) = ⊥

Tactic:
rw [← Finset.coe_singleton]

Result:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
⊢ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x}) = ⊥

Proof state:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : μ x * (B x) x = 0
⊢ μ x = 0

Tactic:
exact eq_zero_of_ne_zero_of_mul_right_eq_zero hx this

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
y : V
h : y ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
⊢ y ∈ ⊥

Tactic:
rcases mem_span_finset.1 h.1 with ⟨μ, rfl⟩

Result:
case intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
⊢ ∑ i ∈ {x}, μ i • i ∈ ⊥

Proof state:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : B.IsOrtho x (μ x • x)
⊢ μ x = 0

Tactic:
change B x (μ x • x) = 0 at this

Result:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : (B x) (μ x • x) = 0
⊢ μ x = 0

Proof state:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : B.IsOrtho x (∑ i ∈ {x}, μ i • i)
⊢ ∑ i ∈ {x}, μ i • i ∈ ⊥

Tactic:
rw [Finset.sum_singleton] at this ⊢

Result:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : B.IsOrtho x (μ x • x)
⊢ μ x • x ∈ ⊥

Proof state:
case intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
⊢ ∑ i ∈ {x}, μ i • i ∈ ⊥

Tactic:
have := h.2 x ?_

Result:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : B.IsOrtho x (∑ i ∈ {x}, μ i • i)
⊢ ∑ i ∈ {x}, μ i • i ∈ ⊥

case intro.refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
⊢ x ∈ Submodule.span K ↑{x}

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
⊢ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x}) = ⊥

Tactic:
refine eq_bot_iff.2 fun y h => ?_

Result:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
y : V
h : y ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
⊢ y ∈ ⊥

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : B.IsOrtho x (μ x • x)
hμzero : μ x = 0
⊢ μ x • x ∈ ⊥

Tactic:
rw [hμzero, zero_smul, Submodule.mem_bot]

Result:
no goals

Proof state:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : (B x) (μ x • x) = 0
⊢ μ x = 0

Tactic:
rw [smul_right] at this

Result:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : μ x * (B x) x = 0
⊢ μ x = 0

Proof state:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : B.IsOrtho x (μ x • x)
⊢ μ x • x ∈ ⊥

Tactic:
suffices hμzero : μ x = 0 by rw [hμzero, zero_smul, Submodule.mem_bot]

Result:
case intro.refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx : ¬B.IsOrtho x x
μ : V → K
h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K ↑{x} ⊓ B.orthogonal (Submodule.span K ↑{x})
this : B.IsOrtho x (μ x • x)
⊢ μ x = 0