-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.vecMul_injective_iff {R : Type*} [CommRing R] {M : Matrix m n R} :
    Function.Injective M.vecMul ↔ LinearIndependent R (fun i ↦ M i)

Proof state:
case refine_1.h
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (x : m → R), x ᵥ* M = 0 → x = 0
c : m → R
h0 : ∑ i : m, c i • M i = 0
i : n
⊢ (c ᵥ* M) i = (∑ i : m, c i • M i) i

Tactic:
simp [vecMul, dotProduct]

Result:
no goals

Proof state:
case refine_1
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (x : m → R), x ᵥ* M = 0 → x = 0
c : m → R
h0 : ∑ i : m, c i • M i = 0
⊢ c ᵥ* M = 0

Tactic:
rw [← h0]

Result:
case refine_1
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (x : m → R), x ᵥ* M = 0 → x = 0
c : m → R
h0 : ∑ i : m, c i • M i = 0
⊢ c ᵥ* M = ∑ i : m, c i • M i

Proof state:
case refine_2.h
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (g : m → R), ∑ i : m, g i • M i = 0 → ∀ (i : m), g i = 0
c : m → R
h0 : c ᵥ* M = 0
j : n
⊢ (∑ i : m, c i • M i) j = (c ᵥ* M) j

Tactic:
simp [vecMul, dotProduct]

Result:
no goals

Proof state:
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
⊢ Function.Injective ⇑M.vecMulLinear ↔ LinearIndependent R fun i => M i

Tactic:
simp only [← LinearMap.ker_eq_bot, Fintype.linearIndependent_iff, Submodule.eq_bot_iff,
  LinearMap.mem_ker, vecMulLinear_apply]

Result:
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
⊢ (∀ (x : m → R), x ᵥ* M = 0 → x = 0) ↔ ∀ (g : m → R), ∑ i : m, g i • M i = 0 → ∀ (i : m), g i = 0

Proof state:
case refine_1
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (x : m → R), x ᵥ* M = 0 → x = 0
c : m → R
h0 : ∑ i : m, c i • M i = 0
⊢ c ᵥ* M = ∑ i : m, c i • M i

Tactic:
ext i

Result:
case refine_1.h
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (x : m → R), x ᵥ* M = 0 → x = 0
c : m → R
h0 : ∑ i : m, c i • M i = 0
i : n
⊢ (c ᵥ* M) i = (∑ i : m, c i • M i) i

Proof state:
case refine_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (g : m → R), ∑ i : m, g i • M i = 0 → ∀ (i : m), g i = 0
c : m → R
h0 : c ᵥ* M = 0
⊢ ∑ i : m, c i • M i = 0

Tactic:
rw [← h0]

Result:
case refine_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (g : m → R), ∑ i : m, g i • M i = 0 → ∀ (i : m), g i = 0
c : m → R
h0 : c ᵥ* M = 0
⊢ ∑ i : m, c i • M i = c ᵥ* M

Proof state:
case refine_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (g : m → R), ∑ i : m, g i • M i = 0 → ∀ (i : m), g i = 0
c : m → R
h0 : c ᵥ* M = 0
⊢ ∑ i : m, c i • M i = c ᵥ* M

Tactic:
ext j

Result:
case refine_2.h
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (g : m → R), ∑ i : m, g i • M i = 0 → ∀ (i : m), g i = 0
c : m → R
h0 : c ᵥ* M = 0
j : n
⊢ (∑ i : m, c i • M i) j = (c ᵥ* M) j

Proof state:
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
⊢ (∀ (x : m → R), x ᵥ* M = 0 → x = 0) ↔ ∀ (g : m → R), ∑ i : m, g i • M i = 0 → ∀ (i : m), g i = 0

Tactic:
refine ⟨fun h c h0 ↦ congr_fun <| h c ?_, fun h c h0 ↦ funext <| h c ?_⟩

Result:
case refine_1
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (x : m → R), x ᵥ* M = 0 → x = 0
c : m → R
h0 : ∑ i : m, c i • M i = 0
⊢ c ᵥ* M = 0

case refine_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
h : ∀ (g : m → R), ∑ i : m, g i • M i = 0 → ∀ (i : m), g i = 0
c : m → R
h0 : c ᵥ* M = 0
⊢ ∑ i : m, c i • M i = 0

Proof state:
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
⊢ (Function.Injective fun v => v ᵥ* M) ↔ LinearIndependent R fun i => M i

Tactic:
rw [← coe_vecMulLinear]

Result:
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
R : Type u_5
inst✝ : CommRing R
M : Matrix m n R
⊢ Function.Injective ⇑M.vecMulLinear ↔ LinearIndependent R fun i => M i