-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc]
lemma cochainsMap_f_3_comp_threeCochainsLequiv :
    (cochainsMap f φ).f 3 ≫ (threeCochainsLequiv B).toModuleIso.hom =
      (threeCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fThree f φ)

Proof state:
case hf.h.h.h.e_6.h.e_a.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x✝ : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
x : Fin 3
⊢ (fun x => ⇑f ∘ x)
      (((Fin.consEquiv fun a => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x => G))).symm g) x =
    ((Fin.consEquiv fun a => H).symm.trans ((Equiv.refl H).prodCongr (piFinTwoEquiv fun x => H))).symm
      (Prod.map (⇑f) (Prod.map ⇑f ⇑f) g) x

Tactic:
fin_cases x <;> rfl

Result:
no goals

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ (cochainsMap f φ).f 3 ≫ (threeCochainsLequiv B).toModuleIso.hom =
    (threeCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fThree f φ)

Tactic:
ext x g

Result:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 3 ≫ (threeCochainsLequiv B).toModuleIso.hom)) x g =
    (ModuleCat.Hom.hom ((threeCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fThree f φ))) x g

Proof state:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 3 ≫ (threeCochainsLequiv B).toModuleIso.hom)) x g =
    (ModuleCat.Hom.hom ((threeCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fThree f φ))) x g

Tactic:
show φ.hom (x _) = φ.hom (x _)

Result:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
⊢ (ConcreteCategory.hom φ.hom)
      (x
        ((fun x => ⇑f ∘ x)
          (((Fin.consEquiv fun a => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x => G))).symm g))) =
    (ConcreteCategory.hom φ.hom)
      (x
        (((Fin.consEquiv fun a => H).symm.trans ((Equiv.refl H).prodCongr (piFinTwoEquiv fun x => H))).symm
          (Prod.map (⇑f) (Prod.map ⇑f ⇑f) g)))

Proof state:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
⊢ (ConcreteCategory.hom φ.hom)
      (x
        ((fun x => ⇑f ∘ x)
          (((Fin.consEquiv fun a => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x => G))).symm g))) =
    (ConcreteCategory.hom φ.hom)
      (x
        (((Fin.consEquiv fun a => H).symm.trans ((Equiv.refl H).prodCongr (piFinTwoEquiv fun x => H))).symm
          (Prod.map (⇑f) (Prod.map ⇑f ⇑f) g)))

Tactic:
rcongr x

Result:
case hf.h.h.h.e_6.h.e_a.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x✝ : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
x : Fin 3
⊢ (fun x => ⇑f ∘ x)
      (((Fin.consEquiv fun a => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x => G))).symm g) x =
    ((Fin.consEquiv fun a => H).symm.trans ((Equiv.refl H).prodCongr (piFinTwoEquiv fun x => H))).symm
      (Prod.map (⇑f) (Prod.map ⇑f ⇑f) g) x