Group Cohomology trivial Cohomology of even of odd of solvable

theorem groupCohomology.trivialCohomology_of_even_of_odd_of_solvable [Finite G] [Group.IsSolvable 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 where  isZero H := by    classical    induction H using solvable_ind with    | bot =>      intro n      exact isZero_groupCohomology_succ_of_subsingleton ..    | ind K H h12 h1 h2 h3 =>    have IH : ∀ i, IsZero (groupCohomology (M ↓ H.subtype ↓        (QuotientGroup.mk' (K.subgroupOf H)).ker.subtype) (i + 1)) := by      refine fun i ↦ .of_iso (h3 (n := i)) <| groupCohomology.mapIso ((MulEquiv.subgroupCongr <|        QuotientGroup.ker_mk' _).trans <| Subgroup.subgroupOfEquivOfLe h12)        (LinearEquiv.refl _ _) (by simp) _    have : ∀ n, IsIso ((infl (QuotientGroup.mk'_surjective        (K.subgroupOf H)) (n + 1)).app (M ↓ H.subtype)) := by      intro n      apply (config := { allowSynthFailures := true }) isIso_of_mono_of_epi      · exact inflation_restriction_mono (R := R)          (QuotientGroup.mk'_surjective (K.subgroupOf H)) n (M := M ↓ H.subtype) (fun i _ ↦ IH i)      · exact (inflation_restriction_exact (QuotientGroup.mk'_surjective _) n fun i _ ↦ IH i).epi_f          ((IH _).eq_zero_of_tgt _)    have : ∀ n : ℕ, groupCohomology ((M ↓ H.subtype) ↑      (QuotientGroup.mk'_surjective (K.subgroupOf H))) (n + 1) ≅      groupCohomology (M ↓ H.subtype) (n + 1) := fun n ↦ asIso ((infl (QuotientGroup.mk'_surjective        (K.subgroupOf H)) (n + 1)).app (M ↓ H.subtype))    specialize h_even H H.subtype_injective    specialize h_odd H H.subtype_injective    have zero1 := IsZero.of_iso h_even <| this (2 * n + 1)    have zero2 := IsZero.of_iso h_odd <| this (2 * m)    intro k    refine .of_iso (Rep.isZero_ofEven_odd ?_ ?_ zero1 zero2 _) <| this k |>.symm <;>      simp [parity_simps]