Group Cohomology trivial Cohomology of even of odd

theorem groupCohomology.trivialCohomology_of_even_of_odd [Finite G]    (M : Rep R G) (n m : ℕ)    -- todo: don't quantify over all types    (h_even : ∀ (H : Type) [Group H] {φ : H →* G} (_ : Function.Injective φ),      IsZero (groupCohomology (M ↓ φ) (2 * n + 2)))    (h_odd : ∀ (H : Type) [Group H] {φ : H →* G} (_ : Function.Injective φ),      IsZero (groupCohomology (M ↓ φ) (2 * m + 1))) :    M.TrivialCohomology := by  constructor  -- let `S` be a subgroup of `G`  intro S u  refine @ModuleCat.isZero_of_subsingleton R _ _    (@Unique.instSubsingleton _ ⟨⟨0⟩, fun x => (?_ : x = 0)⟩)  -- `Hᵘ⁺¹(S, M)` is torsion  have hx : Nat.card S • x = 0 := by    classical    have : Fintype S := Fintype.ofFinite S    apply torsion_of_finite_of_neZero  -- it suffices to show that for every prime `p`, it has no `p^∞` torsion  have hk : 0 < Nat.card S := Nat.card_pos  generalize Nat.card S = k at hx hk  induction k using Nat.recOnPrimePow with  | zero => simp at hk  | one => simpa using hx  | prime_pow_mul a p c hp ha hc ih =>    refine ih ?_ (Nat.pos_of_mul_pos_left hk)    -- let `v` be an arbitrary Sylow-`p` subgroup of `S`    obtain ⟨v⟩ : Nonempty (Sylow p S) := inferInstance    rw [mul_smul] at hx    -- the `p^∞` torsion injects into `Hᵘ⁺¹(v,M)`, so it suffices that `Hᵘ⁺¹(v,M)` is trivial    haveI : Fact p.Prime := ⟨hp⟩    apply (groupCohomology_Sylow (Nat.add_one_pos u) (M ↓ S.subtype) (a • x) p v ⟨c, hx⟩).mtr    -- `Hᵘ⁺¹(v,M)` is trivial if `M` has trivial cohomology    refine @Subsingleton.eq_zero _ _ (ModuleCat.subsingleton_of_isZero      (@isZero_of_trivialCohomology R v _ _ _ ?_ (u + 1) _)) _    -- `v` is a `p`-group, so it is solvable    have : Fact p.Prime := ⟨hp⟩    have : Group.IsNilpotent v := v.isPGroup'.isNilpotent -- todo: make this an instance?    have : Fintype v := Fintype.ofFinite v    classical    -- therefore `M` has trivial cohomology if it has an even and an odd trivial cohomology    apply trivialCohomology_of_even_of_odd_of_solvable (M ↓ S.subtype ↓ v.toSubgroup.subtype) n m    · -- the even trivial cohomology for `G` lifts to `v`      intro H  _ φ hφ      refine .of_iso (h_even H (φ := (S.subtype.comp v.toSubgroup.subtype).comp φ)        ((S.subtype_injective.comp v.toSubgroup.subtype_injective).comp hφ)) ?_      apply (functor R H (2 * n + 2)).mapIso      exact (Rep.resComp (R := R) (S.subtype.comp v.toSubgroup.subtype) φ).trans        (NatIso.hcomp (Rep.resComp _ _) (Iso.refl _)) |>.symm.app M    · -- the odd trivial cohomology for `G` lifts to `v`      intro H  _ φ hφ      refine .of_iso (h_odd H (φ := (S.subtype.comp v.toSubgroup.subtype).comp φ)        ((S.subtype_injective.comp v.toSubgroup.subtype_injective).comp hφ)) ?_      apply (functor R H (2 * m + 1)).mapIso      exact (Rep.resComp (R := R) (S.subtype.comp v.toSubgroup.subtype) φ).trans        (NatIso.hcomp (Rep.resComp _ _) (Iso.refl _)) |>.symm.app M