l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } = finrank R { x // x ∈ LinearMap.range (mulVecLin A) }
l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ rank (Aᴴ ⬝ A) = rank A
dsimp only [rank]
l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (fun x => x + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) })
      (finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) }) =
    (fun x => x + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) })
      (finrank R { x // x ∈ LinearMap.range (mulVecLin A) })
l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } = finrank R { x // x ∈ LinearMap.range (mulVecLin A) }
refine' add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) _
l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) }
l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (fun x => x + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) })
      (finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) }) =
    (fun x => x + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) })
      (finrank R { x // x ∈ LinearMap.range (mulVecLin A) })
dsimp only
l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
      finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) }

l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
      finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) }
l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) }
trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
  finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) }
no goals
l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
      finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) }
rw [ker_mulVecLin_conjTranspose_mul_self]
no goals
l : Type ?u.244698
m : Type u_1
n : Type u_2
o : Type ?u.244707
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
      finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) } =
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) }
simp only [LinearMap.finrank_range_add_finrank_ker]