R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
⊢ SeparatingLeft (domRestrict₁₂ B W W)
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
⊢ Nondegenerate (domRestrict₁₂ B W W)
refine' (hB.domRestrict W).nondegenerate_of_separatingLeft _
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
b₁ : ∀ (y : { x // x ∈ W }), ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) y = 0
⊢ { val := x, property := hx } = 0
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
⊢ SeparatingLeft (domRestrict₁₂ B W W)
rintro ⟨x, hx⟩ b₁
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
b₁ : ∀ (y : { x // x ∈ W }), ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) y = 0
⊢ x ∈ ⊥
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
b₁ : ∀ (y : { x // x ∈ W }), ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) y = 0
⊢ { val := x, property := hx } = 0
rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R]
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
b₁ : ∀ (y : { x // x ∈ W }), ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) y = 0
y : M
hy : y ∈ W
⊢ IsOrtho B y x
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
b₁ : ∀ (y : { x // x ∈ W }), ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) y = 0
⊢ x ∈ ⊥
refine' hW.le_bot ⟨hx, fun y hy ↦ _⟩
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) { val := y, property := hy } = 0
⊢ IsOrtho B y x
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
b₁ : ∀ (y : { x // x ∈ W }), ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) y = 0
y : M
hy : y ∈ W
⊢ IsOrtho B y x
specialize b₁ ⟨y, hy⟩
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ↑(↑B x) y = 0
⊢ IsOrtho B y x
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ↑(↑(domRestrict₁₂ B W W) { val := x, property := hx }) { val := y, property := hy } = 0
⊢ IsOrtho B y x
simp_rw [domRestrict₁₂_apply] at b₁
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ↑(↑B x) y = 0
⊢ IsOrtho B x y
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ↑(↑B x) y = 0
⊢ IsOrtho B y x
rw [hB.ortho_comm]
no goals
case mk
R : Type u_1
R₁ : Type ?u.581487
R₂ : Type ?u.581490
R₃ : Type ?u.581493
M : Type u_2
M₁ : Type ?u.581499
M₂ : Type ?u.581502
Mₗ₁ : Type ?u.581505
Mₗ₁' : Type ?u.581508
Mₗ₂ : Type ?u.581511
Mₗ₂' : Type ?u.581514
K : Type ?u.581517
K₁ : Type ?u.581520
K₂ : Type ?u.581523
V : Type ?u.581526
V₁ : Type ?u.581529
V₂ : Type ?u.581532
n : Type ?u.581535
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin W B)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ↑(↑B x) y = 0
⊢ IsOrtho B x y
exact b₁