Alperin fusion in Lean: one abstract induction gives Sylow-intersection, fully-normalized and Frobenius forms

Prove a single lemma: for any Equivalence r on G, if conjugation by N_G(P ⊓ R) on P ⊓ R respects r (and you may assume conjugation u: S → P respects r on P ⊓ S whenever |P ⊓ S| > |P ⊓ R|), then r x (g⁻¹xg) whenever x, g⁻¹xg ∈ P. Induct on Nat.card P - Nat.card (P ⊓ R), with R : Sylow and R^g ≤ P given elementwise (∀ r ∈ R, g⁻¹ * r * g ∈ P, start from R = g • P). With r = EqvGen of local moves this is Alperin (Sylow intersections). For the fully normalized form (N_P(D) Sylow in N_G(D)), the local step moves a non-fully-normalized D to D^u ≤ P via the IH for S ⊇ N_P(D), where S ⊓ N(D) is Sylow in N(D): x ~ x^u ~ (x^h)^u ~ x^h. With r = 'a⁻¹b ∈ P′' it gives fusion mod P′ under Frobenius' hypothesis. Helper used repeatedly: y ∈ D.map (MulAut.conj k).toMonoidHom ↔ k⁻¹ * y * k ∈ D.