-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem nondegenerate_restrict_of_disjoint_orthogonal (B : BilinForm R₁ M₁) (b : B.IsRefl)
    {W : Submodule R₁ M₁} (hW : Disjoint W (B.orthogonal W)) : (B.restrict W).Nondegenerate

Proof state:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
y : M₁
hy : y ∈ W
b₁ : (B x) y = 0
⊢ B.IsOrtho y x

Tactic:
exact isOrtho_def.mpr (b x y b₁)

Result:
no goals

Proof state:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : ↥W), ((B.restrict W) ⟨x, hx⟩) n = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R₁]

Result:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : ↥W), ((B.restrict W) ⟨x, hx⟩) n = 0
⊢ x ∈ ⊥

Proof state:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : ↥W), ((B.restrict W) ⟨x, hx⟩) n = 0
⊢ x ∈ ⊥

Tactic:
refine hW.le_bot ⟨hx, fun y hy => ?_⟩

Result:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : ↥W), ((B.restrict W) ⟨x, hx⟩) n = 0
y : M₁
hy : y ∈ W
⊢ B.IsOrtho y x

Proof state:
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
⊢ (B.restrict W).Nondegenerate

Tactic:
rintro ⟨x, hx⟩ b₁

Result:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : ↥W), ((B.restrict W) ⟨x, hx⟩) n = 0
⊢ ⟨x, hx⟩ = 0

Proof state:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
y : M₁
hy : y ∈ W
b₁ : ((B.restrict W) ⟨x, hx⟩) ⟨y, hy⟩ = 0
⊢ B.IsOrtho y x

Tactic:
simp only [restrict_apply, domRestrict_apply] at b₁

Result:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
y : M₁
hy : y ∈ W
b₁ : (B x) y = 0
⊢ B.IsOrtho y x

Proof state:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
b₁ : ∀ (n : ↥W), ((B.restrict W) ⟨x, hx⟩) n = 0
y : M₁
hy : y ∈ W
⊢ B.IsOrtho y x

Tactic:
specialize b₁ ⟨y, hy⟩

Result:
case mk
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
x : M₁
hx : x ∈ W
y : M₁
hy : y ∈ W
b₁ : ((B.restrict W) ⟨x, hx⟩) ⟨y, hy⟩ = 0
⊢ B.IsOrtho y x