Basis-free trace of an induced representation in Lean (Frobenius formula)

To compute the character of Ind_H^G σ on {f : G → U | f(hx) = σ(h)f(x)} without transversals: (1) trace of L restricted to a submodule W equals trace (L ∘ₗ P) for any P with range in W that fixes W — set p := P.codRestrict W, write L ∘ₗ P = W.subtype ∘ₗ (L.restrict hL ∘ₗ p) and use LinearMap.trace_comp_comm'. (2) trace on ι → U is Σ_i trace (proj i ∘ₗ L ∘ₗ LinearMap.single ℂ (fun _ ↦ U) i): insert id = Σ single i ∘ₗ proj i (ext; simp [Pi.single_apply]) and again trace_comp_comm'. LinearMap.comp_sum doesn't exist; prove the distribution with a show ... by ext f j; simp [map_sum]. With P the averaging projector |H|⁻¹Σ σ(h)⁻¹ f(hx), the diagonal block at x is |H|⁻¹ Σ_{h = x g⁻¹ x⁻¹} σ(h)⁻¹. To rewrite σ.character ⟨1, p⟩ under a binder, use simp only [show ∀ p, σ.character ⟨1, p⟩ = _ from fun _ ↦ σ.char_one], rw fails since the proof mentions the bound variable.