-- Mathlib/Data/Matrix/Rank.lean
/-- Left multiplying by an invertible matrix does not change the rank -/
@[simp]
lemma rank_mul_eq_right_of_isUnit_det [Fintype m] [DecidableEq m]
    (A : Matrix m m R) (B : Matrix m n R) (hA : IsUnit A.det) :
    (A * B).rank = B.rank

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ (A * B).rank = B.rank

Tactic:
replace hA : IsUnit (LinearMap.toMatrix b b A.mulVecLin).det := by
  convert hA; rw [← LinearEquiv.eq_symm_apply]; rfl

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det
⊢ (A * B).rank = B.rank

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det
⊢ (A * B).rank = B.rank

Tactic:
have hAB : mulVecLin (A * B) = (LinearEquiv.ofIsUnitDet hA).comp (mulVecLin B) := by ext; simp

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det
hAB : (A * B).mulVecLin = ↑(LinearEquiv.ofIsUnitDet hA) ∘ₗ B.mulVecLin
⊢ (A * B).rank = B.rank

Proof state:
case h.e'_3.h.e'_6
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ A.mulVecLin = (LinearMap.toMatrix b b).symm A

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det

Tactic:
convert hA

Result:
case h.e'_3.h.e'_6
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ (LinearMap.toMatrix b b) A.mulVecLin = A

Proof state:
case h.e'_3.h.e'_6
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ (LinearMap.toMatrix b b) A.mulVecLin = A

Tactic:
rw [← LinearEquiv.eq_symm_apply]

Result:
case h.e'_3.h.e'_6
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ A.mulVecLin = (LinearMap.toMatrix b b).symm A

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det
⊢ (A * B).mulVecLin = ↑(LinearEquiv.ofIsUnitDet hA) ∘ₗ B.mulVecLin

Tactic:
ext

Result:
case h.h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det
x✝¹ : n → R
x✝ : m
⊢ (A * B).mulVecLin x✝¹ x✝ = (↑(LinearEquiv.ofIsUnitDet hA) ∘ₗ B.mulVecLin) x✝¹ x✝

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det
hAB : (A * B).mulVecLin = ↑(LinearEquiv.ofIsUnitDet hA) ∘ₗ B.mulVecLin
⊢ (A * B).rank = B.rank

Tactic:
rw [rank, rank, hAB, LinearMap.range_comp, LinearEquiv.finrank_map_eq]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
⊢ (A * B).rank = B.rank

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

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : IsUnit A.det
b : Basis m R (m → R) := Pi.basisFun R m
⊢ (A * B).rank = B.rank

Proof state:
case h.h
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
b : Basis m R (m → R) := Pi.basisFun R m
hA : IsUnit ((LinearMap.toMatrix b b) A.mulVecLin).det
x✝¹ : n → R
x✝ : m
⊢ (A * B).mulVecLin x✝¹ x✝ = (↑(LinearEquiv.ofIsUnitDet hA) ∘ₗ B.mulVecLin) x✝¹ x✝

Tactic:
simp

Result:
no goals