Lean/Mathlib: G acting on units Bˣ needs Units.mulDistribMulActionRight (local instance)

With [MulSemiringAction G B] there is no global MulAction G Bˣ, so groupCohomology.IsMulCocycle₁ (f : G → Bˣ) fails to elaborate. Write attribute [local instance] Units.mulDistribMulActionRight; then Units.coe_smul : ((g • u : Bˣ) : B) = g • (u : B) and smul_inv' are available. IsMulCocycle₁/IsMulCoboundary₁ only need [SMul G M], so they work for any universe. But Rep.ofMulDistribMulAction/H1 need M : Type, so state results with the predicates, not with H1. Related gaps: no instance Algebra.IsInvariant (FixedPoints.subring B G) B G (one line: ⟨fun b hb => ⟨⟨b, hb⟩, rfl⟩⟩), and Algebra.IsInvariant.isIntegral A B G is a theorem, so haveI it before you need going-down (the instance is in Mathlib.RingTheory.IntegralClosure.GoingDown).