-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem restrict_nondegenerate_orthogonal_spanSingleton (B : BilinForm K V) (b₁ : B.Nondegenerate)
    (b₂ : B.IsRefl) {x : V} (hx : ¬B.IsOrtho x x) :
    Nondegenerate <| B.restrict <| B.orthogonal (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
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
y : V
hy : y ∈ Submodule.span K {x}
z : V
hz : z ∈ B.orthogonal (Submodule.span K {x})
this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
hm : ((domRestrict₁₂ B (B.orthogonal (Submodule.span K {x})) (B.orthogonal (Submodule.span K {x}))) m) ⟨z, hz⟩ = 0
⊢ (B ↑m) y = 0

Tactic:
rw [b₂]

Result:
case a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
y : V
hy : y ∈ Submodule.span K {x}
z : V
hz : z ∈ B.orthogonal (Submodule.span K {x})
this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
hm : ((domRestrict₁₂ B (B.orthogonal (Submodule.span K {x})) (B.orthogonal (Submodule.span K {x}))) m) ⟨z, hz⟩ = 0
⊢ (B y) ↑m = 0

Proof state:
case intro.intro.intro.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
y : V
hy : y ∈ Submodule.span K {x}
z : V
hz : z ∈ B.orthogonal (Submodule.span K {x})
this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
hm : ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) ⟨z, hz⟩ = 0
⊢ (B ↑m) (y + z) = 0

Tactic:
rw [restrict] at hm

Result:
case intro.intro.intro.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
y : V
hy : y ∈ Submodule.span K {x}
z : V
hz : z ∈ B.orthogonal (Submodule.span K {x})
this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
hm : ((domRestrict₁₂ B (B.orthogonal (Submodule.span K {x})) (B.orthogonal (Submodule.span K {x}))) m) ⟨z, hz⟩ = 0
⊢ (B ↑m) (y + z) = 0

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
hm : ∀ (n : ↥(B.orthogonal (Submodule.span K {x}))), ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) n = 0
n : V
this : n ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
⊢ (B ↑m) n = 0

Tactic:
rcases Submodule.mem_sup.1 this with ⟨y, hy, z, hz, rfl⟩

Result:
case intro.intro.intro.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
hm : ∀ (n : ↥(B.orthogonal (Submodule.span K {x}))), ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) n = 0
y : V
hy : y ∈ Submodule.span K {x}
z : V
hz : z ∈ B.orthogonal (Submodule.span K {x})
this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
⊢ (B ↑m) (y + z) = 0

Proof state:
case intro.intro.intro.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
y : V
hy : y ∈ Submodule.span K {x}
z : V
hz : z ∈ B.orthogonal (Submodule.span K {x})
this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
hm : ((domRestrict₁₂ B (B.orthogonal (Submodule.span K {x})) (B.orthogonal (Submodule.span K {x}))) m) ⟨z, hz⟩ = 0
⊢ (B ↑m) (y + z) = 0

Tactic:
erw [add_right, show B m.1 y = 0 by rw [b₂]; exact m.2 y hy, hm, add_zero]

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
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
⊢ (B.restrict (B.orthogonal (Submodule.span K {x}))).Nondegenerate

Tactic:
refine fun m hm => Submodule.coe_eq_zero.1 (b₁ m.1 fun n => ?_)

Result:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
hm : ∀ (n : ↥(B.orthogonal (Submodule.span K {x}))), ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) n = 0
n : V
⊢ (B ↑m) n = 0

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
hm : ∀ (n : ↥(B.orthogonal (Submodule.span K {x}))), ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) n = 0
n : V
⊢ (B ↑m) n = 0

Tactic:
have : n ∈ (K ∙ x) ⊔ B.orthogonal (K ∙ x) :=
  (span_singleton_sup_orthogonal_eq_top hx).symm ▸ Submodule.mem_top

Result:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
hm : ∀ (n : ↥(B.orthogonal (Submodule.span K {x}))), ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) n = 0
n : V
this : n ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
⊢ (B ↑m) n = 0

Proof state:
case a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
y : V
hy : y ∈ Submodule.span K {x}
z : V
hz : z ∈ B.orthogonal (Submodule.span K {x})
this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
hm : ((domRestrict₁₂ B (B.orthogonal (Submodule.span K {x})) (B.orthogonal (Submodule.span K {x}))) m) ⟨z, hz⟩ = 0
⊢ (B y) ↑m = 0

Tactic:
exact m.2 y hy

Result:
no goals

Proof state:
case intro.intro.intro.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
hm : ∀ (n : ↥(B.orthogonal (Submodule.span K {x}))), ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) n = 0
y : V
hy : y ∈ Submodule.span K {x}
z : V
hz : z ∈ B.orthogonal (Submodule.span K {x})
this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
⊢ (B ↑m) (y + z) = 0

Tactic:
specialize hm ⟨z, hz⟩

Result:
case intro.intro.intro.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
m : ↥(B.orthogonal (Submodule.span K {x}))
y : V
hy : y ∈ Submodule.span K {x}
z : V
hz : z ∈ B.orthogonal (Submodule.span K {x})
this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})
hm : ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) ⟨z, hz⟩ = 0
⊢ (B ↑m) (y + z) = 0