Pinching pythagoras

theorem pinching_pythagoras (ρ σ : MState d) :    𝐃(ρ‖σ) = 𝐃(ρ‖pinching_map σ ρ) + 𝐃(pinching_map σ ρ‖σ) := by  by_cases h_ker : σ.M.ker ≤ ρ.M.ker  · have h_ker₁ : (pinching_map σ ρ).M.ker ≤ ρ.M.ker := pinching_map_ker_le ρ σ    have h_ker₂ : σ.M.ker ≤ (pinching_map σ ρ).M.ker := ker_le_ker_pinching_map_ker ρ σ h_ker    rw [← EReal.coe_ennreal_eq_coe_ennreal_iff, EReal.coe_ennreal_add]    rw [qRelativeEnt_ker h_ker, qRelativeEnt_ker h_ker₁, qRelativeEnt_ker h_ker₂]    have h_eq₁ := inner_cfc_pinching_right ρ σ Real.log    have h_eq₂ := inner_cfc_pinching ρ σ Real.log    rw [← HermitianMat.log] at h_eq₁ h_eq₂    simp only [inner_sub_right]    rw [h_eq₂, h_eq₁]    simp only [EReal.coe_sub]    rw [← add_sub_assoc, EReal.sub_add_cancel]  · simp only [qRelativeEnt, SandwichedRelRentropy, dif_pos zero_lt_one]    trans ⊤    · exact dif_neg h_ker    · convert (add_top _).symm      apply dif_neg ?_      contrapose! h_ker      exact h_ker.trans (pinching_map_ker_le ρ σ)