theorem ConjugatorProof.conjugator_in_target_from_bnpair {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S₁ S₂ : Set B_idx) (g : G) : (fun (x : G) => g * x * g⁻¹) '' bp.standardParabolic S₁ = bp.standardParabolic S₂ → g ∈ bp.standardParabolic S₂

Conjugator-target lemma. If $g \in G$ conjugates the standard parabolic $P_{S_1} = BW_{S_1}B$ onto $P_{S_2}$, then $g$ itself lies in $P_{S_2}$. This is the key step in showing that no two standard parabolics are conjugate in a BN-pair: any conjugator is forced to land in the target.