-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem forget₂ToModuleCatHomotopyEquiv_f_0_eq :
    (forget₂ToModuleCatHomotopyEquiv k G).1.f 0 = (forget₂ (Rep k G) _).map (ε k G)

Proof state:
case h.e'_3.h.hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map (ε k G)) =
    ModuleCat.Hom.hom
      ((extraDegeneracyCompForgetAugmentedToModule k G).homotopyEquiv.hom.f 0 ≫
        (HomotopyEquiv.ofIso
                ((ChainComplex.single₀ (ModuleCat k)).mapIso
                  (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
          0)

Tactic:
trans (linearCombination _ fun _ => (1 : k)).comp ((ModuleCat.free k).map (terminal.from _)).hom

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map (ε k G)) =
    (linearCombination k fun x => 1) ∘ₗ ModuleCat.Hom.hom ((ModuleCat.free k).map (terminal.from (Fin 1 → G)))

k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (linearCombination k fun x => 1) ∘ₗ ModuleCat.Hom.hom ((ModuleCat.free k).map (terminal.from (Fin 1 → G))) =
    ModuleCat.Hom.hom
      ((extraDegeneracyCompForgetAugmentedToModule k G).homotopyEquiv.hom.f 0 ≫
        (HomotopyEquiv.ofIso
                ((ChainComplex.single₀ (ModuleCat k)).mapIso
                  (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
          0)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map (ε k G)) =
    (linearCombination k fun x => 1) ∘ₗ ModuleCat.Hom.hom ((ModuleCat.free k).map (terminal.from (Fin 1 → G)))

Tactic:
erw [Finsupp.lmapDomain_linearCombination (α := Fin 1 → G) (R := k) (α' := ⊤_ Type u)
    (v := fun _ => (1 : k)) (v' := fun _ => (1 : k))
    (terminal.from
      ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk 0))).V)
    LinearMap.id fun i => rfl,
  LinearMap.id_comp]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map (ε k G)) = linearCombination k fun x => 1

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (linearCombination k fun x => 1) ∘ₗ ModuleCat.Hom.hom ((ModuleCat.free k).map (terminal.from (Fin 1 → G))) =
    ModuleCat.Hom.hom
      ((extraDegeneracyCompForgetAugmentedToModule k G).homotopyEquiv.hom.f 0 ≫
        (HomotopyEquiv.ofIso
                ((ChainComplex.single₀ (ModuleCat k)).mapIso
                  (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
          0)

Tactic:
rw [ModuleCat.hom_comp]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (linearCombination k fun x => 1) ∘ₗ ModuleCat.Hom.hom ((ModuleCat.free k).map (terminal.from (Fin 1 → G))) =
    ModuleCat.Hom.hom
        ((HomotopyEquiv.ofIso
                ((ChainComplex.single₀ (ModuleCat k)).mapIso
                  (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
          0) ∘ₗ
      ModuleCat.Hom.hom ((extraDegeneracyCompForgetAugmentedToModule k G).homotopyEquiv.hom.f 0)

Proof state:
case h.e'_3.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) =
    (extraDegeneracyCompForgetAugmentedToModule k G).homotopyEquiv.hom.f 0 ≫
      (HomotopyEquiv.ofIso
              ((ChainComplex.single₀ (ModuleCat k)).mapIso
                (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
        0

Tactic:
ext : 1

Result:
case h.e'_3.h.hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map (ε k G)) =
    ModuleCat.Hom.hom
      ((extraDegeneracyCompForgetAugmentedToModule k G).homotopyEquiv.hom.f 0 ≫
        (HomotopyEquiv.ofIso
                ((ChainComplex.single₀ (ModuleCat k)).mapIso
                  (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
          0)

Proof state:
case e_f.h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x : ⊤_ Type u
⊢ (linearCombination k fun x => 1) (single default 1) =
    (ModuleCat.Hom.hom
        (((ChainComplex.single₀ (ModuleCat k)).map
              (ModuleCat.ofHom { toFun := (fun f => f default) ∘ ⇑equivFunOnFinite, map_add' := ⋯, map_smul' := ⋯ })).f
          0))
      (single default 1)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_6.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
e_4✝ : (compForgetAugmented.toModule k G).left.obj (Opposite.op (SimplexCategory.mk 0)) = (forget₂ToModuleCat k G).X 0
⊢ (HomotopyEquiv.ofIso (compForgetAugmentedIso k G).symm).hom.f 0 = 𝟙 ((forget₂ToModuleCat k G).X 0)

Tactic:
dsimp only [HomotopyEquiv.ofIso, compForgetAugmentedIso]

Result:
case h.e'_2.h.h.e'_6.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
e_4✝ : (compForgetAugmented.toModule k G).left.obj (Opposite.op (SimplexCategory.mk 0)) = (forget₂ToModuleCat k G).X 0
⊢ (eqToIso ⋯).symm.hom.f 0 = 𝟙 ((forget₂ToModuleCat k G).X 0)