-- 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:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ((HomotopyEquiv.ofIso (compForgetAugmentedIso k G).symm).hom ≫
          (extraDegeneracyCompForgetAugmentedToModule k G).homotopyEquiv.hom ≫
            (HomotopyEquiv.ofIso
                ((ChainComplex.single₀ (ModuleCat k)).mapIso
                  (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom).f
      0 =
    (forget₂ (Rep k G) (ModuleCat k)).map (ε k G)

Tactic:
simp only [HomologicalComplex.comp_f]

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

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
        ((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)

Tactic:
congr

Result:
case e_f
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (linearCombination k fun x => 1) =
    ModuleCat.Hom.hom
      ((HomotopyEquiv.ofIso
              ((ChainComplex.single₀ (ModuleCat k)).mapIso
                (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
        0)

case e_g.e_f.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ terminal.from (Fin 1 → G) = (compForgetAugmented G).hom.app (Opposite.op (SimplexCategory.mk 0))

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

Tactic:
convert Category.id_comp (X := (forget₂ToModuleCat k G).X 0) _

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
⊢ (HomotopyEquiv.ofIso (compForgetAugmentedIso k G).symm).hom.f 0 = 𝟙 ((forget₂ToModuleCat k G).X 0)

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

Proof state:
case e_f
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (linearCombination k fun x => 1) =
    ModuleCat.Hom.hom
      ((HomotopyEquiv.ofIso
              ((ChainComplex.single₀ (ModuleCat k)).mapIso
                (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
        0)

Tactic:
ext x

Result:
case e_f.h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x : ⊤_ Type u
⊢ ((linearCombination k fun x => 1) ∘ₗ lsingle x) 1 =
    (ModuleCat.Hom.hom
          ((HomotopyEquiv.ofIso
                  ((ChainComplex.single₀ (ModuleCat k)).mapIso
                    (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
            0) ∘ₗ
        lsingle x)
      1

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0 = (forget₂ (Rep k G) (ModuleCat k)).map (ε k G)

Tactic:
show (HomotopyEquiv.hom _ ≫ HomotopyEquiv.hom _ ≫ HomotopyEquiv.hom _).f 0 = _

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

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 x 1) =
    (ModuleCat.Hom.hom
        (((ChainComplex.single₀ (ModuleCat k)).map
              (ModuleCat.ofHom { toFun := (fun f => f default) ∘ ⇑equivFunOnFinite, map_add' := ⋯, map_smul' := ⋯ })).f
          0))
      (single x 1)

Tactic:
rw [@Unique.eq_default _ Types.terminalIso.toEquiv.unique x]

Result:
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)

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

Tactic:
rfl

Result:
no goals

Proof state:
case e_g.e_f.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ terminal.from (Fin 1 → G) = (compForgetAugmented G).hom.app (Opposite.op (SimplexCategory.mk 0))

Tactic:
exact @Subsingleton.elim _ (@Unique.instSubsingleton _ (Limits.uniqueToTerminal _)) _ _

Result:
no goals

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) ∘ₗ lsingle x) 1 =
    (ModuleCat.Hom.hom
          ((HomotopyEquiv.ofIso
                  ((ChainComplex.single₀ (ModuleCat k)).mapIso
                    (LinearEquiv.finsuppUnique k k (⊤_ Type u)).toModuleIso)).hom.f
            0) ∘ₗ
        lsingle x)
      1

Tactic:
dsimp (config := { unfoldPartialApp := true }) [HomotopyEquiv.ofIso,
  Finsupp.LinearEquiv.finsuppUnique]

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

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
⊢ (eqToIso ⋯).symm.hom.f 0 = 𝟙 ((forget₂ToModuleCat k G).X 0)

Tactic:
simp only [Iso.symm_hom, eqToIso.inv, HomologicalComplex.eqToHom_f, eqToHom_refl]

Result:
no goals