-- Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
theorem nondegenerate_iff_det_ne_zero {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A]
    {M : Matrix n n A} : Nondegenerate M ↔ M.det ≠ 0

Proof state:
case mp
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : M.Nondegenerate
v : n → A
hv : v ≠ 0
hMv : v ᵥ* M = 0
⊢ False

Tactic:
obtain ⟨w, hwMv⟩ := hM.exists_not_ortho_of_ne_zero hv

Result:
case mp.intro
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : M.Nondegenerate
v : n → A
hv : v ≠ 0
hMv : v ᵥ* M = 0
w : n → A
hwMv : v ⬝ᵥ M *ᵥ w ≠ 0
⊢ False

Proof state:
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate ↔ M.det ≠ 0

Tactic:
rw [ne_eq, ← exists_vecMul_eq_zero_iff]

Result:
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate ↔ ¬∃ v, v ≠ 0 ∧ v ᵥ* M = 0

Proof state:
case mp
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate → ∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0

Tactic:
intro hM v hv hMv

Result:
case mp
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : M.Nondegenerate
v : n → A
hv : v ≠ 0
hMv : v ᵥ* M = 0
⊢ False

Proof state:
case mpr
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0
⊢ v = 0

Tactic:
refine not_imp_not.mp (h v) (funext fun i => ?_)

Result:
case mpr
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0
i : n
⊢ (v ᵥ* M) i = 0 i

Proof state:
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate ↔ ¬∃ v, v ≠ 0 ∧ v ᵥ* M = 0

Tactic:
push_neg

Result:
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate ↔ ∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0

Proof state:
case mp.intro
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : M.Nondegenerate
v : n → A
hv : v ≠ 0
hMv : v ᵥ* M = 0
w : n → A
hwMv : v ⬝ᵥ M *ᵥ w ≠ 0
⊢ False

Tactic:
simp [dotProduct_mulVec, hMv, zero_dotProduct, ne_eq, not_true] at hwMv

Result:
no goals

Proof state:
case mpr
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ (∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0) → M.Nondegenerate

Tactic:
intro h v hv

Result:
case mpr
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0
⊢ v = 0

Proof state:
case mpr
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0
i : n
⊢ (v ᵥ* M) i = 0 i

Tactic:
simpa only [dotProduct_mulVec, dotProduct_single, mul_one] using hv (Pi.single i 1)

Result:
no goals

Proof state:
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate ↔ ∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0

Tactic:
constructor

Result:
case mp
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate → ∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0

case mpr
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ (∀ (v : n → A), v ≠ 0 → v ᵥ* M ≠ 0) → M.Nondegenerate