-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem toLin_restrict_range_dualCoannihilator_eq_orthogonal (B : BilinForm K V)
    (W : Subspace K V) : (B.domRestrict W).range.dualCoannihilator = B.orthogonal W

Proof state:
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
⊢ (range (domRestrict B W)).dualCoannihilator = B.orthogonal W

Tactic:
ext x

Result:
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
x : V
⊢ x ∈ (range (domRestrict B W)).dualCoannihilator ↔ x ∈ B.orthogonal W

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
x : V
hx : ∀ φ ∈ range (domRestrict B W), φ x = 0
y : V
hy : y ∈ W
⊢ B.IsOrtho y x

Tactic:
exact hx (B.domRestrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩

Result:
no goals

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
x : V
hx : x ∈ (range (domRestrict B W)).dualCoannihilator
y : V
hy : y ∈ W
⊢ B.IsOrtho y x

Tactic:
rw [Submodule.mem_dualCoannihilator] at 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
x : V
hx : ∀ φ ∈ range (domRestrict B W), φ x = 0
y : V
hy : y ∈ W
⊢ B.IsOrtho y x

Proof state:
case h.mpr.intro.mk
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
x : V
hx : ∀ n ∈ W, B.IsOrtho n x
w : V
hw : w ∈ W
⊢ ((domRestrict B W) ⟨w, hw⟩) x = 0

Tactic:
exact hx w hw

Result:
no goals

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
x : V
hx : ∀ n ∈ W, B.IsOrtho n x
⊢ ∀ φ ∈ range (domRestrict B W), φ x = 0

Tactic:
rintro _ ⟨⟨w, hw⟩, rfl⟩

Result:
case h.mpr.intro.mk
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
x : V
hx : ∀ n ∈ W, B.IsOrtho n x
w : V
hw : w ∈ W
⊢ ((domRestrict B W) ⟨w, hw⟩) 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
x : V
hx : ∀ n ∈ W, B.IsOrtho n x
⊢ x ∈ (range (domRestrict B W)).dualCoannihilator

Tactic:
rw [Submodule.mem_dualCoannihilator]

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
x : V
hx : ∀ n ∈ W, B.IsOrtho n x
⊢ ∀ φ ∈ range (domRestrict B W), φ x = 0

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
x : V
⊢ x ∈ (range (domRestrict B W)).dualCoannihilator ↔ x ∈ B.orthogonal W

Tactic:
constructor <;> rw [mem_orthogonal_iff] <;> 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
x : V
hx : x ∈ (range (domRestrict B W)).dualCoannihilator
⊢ ∀ n ∈ W, B.IsOrtho n x

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
x : V
hx : ∀ n ∈ W, B.IsOrtho n x
⊢ x ∈ (range (domRestrict B W)).dualCoannihilator

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
x : V
hx : x ∈ (range (domRestrict B W)).dualCoannihilator
⊢ ∀ n ∈ W, B.IsOrtho n x

Tactic:
intro y hy

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
x : V
hx : x ∈ (range (domRestrict B W)).dualCoannihilator
y : V
hy : y ∈ W
⊢ B.IsOrtho y x