case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : { x // x ∈ W }), bilin (restrict B W) { val := x, property := hx } n = 0
⊢ { val := x, property := hx } = 0
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
⊢ Nondegenerate (restrict B W)
rintro ⟨x, hx⟩ b₁
case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : { x // x ∈ W }), bilin (restrict B W) { val := x, property := hx } n = 0
⊢ x ∈ ⊥
case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : { x // x ∈ W }), bilin (restrict B W) { val := x, property := hx } n = 0
⊢ { val := x, property := hx } = 0
rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R₁]
case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : { x // x ∈ W }), bilin (restrict B W) { val := x, property := hx } n = 0
y : M₁
hy : y ∈ W
⊢ IsOrtho B y x
case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : { x // x ∈ W }), bilin (restrict B W) { val := x, property := hx } n = 0
⊢ x ∈ ⊥
refine' hW.le_bot ⟨hx, fun y hy => _⟩
case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
y : M₁
hy : y ∈ W
b₁ : bilin (restrict B W) { val := x, property := hx } { val := y, property := hy } = 0
⊢ IsOrtho B y x
case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : { x // x ∈ W }), bilin (restrict B W) { val := x, property := hx } n = 0
y : M₁
hy : y ∈ W
⊢ IsOrtho B y x
specialize b₁ ⟨y, hy⟩
case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
y : M₁
hy : y ∈ W
b₁ : bilin B x y = 0
⊢ IsOrtho B y x
case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
y : M₁
hy : y ∈ W
b₁ : bilin (restrict B W) { val := x, property := hx } { val := y, property := hy } = 0
⊢ IsOrtho B y x
rw [restrict_apply, Submodule.coe_mk, Submodule.coe_mk] at b₁
no goals
case mk
R : Type ?u.1488672
M : Type ?u.1488675
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1489323
M₂ : Type ?u.1489326
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type ?u.1489513
M₃ : Type ?u.1489516
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1490104
K : Type ?u.1490107
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.1491321
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₁ M₁
b : IsRefl B
W : Submodule R₁ M₁
hW : Disjoint W (orthogonal B W)
x : M₁
hx : x ∈ W
y : M₁
hy : y ∈ W
b₁ : bilin B x y = 0
⊢ IsOrtho B y x
exact isOrtho_def.mpr (b x y b₁)