-- Mathlib/Data/Matrix/Rank.lean
theorem rank_transpose_mul_self (A : Matrix m n R) : (Aᵀ * A).rank = A.rank

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ (Aᵀ * A).rank = A.rank

Tactic:
dsimp only [rank]

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)

Tactic:
trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } +
  finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) }

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin)

m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ (fun x => x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin)) =
    (fun x => x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range A.mulVecLin))

Tactic:
dsimp only

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin) =
    finrank R ↥(LinearMap.range A.mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin)

Tactic:
simp only [LinearMap.finrank_range_add_finrank_ker]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
refine add_left_injective (finrank R <| LinearMap.ker A.mulVecLin) ?_

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ (fun x => x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin)) =
    (fun x => x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range A.mulVecLin))

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker A.mulVecLin) =
    finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) + finrank R ↥(LinearMap.ker (Aᵀ * A).mulVecLin)

Tactic:
rw [ker_mulVecLin_transpose_mul_self]

Result:
no goals