-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem nondegenerate_iff_ker_eq_bot {B : BilinForm R M} :
    B.Nondegenerate ↔ LinearMap.ker B = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
⊢ B.Nondegenerate ↔ ker B = ⊥

Tactic:
rw [LinearMap.ker_eq_bot']

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
⊢ B.Nondegenerate ↔ ∀ (m : M), B m = 0 → m = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
⊢ B.Nondegenerate ↔ ∀ (m : M), B m = 0 → m = 0

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : B.Nondegenerate
⊢ ∀ (m : M), B m = 0 → m = 0

case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : ∀ (m : M), B m = 0 → m = 0
⊢ B.Nondegenerate

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : B.Nondegenerate
m : M
hm : B m = 0
x : M
⊢ (B m) x = 0

Tactic:
rw [hm]

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : B.Nondegenerate
m : M
hm : B m = 0
x : M
⊢ 0 x = 0

Proof state:
case mpr.a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : ∀ (m : M), B m = 0 → m = 0
m : M
hm : ∀ (n : M), (B m) n = 0
⊢ B m = 0

Tactic:
ext x

Result:
case mpr.a.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : ∀ (m : M), B m = 0 → m = 0
m : M
hm : ∀ (n : M), (B m) n = 0
x : M
⊢ (B m) x = 0 x

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : B.Nondegenerate
m : M
hm : B m = 0
x : M
⊢ 0 x = 0

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : ∀ (m : M), B m = 0 → m = 0
⊢ B.Nondegenerate

Tactic:
intro m hm

Result:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : ∀ (m : M), B m = 0 → m = 0
m : M
hm : ∀ (n : M), (B m) n = 0
⊢ m = 0

Proof state:
case mpr.a.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : ∀ (m : M), B m = 0 → m = 0
m : M
hm : ∀ (n : M), (B m) n = 0
x : M
⊢ (B m) x = 0 x

Tactic:
exact hm x

Result:
no goals

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : ∀ (m : M), B m = 0 → m = 0
m : M
hm : ∀ (n : M), (B m) n = 0
⊢ m = 0

Tactic:
apply h

Result:
case mpr.a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : ∀ (m : M), B m = 0 → m = 0
m : M
hm : ∀ (n : M), (B m) n = 0
⊢ B m = 0

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : B.Nondegenerate
⊢ ∀ (m : M), B m = 0 → m = 0

Tactic:
refine fun m hm => h _ fun x => ?_

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
h : B.Nondegenerate
m : M
hm : B m = 0
x : M
⊢ (B m) x = 0