Tate Theorem lemma 2

lemma TateTheorem_lemma_2 [FiniteClassFormation σ] [Finite H] :    IsIso (δ (res_isShortExact σ φ) 1 2 rfl) := by  cases nonempty_fintype H  let e₁ : groupCohomology (aug R G ↓ φ) 1 ≅ .of R (R ⧸ Ideal.span {(Nat.card H : R)}) :=    Rep.aug.H1_iso' R G inj  let e₂' : (R ⧸ Ideal.span {(Nat.card H : R)}) ≃ₗ[R] groupCohomology (M ↓ φ) 2 :=    .ofBijective (Submodule.liftQ _ (.toSpanSingleton _ _ (σ ↡ φ))      (by rw [← FiniteClassFormation.hypothesis₂' σ inj])) <| by    constructor    · rw [← LinearMap.ker_eq_bot, Submodule.ker_liftQ, ← FiniteClassFormation.hypothesis₂' σ inj,        Submodule.mkQ_map_self]    · rw [← LinearMap.range_eq_top, Submodule.range_liftQ, LinearMap.range_toSpanSingleton,        FiniteClassFormation.hypothesis₂ σ inj]  let e₂ : groupCohomology (M ↓ φ) 2 ≅ .of R (R ⧸ Ideal.span {(Nat.card H : R)}) :=    e₂'.symm.toModuleIso  refine @IsIso.of_isIso_comp_right _ _ _ _ _ _ e₂.hom _ <|    @IsIso.of_isIso_comp_left _ _ _ _ _ e₁.inv _ _ ?_  suffices Function.Surjective (e₁.inv ≫ δ (res_isShortExact σ φ) 1 2 rfl ≫ e₂.hom) by    rw [ConcreteCategory.isIso_iff_bijective]    refine ⟨OrzechProperty.injective_of_surjective_endomorphism _ this, this⟩  suffices Function.Surjective (δ (res_isShortExact σ φ) 1 2 rfl) from    e₂.toLinearEquiv.surjective.comp (this.comp e₁.toLinearEquiv.symm.surjective)  rw [← ModuleCat.epi_iff_surjective]  let S := HomologicalComplex.HomologySequence.snakeInput    (map_cochainsFunctor_shortExact <| res_isShortExact (R := R) σ φ) 1 2 rfl  exact S.L₂'_exact.epi_f_iff.mpr (TateTheorem_lemma_1 _ inj)