-- Mathlib/Data/Matrix/Rank.lean
theorem rank_conjTranspose_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✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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 (mulVecLin A))) ?_

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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_conjTranspose_mul_self]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing 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)