-- Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean
theorem nondegenerate_of_det_ne_zero [DecidableEq m] {M : Matrix m m A} (hM : M.det ≠ 0) :
    Nondegenerate M

Proof state:
case h.e'_2
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ v i * M.det = ∑ x : m, v x * (M.det * Pi.single i 1 x)

Tactic:
rw [Finset.sum_eq_single i, Pi.single_eq_same, mul_one]

Result:
case h.e'_2.h₀
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ ∀ b ∈ Finset.univ, b ≠ i → v b * (M.det * Pi.single i 1 b) = 0

case h.e'_2.h₁
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ i ∉ Finset.univ → v i * (M.det * Pi.single i 1 i) = 0

Proof state:
case h.e'_2.h₁
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ i ∉ Finset.univ → v i * (M.det * Pi.single i 1 i) = 0

Tactic:
intros

Result:
case h.e'_2.h₁
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
a✝ : i ∉ Finset.univ
⊢ v i * (M.det * Pi.single i 1 i) = 0

Proof state:
case h.e'_2
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ v i * M.det = v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1)

Tactic:
simp only [mulVec_cramer M (Pi.single i 1), dotProduct, Pi.smul_apply, smul_eq_mul]

Result:
case h.e'_2
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ v i * M.det = ∑ x : m, v x * (M.det * Pi.single i 1 x)

Proof state:
case h.e'_2.h₀
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
j : m
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ v j * (M.det * Pi.single i 1 j) = 0

Tactic:
simp [hj]

Result:
no goals

Proof state:
case h.e'_2.h₁
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
a✝ : i ∉ Finset.univ
this : i ∈ Finset.univ
⊢ v i * (M.det * Pi.single i 1 i) = 0

Tactic:
contradiction

Result:
no goals

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

Tactic:
specialize hv (M.cramer (Pi.single i 1))

Result:
case h
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ v i = 0 i

Proof state:
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
⊢ M.Nondegenerate

Tactic:
intro v hv

Result:
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ M *ᵥ w = 0
⊢ v = 0

Proof state:
case h
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ v i = 0 i

Tactic:
refine (mul_eq_zero.mp ?_).resolve_right hM

Result:
case h
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ v i * M.det = 0

Proof state:
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ M *ᵥ w = 0
⊢ v = 0

Tactic:
ext i

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

Proof state:
case h.e'_2.h₀
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ ∀ b ∈ Finset.univ, b ≠ i → v b * (M.det * Pi.single i 1 b) = 0

Tactic:
intro j _ hj

Result:
case h.e'_2.h₀
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
j : m
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ v j * (M.det * Pi.single i 1 j) = 0

Proof state:
case h
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ v i * M.det = 0

Tactic:
convert hv

Result:
case h.e'_2
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
⊢ v i * M.det = v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1)

Proof state:
case h.e'_2.h₁
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
a✝ : i ∉ Finset.univ
⊢ v i * (M.det * Pi.single i 1 i) = 0

Tactic:
have := Finset.mem_univ i

Result:
case h.e'_2.h₁
m : Type u_1
A : Type u_3
inst✝³ : Fintype m
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0
a✝ : i ∉ Finset.univ
this : i ∈ Finset.univ
⊢ v i * (M.det * Pi.single i 1 i) = 0