-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem toLin_restrict_ker_eq_inf_orthogonal (B : BilinForm K V) (W : Subspace K V) (b : B.IsRefl) :
    (B.domRestrict W).ker.map W.subtype = (W ⊓ B.orthogonal ⊤ : Subspace K V)

Proof state:
case h.mp.intro.mk.intro.right.a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
y : V
a✝ : y ∈ ⊤
⊢ 0 y = 0

Tactic:
rfl

Result:
no goals

Proof state:
case h.mp.intro.mk.intro.right
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ ↑(B.orthogonal ⊤)

Tactic:
intro y _

Result:
case h.mp.intro.mk.intro.right
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
y : V
a✝ : y ∈ ⊤
⊢ B.IsOrtho y ((Submodule.subtype W) ⟨x, hx⟩)

Proof state:
case h.mpr.h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
y : V
⊢ (B x) y = 0

Tactic:
rw [b]

Result:
case h.mpr.h.a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
y : V
⊢ (B y) x = 0

Proof state:
case h.mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
⊢ ∃ y, (domRestrict B W) y = 0 ∧ (Submodule.subtype W) y = x

Tactic:
refine ⟨⟨x, hx.1⟩, ?_, rfl⟩

Result:
case h.mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
⊢ (domRestrict B W) ⟨x, ⋯⟩ = 0

Proof state:
case h.mp.intro.mk.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ W ⊓ B.orthogonal ⊤

Tactic:
constructor

Result:
case h.mp.intro.mk.intro.left
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ ↑W

case h.mp.intro.mk.intro.right
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ ↑(B.orthogonal ⊤)

Proof state:
case h.mpr.h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
y : V
⊢ ((domRestrict B W) ⟨x, ⋯⟩) y = 0 y

Tactic:
change B x y = 0

Result:
case h.mpr.h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
y : V
⊢ (B x) y = 0

Proof state:
case h.mpr.h.a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
y : V
⊢ (B y) x = 0

Tactic:
exact hx.2 _ Submodule.mem_top

Result:
no goals

Proof state:
case h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
⊢ x ∈ Submodule.map (Submodule.subtype W) (ker (domRestrict B W)) ↔ x ∈ W ⊓ B.orthogonal ⊤

Tactic:
constructor <;> intro hx

Result:
case h.mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ Submodule.map (Submodule.subtype W) (ker (domRestrict B W))
⊢ x ∈ W ⊓ B.orthogonal ⊤

case h.mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
⊢ x ∈ Submodule.map (Submodule.subtype W) (ker (domRestrict B W))

Proof state:
case h.mp.intro.mk.intro.right.a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
y : V
a✝ : y ∈ ⊤
⊢ (B ((Submodule.subtype W) ⟨x, hx⟩)) y = 0

Tactic:
change (B.domRestrict W) ⟨x, hx⟩ y = 0

Result:
case h.mp.intro.mk.intro.right.a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
y : V
a✝ : y ∈ ⊤
⊢ ((domRestrict B W) ⟨x, hx⟩) y = 0

Proof state:
case h.mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
⊢ x ∈ Submodule.map (Submodule.subtype W) (ker (domRestrict B W))

Tactic:
simp_rw [Submodule.mem_map, LinearMap.mem_ker]

Result:
case h.mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
⊢ ∃ y, (domRestrict B W) y = 0 ∧ (Submodule.subtype W) y = x

Proof state:
case h.mp.intro.mk.intro.right.a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
y : V
a✝ : y ∈ ⊤
⊢ ((domRestrict B W) ⟨x, hx⟩) y = 0

Tactic:
rw [hker]

Result:
case h.mp.intro.mk.intro.right.a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
y : V
a✝ : y ∈ ⊤
⊢ 0 y = 0

Proof state:
case h.mp.intro.mk.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : ⟨x, hx⟩ ∈ ↑(ker (domRestrict B W))
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ W ⊓ B.orthogonal ⊤

Tactic:
erw [LinearMap.mem_ker] at hker

Result:
case h.mp.intro.mk.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ W ⊓ B.orthogonal ⊤

Proof state:
case h.mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
⊢ (domRestrict B W) ⟨x, ⋯⟩ = 0

Tactic:
ext y

Result:
case h.mpr.h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W ⊓ B.orthogonal ⊤
y : V
⊢ ((domRestrict B W) ⟨x, ⋯⟩) y = 0 y

Proof state:
case h.mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ Submodule.map (Submodule.subtype W) (ker (domRestrict B W))
⊢ x ∈ W ⊓ B.orthogonal ⊤

Tactic:
rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩

Result:
case h.mp.intro.mk.intro
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : ⟨x, hx⟩ ∈ ↑(ker (domRestrict B W))
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ W ⊓ B.orthogonal ⊤