-- Mathlib/LinearAlgebra/SesquilinearForm.lean
lemma nondegenerate_restrict_iff_disjoint_ker (hs : ∀ x, 0 ≤ B x x) (hB : B.IsSymm)
    {W : Submodule R M} :
    (B.domRestrict₁₂ W W).Nondegenerate ↔ Disjoint W (LinearMap.ker B)

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
⊢ (domRestrict₁₂ B W W).SeparatingLeft

Tactic:
intro ⟨x, hx⟩ h

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : ∀ (y : ↥W), ((domRestrict₁₂ B W W) ⟨x, hx⟩) y = 0
⊢ ⟨x, hx⟩ = 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : ∀ a ∈ W, (B x) a = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
specialize h x hx

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : (B x) x = 0
⊢ ⟨x, hx⟩ = 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : x ∈ ker B
key : x ∈ W ⊓ ker B
⊢ ⟨x, hx⟩ = 0

Tactic:
simpa [hW.eq_bot] using key

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : x ∈ ker B
⊢ ⟨x, hx⟩ = 0

Tactic:
have key : x ∈ W ⊓ LinearMap.ker B := ⟨hx, h⟩

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : x ∈ ker B
key : x ∈ W ⊓ ker B
⊢ ⟨x, hx⟩ = 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
⊢ (domRestrict₁₂ B W W).Nondegenerate

Tactic:
have hB' : (B.domRestrict₁₂ W W).IsRefl := fun x y ↦ hB.isRefl (W.subtype x) (W.subtype y)

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
⊢ (domRestrict₁₂ B W W).Nondegenerate

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : (B x) x = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
rw [B.apply_apply_same_eq_zero_iff hs hB] at h

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : x ∈ ker B
⊢ ⟨x, hx⟩ = 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
⊢ (domRestrict₁₂ B W W).Nondegenerate

Tactic:
rw [IsRefl.nondegenerate_iff_separatingLeft hB']

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
⊢ (domRestrict₁₂ B W W).SeparatingLeft

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
⊢ (domRestrict₁₂ B W W).Nondegenerate ↔ Disjoint W (ker B)

Tactic:
refine ⟨disjoint_ker_of_nondegenerate_restrict, fun hW ↦ ?_⟩

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
⊢ (domRestrict₁₂ B W W).Nondegenerate

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : ∀ (y : ↥W), ((domRestrict₁₂ B W W) ⟨x, hx⟩) y = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
simp_rw [Subtype.forall, domRestrict₁₂_apply] at h

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : ∀ a ∈ W, (B x) a = 0
⊢ ⟨x, hx⟩ = 0