-- Mathlib/Data/Matrix/Bilinear.lean
theorem mulLeftLinearMap_eq_zero_iff [Nonempty n] (a : Matrix l m A) :
    mulLeftLinearMap n R a = 0 ↔ a = 0

Proof state:
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R a = 0

Tactic:
rw [h]

Result:
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R 0 = 0

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ mulLeftLinearMap n R a = 0 ↔ a = 0

Tactic:
constructor <;> intro h

Result:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
⊢ a = 0

case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R a = 0

Proof state:
case mp.a
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
i : l
j : m
⊢ a i j = 0 i j

Tactic:
replace h := DFunLike.congr_fun h (Matrix.stdBasisMatrix j (default : n) 1)

Result:
case mp.a
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
inhabited_h : Inhabited n
i : l
j : m
h : (mulLeftLinearMap n R a) (Matrix.stdBasisMatrix j default 1) = 0 (Matrix.stdBasisMatrix j default 1)
⊢ a i j = 0 i j

Proof state:
case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R 0 = 0

Tactic:
exact mulLeftLinearMap_zero_eq_zero _ _

Result:
no goals

Proof state:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
⊢ a = 0

Tactic:
ext i j

Result:
case mp.a
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
i : l
j : m
⊢ a i j = 0 i j

Proof state:
case mp.a
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
inhabited_h : Inhabited n
i : l
j : m
h : (mulLeftLinearMap n R a) (Matrix.stdBasisMatrix j default 1) = 0 (Matrix.stdBasisMatrix j default 1)
⊢ a i j = 0 i j

Tactic:
simpa using Matrix.ext_iff.2 h i default

Result:
no goals

Proof state:
case mp.a
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
i : l
j : m
⊢ a i j = 0 i j

Tactic:
classical
replace h := DFunLike.congr_fun h (Matrix.stdBasisMatrix j (default : n) 1)
simpa using Matrix.ext_iff.2 h i default

Result:
no goals

Proof state:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
⊢ a = 0

Tactic:
inhabit n

Result:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
⊢ a = 0