-- Mathlib/Data/Matrix/Bilinear.lean
theorem mulRightLinearMap_eq_zero_iff (a : Matrix m n A) [Nonempty l] :
    mulRightLinearMap l R a = 0 ↔ 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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
inhabited_h : Inhabited l
i : m
j : n
⊢ a i j = 0 i j

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

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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
inhabited_h : Inhabited l
⊢ 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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
inhabited_h : Inhabited l
i : m
j : n
⊢ a i j = 0 i j

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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ mulRightLinearMap l 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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l 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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : a = 0
⊢ mulRightLinearMap l R 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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : a = 0
⊢ mulRightLinearMap l 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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : a = 0
⊢ mulRightLinearMap l R 0 = 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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : a = 0
⊢ mulRightLinearMap l R 0 = 0

Tactic:
exact mulRightLinearMap_zero_eq_zero _ _

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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
inhabited_h : Inhabited l
i : m
j : n
h : (mulRightLinearMap l R a) (Matrix.stdBasisMatrix default i 1) = 0 (Matrix.stdBasisMatrix default i 1)
⊢ a i j = 0 i j

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

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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
⊢ a = 0

Tactic:
inhabit l

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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
inhabited_h : Inhabited l
⊢ 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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
inhabited_h : Inhabited l
i : m
j : n
⊢ a i j = 0 i j

Tactic:
replace h := DFunLike.congr_fun h (Matrix.stdBasisMatrix (default : l) i 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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
inhabited_h : Inhabited l
i : m
j : n
h : (mulRightLinearMap l R a) (Matrix.stdBasisMatrix default i 1) = 0 (Matrix.stdBasisMatrix default i 1)
⊢ a i j = 0 i j