\begin{lemma}[Conditional rho and relabeling]\label{rho-cond-relabeled}\lean{condRho_of_injective}\leanok
  If $f$ is injective, then $\rho(X|f(Y))=\rho(X|Y)$.
\end{lemma}
\begin{proof}\leanok
  \uses{rho-cond-def}
  Clear from the definition.
\end{proof}
/-- If $f$ is injective, then $\rho(X|f(Y))=\rho(X|Y)$. -/
lemma condRho_of_injective {S T : Type*}
    (Y : Ω → S) {A : Finset G} {f : S → T} (hf : Function.Injective f) :
    ρ[X | f ∘ Y ; μ # A] = ρ[X | Y ; μ # A] := by
  simp only [condRho]
  rw [← hf.tsum_eq]
  · have I c : f ∘ Y ⁻¹' {f c} = Y ⁻¹' {c} := by
      ext z; simp [hf.eq_iff]
    simp [I]
  · intro y hy
    have : f ∘ Y ⁻¹' {y} ≠ ∅ := by
      intro h
      simp [h] at hy
    rcases Set.nonempty_iff_ne_empty.2 this with ⟨a, ha⟩
    simp only [mem_preimage, Function.comp_apply, mem_singleton_iff] at ha
    rw [← ha]
    exact mem_range_self (Y a)