-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem dTwo_comp_dOne : dTwo A ∘ₗ dOne A = 0

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
h1 :
  ModuleCat.ofHom (dOne A ∘ₗ ↑(oneCochainsLequiv A)) =
    ModuleCat.ofHom (↑(twoCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2))
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A)) = 0

Tactic:
have h2 := congr_arg ModuleCat.ofHom (dTwo_comp_eq A)

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
h1 :
  ModuleCat.ofHom (dOne A ∘ₗ ↑(oneCochainsLequiv A)) =
    ModuleCat.ofHom (↑(twoCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2))
h2 :
  ModuleCat.ofHom (dTwo A ∘ₗ ↑(twoCochainsLequiv A)) =
    ModuleCat.ofHom (↑(threeCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 2 3))
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A)) = 0

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ dTwo A ∘ₗ dOne A = 0

Tactic:
show (ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A)).hom = _

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A)) = 0

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
h1 :
  (oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (dOne A) =
    ModuleCat.ofHom (ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2)) ≫ (twoCochainsLequiv A).toModuleIso.hom
h2 :
  (twoCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (dTwo A) =
    ModuleCat.ofHom (ModuleCat.Hom.hom ((inhomogeneousCochains A).d 2 3)) ≫ (threeCochainsLequiv A).toModuleIso.hom
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A)) = 0

Tactic:
simp only [(Iso.eq_inv_comp _).2 h2, (Iso.eq_inv_comp _).2 h1, ModuleCat.ofHom_hom,
  ModuleCat.hom_ofHom, Category.assoc, Iso.hom_inv_id_assoc, HomologicalComplex.d_comp_d_assoc,
  zero_comp, comp_zero, ModuleCat.hom_zero]

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
h1 :
  ModuleCat.ofHom (dOne A ∘ₗ ↑(oneCochainsLequiv A)) =
    ModuleCat.ofHom (↑(twoCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2))
h2 :
  ModuleCat.ofHom (dTwo A ∘ₗ ↑(twoCochainsLequiv A)) =
    ModuleCat.ofHom (↑(threeCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 2 3))
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A)) = 0

Tactic:
simp only [ModuleCat.ofHom_comp, ModuleCat.ofHom_comp, ← LinearEquiv.toModuleIso_hom] at h1 h2

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
h1 :
  (oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (dOne A) =
    ModuleCat.ofHom (ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2)) ≫ (twoCochainsLequiv A).toModuleIso.hom
h2 :
  (twoCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (dTwo A) =
    ModuleCat.ofHom (ModuleCat.Hom.hom ((inhomogeneousCochains A).d 2 3)) ≫ (threeCochainsLequiv A).toModuleIso.hom
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A)) = 0

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A)) = 0

Tactic:
have h1 := congr_arg ModuleCat.ofHom (dOne_comp_eq A)

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
h1 :
  ModuleCat.ofHom (dOne A ∘ₗ ↑(oneCochainsLequiv A)) =
    ModuleCat.ofHom (↑(twoCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2))
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A)) = 0