-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem vecMul_injective_iff_isUnit {A : Matrix m m K} :
    Function.Injective A.vecMul ↔ IsUnit A

Proof state:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ Function.Injective fun v => v ᵥ* A

Tactic:
change Function.Injective A.vecMulLinear

Result:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ Function.Injective ⇑A.vecMulLinear

Proof state:
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ (Function.Injective fun v => v ᵥ* A) ↔ IsUnit A

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : Function.Injective fun v => v ᵥ* A
⊢ IsUnit A

case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ Function.Injective fun v => v ᵥ* A

Proof state:
case refine_1
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : Function.Injective fun v => v ᵥ* A
⊢ Function.Surjective fun v => v ᵥ* A

Tactic:
exact LinearMap.surjective_of_injective (f := A.vecMulLinear) h

Result:
no goals

Proof state:
case refine_1
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : Function.Injective fun v => v ᵥ* A
⊢ IsUnit A

Tactic:
rw [← vecMul_surjective_iff_isUnit]

Result:
case refine_1
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : Function.Injective fun v => v ᵥ* A
⊢ Function.Surjective fun v => v ᵥ* A

Proof state:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
c : m → K
hc : A.vecMulLinear c = 0
h : Invertible A
⊢ c = 0

Tactic:
simpa using congr_arg A⁻¹.vecMulLinear hc

Result:
no goals

Proof state:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ ∀ (m_1 : m → K), A.vecMulLinear m_1 = 0 → m_1 = 0

Tactic:
intro c hc

Result:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
c : m → K
hc : A.vecMulLinear c = 0
⊢ c = 0

Proof state:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ Function.Injective ⇑A.vecMulLinear

Tactic:
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']

Result:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ ∀ (m_1 : m → K), A.vecMulLinear m_1 = 0 → m_1 = 0

Proof state:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
c : m → K
hc : A.vecMulLinear c = 0
⊢ c = 0

Tactic:
replace h := h.invertible

Result:
case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
c : m → K
hc : A.vecMulLinear c = 0
h : Invertible A
⊢ c = 0