-- Mathlib/Data/Matrix/Rank.lean
lemma rank_add_rank_le_card_of_mul_eq_zero [Field R] [Finite l] [Fintype m]
    {A : Matrix l m R} {B : Matrix m n R} (hAB : A * B = 0) :
    A.rank + B.rank ≤ Fintype.card m

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ finrank R ↥(LinearMap.range ((toLin en em) B)) ≤ finrank R ↥(LinearMap.ker ((toLin em el) A))

Tactic:
apply Submodule.finrank_mono

Result:
case hst
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ LinearMap.range ((toLin en em) B) ≤ LinearMap.ker ((toLin em el) A)

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
let en : Basis n R (n → R) := Pi.basisFun R n

Result:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ A.rank + B.rank ≤ Fintype.card m

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
let el : Basis l R (l → R) := Pi.basisFun R l

Result:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
⊢ A.rank + B.rank ≤ Fintype.card m

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
rw [Matrix.rank_eq_finrank_range_toLin A el em,
    Matrix.rank_eq_finrank_range_toLin B em en,
    ← Module.finrank_fintype_fun_eq_card R,
    ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A),
    add_le_add_iff_left]

Result:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ finrank R ↥(LinearMap.range ((toLin en em) B)) ≤ finrank R ↥(LinearMap.ker ((toLin em el) A))

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
classical
let el : Basis l R (l → R) := Pi.basisFun R l
let em : Basis m R (m → R) := Pi.basisFun R m
let en : Basis n R (n → R) := Pi.basisFun R n
rw [Matrix.rank_eq_finrank_range_toLin A el em,
    Matrix.rank_eq_finrank_range_toLin B em en,
    ← Module.finrank_fintype_fun_eq_card R,
    ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A),
    add_le_add_iff_left]
apply Submodule.finrank_mono
rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]

Result:
no goals

Proof state:
case hst
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ LinearMap.range ((toLin en em) B) ≤ LinearMap.ker ((toLin em el) A)

Tactic:
rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
let em : Basis m R (m → R) := Pi.basisFun R m

Result:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
⊢ A.rank + B.rank ≤ Fintype.card m