case h
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
⊢ x ∈ Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict (↑toLin B) W)) ↔ x ∈ W ⊓ orthogonal B ⊤
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
⊢ Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict (↑toLin B) W)) = W ⊓ orthogonal B ⊤
ext x
case h.mp
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict (↑toLin B) W))
⊢ x ∈ W ⊓ orthogonal B ⊤

case h.mpr
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
⊢ x ∈ Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict (↑toLin B) W))
case h
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
⊢ x ∈ Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict (↑toLin B) W)) ↔ x ∈ W ⊓ orthogonal B ⊤
constructor <;> intro hx
case h.mp.intro.mk.intro
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : { val := x, property := hx } ∈ ↑(LinearMap.ker (LinearMap.domRestrict (↑toLin B) W))
⊢ ↑(Submodule.subtype W) { val := x, property := hx } ∈ W ⊓ orthogonal B ⊤
case h.mp
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict (↑toLin B) W))
⊢ x ∈ W ⊓ orthogonal B ⊤
rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩
case h.mp.intro.mk.intro
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
⊢ ↑(Submodule.subtype W) { val := x, property := hx } ∈ W ⊓ orthogonal B ⊤
case h.mp.intro.mk.intro
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : { val := x, property := hx } ∈ ↑(LinearMap.ker (LinearMap.domRestrict (↑toLin B) W))
⊢ ↑(Submodule.subtype W) { val := x, property := hx } ∈ W ⊓ orthogonal B ⊤
erw [LinearMap.mem_ker] at hker
case h.mp.intro.mk.intro.left
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
⊢ ↑(Submodule.subtype W) { val := x, property := hx } ∈ ↑W

case h.mp.intro.mk.intro.right
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
⊢ ↑(Submodule.subtype W) { val := x, property := hx } ∈ ↑(orthogonal B ⊤)
case h.mp.intro.mk.intro
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
⊢ ↑(Submodule.subtype W) { val := x, property := hx } ∈ W ⊓ orthogonal B ⊤
constructor
no goals
case h.mp.intro.mk.intro.left
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
⊢ ↑(Submodule.subtype W) { val := x, property := hx } ∈ ↑W
simp [hx]
case h.mp.intro.mk.intro.right
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
y : V
a✝ : y ∈ ⊤
⊢ IsOrtho B y (↑(Submodule.subtype W) { val := x, property := hx })
case h.mp.intro.mk.intro.right
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
⊢ ↑(Submodule.subtype W) { val := x, property := hx } ∈ ↑(orthogonal B ⊤)
intro y _
case h.mp.intro.mk.intro.right.a
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
y : V
a✝ : y ∈ ⊤
⊢ bilin B (↑(Submodule.subtype W) { val := x, property := hx }) y = 0
case h.mp.intro.mk.intro.right
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
y : V
a✝ : y ∈ ⊤
⊢ IsOrtho B y (↑(Submodule.subtype W) { val := x, property := hx })
rw [IsOrtho, b]
case h.mp.intro.mk.intro.right.a
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
y : V
a✝ : y ∈ ⊤
⊢ ↑(↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx }) y = 0
case h.mp.intro.mk.intro.right.a
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
y : V
a✝ : y ∈ ⊤
⊢ bilin B (↑(Submodule.subtype W) { val := x, property := hx }) y = 0
change (B.toLin.domRestrict W) ⟨x, hx⟩ y = 0
case h.mp.intro.mk.intro.right.a
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
y : V
a✝ : y ∈ ⊤
⊢ ↑0 y = 0
case h.mp.intro.mk.intro.right.a
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
y : V
a✝ : y ∈ ⊤
⊢ ↑(↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx }) y = 0
rw [hker]
no goals
case h.mp.intro.mk.intro.right.a
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W
hker : ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := hx } = 0
y : V
a✝ : y ∈ ⊤
⊢ ↑0 y = 0
rfl
case h.mpr
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
⊢ ∃ y, ↑(LinearMap.domRestrict (↑toLin B) W) y = 0 ∧ ↑(Submodule.subtype W) y = x
case h.mpr
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
⊢ x ∈ Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict (↑toLin B) W))
simp_rw [Submodule.mem_map, LinearMap.mem_ker]
case h.mpr
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
⊢ ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := (_ : x ∈ ↑W) } = 0
case h.mpr
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
⊢ ∃ y, ↑(LinearMap.domRestrict (↑toLin B) W) y = 0 ∧ ↑(Submodule.subtype W) y = x
refine' ⟨⟨x, hx.1⟩, _, rfl⟩
case h.mpr.h
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
y : V
⊢ ↑(↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := (_ : x ∈ ↑W) }) y = ↑0 y
case h.mpr
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
⊢ ↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := (_ : x ∈ ↑W) } = 0
ext y
case h.mpr.h
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
y : V
⊢ bilin B x y = 0
case h.mpr.h
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
y : V
⊢ ↑(↑(LinearMap.domRestrict (↑toLin B) W) { val := x, property := (_ : x ∈ ↑W) }) y = ↑0 y
change B x y = 0
case h.mpr.h.a
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
y : V
⊢ bilin B y x = 0
case h.mpr.h
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
y : V
⊢ bilin B x y = 0
rw [b]
no goals
case h.mpr.h.a
R : Type ?u.1511059
M : Type ?u.1511062
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1511098
M₁ : Type ?u.1511101
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1511710
M₂ : Type ?u.1511713
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1511900
M₃ : Type ?u.1511903
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₂
M₂' : Type ?u.1513708
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm K V
W : Subspace K V
b : IsRefl B
x : V
hx : x ∈ W ⊓ orthogonal B ⊤
y : V
⊢ bilin B y x = 0
exact hx.2 _ Submodule.mem_top