awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
hf : Function.Surjective (α := G) (β := H) (⇑f : (a : G) → H)
inst_3 : Mono φ
i : ℕ
⊢ Mono ((cochainsMap f φ).f i)

Tactic:
simpa [ModuleCat.mono_iff_injective] using
    ((Rep.mono_iff_injective φ).1 inferInstance).comp_left.comp <|
    LinearMap.funLeft_injective_of_surjective k A _ hf.comp_left

Premises used: Function.Surjective.comp_left, Rep.V, inferInstance, ModuleCat.mono_iff_injective, LinearMap.funLeft_injective_of_surjective, Function.Injective.comp, Iff.mp, Function.Injective.comp_left, Rep.mono_iff_injective
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B_1 : Rep k G
f : G →* H
φ_1 : Quiver.Hom.{?u.56044, max (?u.56044 + 1) u} (res f A_1) B_1
n : ℕ
A B : Rep k G
φ : A ⟶ B
inst_3 : Mono φ
i : ℕ
⊢ Mono (C := ModuleCat k) (X := (inhomogeneousCochains A).X i) (Y := (inhomogeneousCochains B).X i)
    (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) φ) i)

Tactic:
cochainsMap_f_map_mono (MonoidHom.id G) φ (fun x => ⟨x, rfl⟩) i

Premises used: MonoidHom.id, groupCohomology.cochainsMap_f_map_mono, Exists.intro, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
hf : Function.Injective (α := G) (β := H) (⇑f : (a : G) → H)
inst_3 : Epi φ
i : ℕ
⊢ Epi ((cochainsMap f φ).f i)

Tactic:
simpa [ModuleCat.epi_iff_surjective] using
    ((Rep.epi_iff_surjective φ).1 inferInstance).comp_left.comp <|
    LinearMap.funLeft_surjective_of_injective k A _ hf.comp_left

Premises used: Function.Surjective.comp_left, Rep.V, LinearMap.funLeft_surjective_of_injective, ModuleCat.epi_iff_surjective, inferInstance, Iff.mp, Function.Surjective.comp, Function.Injective.comp_left, Rep.epi_iff_surjective
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B_1 : Rep k G
f : G →* H
φ_1 : Quiver.Hom.{?u.62017, max (?u.62017 + 1) u} (res f A_1) B_1
n : ℕ
A B : Rep k G
φ : A ⟶ B
inst_3 : Epi φ
i : ℕ
⊢ Epi (C := ModuleCat k) (X := (inhomogeneousCochains A).X i) (Y := (inhomogeneousCochains B).X i)
    (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) φ) i)

Tactic:
cochainsMap_f_map_epi (MonoidHom.id G) φ (fun _ _ h => h) i

Premises used: groupCohomology.cochainsMap_f_map_epi, MonoidHom.id
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
B : Rep k G
n : ℕ
⊢ cocyclesMap (MonoidHom.id G) (𝟙 B) n = 𝟙 (cocycles B n)

Tactic:
HomologicalComplex.cyclesMap_id _ _

Premises used: HomologicalComplex.id, HomologicalComplex.cyclesMap_id, groupCohomology.cochainsMap
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k K
B : Rep k H
C : Rep k G
f : H →* K
g : G →* H
φ : res f A ⟶ B
ψ : res g B ⟶ C
n : ℕ
⊢ cocyclesMap (f.comp g) (CategoryTheory.Functor.map (resFunctor g) φ ≫ ψ) n = cocyclesMap f φ n ≫ cocyclesMap g ψ n

Tactic:
simp [cocyclesMap, ← HomologicalComplex.cyclesMap_comp, ← cochainsMap_comp]

Premises used: groupCohomology.cochainsMap_comp, HomologicalComplex.cyclesMap_comp, groupCohomology.cocyclesMap
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ cocyclesMap (MonoidHom.id G) (φ ≫ ψ) n =
    CategoryStruct.comp (Y := cocycles B n) (cocyclesMap (MonoidHom.id G) φ n) (cocyclesMap (MonoidHom.id G) ψ n)

Tactic:
simp [cocyclesMap, cochainsMap_id_comp, HomologicalComplex.cyclesMap_comp]

Premises used: HomologicalComplex.cyclesMap_comp, groupCohomology.cochainsMap_id_comp, groupCohomology.cocyclesMap
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
⊢ π A n ≫ map f φ n = cocyclesMap f φ n ≫ π B n

Tactic:
simp [map, cocyclesMap]

Premises used: groupCohomology.map, groupCohomology.cocyclesMap
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
B : Rep k G
n : ℕ
⊢ map (MonoidHom.id G) (𝟙 B) n = 𝟙 (groupCohomology B n)

Tactic:
HomologicalComplex.homologyMap_id _ _

Premises used: groupCohomology, HomologicalComplex.id, HomologicalComplex.homologyMap_id, groupCohomology.cochainsMap
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k K
B : Rep k H
C : Rep k G
f : H →* K
g : G →* H
φ : res f A ⟶ B
ψ : res g B ⟶ C
n : ℕ
⊢ map (f.comp g) (CategoryTheory.Functor.map (resFunctor g) φ ≫ ψ) n = map f φ n ≫ map g ψ n

Tactic:
simp [map, ← HomologicalComplex.homologyMap_comp, ← cochainsMap_comp]

Premises used: groupCohomology.map, groupCohomology.cochainsMap_comp, HomologicalComplex.homologyMap_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
rw :
  HomologicalComplex.homologyMap (cochainsMap (MonoidHom.id G) (φ ≫ ψ)) n =
    CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
rw₁ :
  Eq (α := groupCohomology A n ⟶ groupCohomology C n)
    (HomologicalComplex.homologyMap
      (CategoryStruct.comp (Y := inhomogeneousCochains B) (cochainsMap (MonoidHom.id G) φ)
        (cochainsMap (MonoidHom.id G) ψ))
      n)
    (CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n))
rw₂ rw₃ :
  Eq (α := groupCohomology A n ⟶ groupCohomology C n)
    (CategoryStruct.comp (Y := HomologicalComplex.homology (inhomogeneousCochains B) n)
      (HomologicalComplex.homologyMap (cochainsMap (MonoidHom.id G) φ) n)
      (HomologicalComplex.homologyMap (cochainsMap (MonoidHom.id G) ψ) n))
    (CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n))
⊢ map (MonoidHom.id G) (φ ≫ ψ) n =
    CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)

Tactic:
rw [map, cochainsMap_id_comp, HomologicalComplex.homologyMap_comp]

Premises used: groupCohomology.map, groupCohomology.cochainsMap_id_comp, HomologicalComplex.homologyMap_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
hf :
  ∀ (x : Fin 0 → H) (x_1 : (↑A : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑B : Type u)) : Type u))
      ((ModuleCat.Hom.hom ((cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom) ∘ₗ
              LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
          x_1 :
        (↑(ModuleCat.of k (↑B : Type u)) : Type u))
      ((ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) ∘ₗ
              LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
          x_1 :
        (↑(ModuleCat.of k (↑B : Type u)) : Type u))
⊢ (cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom = (cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : Fin 0 → H
x_1 : (↑A : Type u)
hf :
  Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom
              ((ModuleCat.ofHom (LinearMap.funLeft k (↑A : Type u) fun (x : Fin 0 → G) ↦ default) ≫
                  ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin 0 → G))) ≫
                (cochainsIso₀ B).hom) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑B : Type u))
        x_1 :
      (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑B : Type u))
        x_1 :
      (↑B : Type u))
⊢ Eq (α := (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom ((cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x_1 :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x_1 :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))

Tactic:
simp only [cochainsMap_f, Unique.eq_default (f ∘ _)]

Premises used: Function.comp, Unique.eq_default, groupCohomology.cochainsMap_f, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : Fin 0 → H
x_1 : (↑A : Type u)
⊢ Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom
              ((ModuleCat.ofHom (LinearMap.funLeft k (↑A : Type u) fun (x : Fin 0 → G) ↦ default) ≫
                  ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin 0 → G))) ≫
                (cochainsIso₀ B).hom) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑B : Type u))
        x_1 :
      (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑B : Type u))
        x_1 :
      (↑B : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ (cochainsMap f φ).f 1 ≫ (cochainsIso₁ B).hom = (cochainsIso₁ A).hom ≫ cochainsMap₁ f φ

Tactic:
rfl

Premises used: Eq.mpr, uniqueElim, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
hf :
  ∀ (x : (↑((inhomogeneousCochains A).X 2) : Type u)) (g : G × G),
    Eq (α := (↑B : Type u))
      ((ModuleCat.Hom.hom ((cochainsMap f φ).f 2 ≫ (cochainsIso₂ B).hom) :
            (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G → (↑B : Type u))) : Type u))
          x g :
        (↑B : Type u))
      ((ModuleCat.Hom.hom ((cochainsIso₂ A).hom ≫ cochainsMap₂ f φ) :
            (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G → (↑B : Type u))) : Type u))
          x g :
        (↑B : Type u))
⊢ (cochainsMap f φ).f 2 ≫ (cochainsIso₂ B).hom = (cochainsIso₂ A).hom ≫ cochainsMap₂ f φ

Tactic:
ext x g
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 2) : Type u)
g : G × G
hf :
  Eq (α := (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
            (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              g))) :
      (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) :
              (a : H × H) → (i : Fin 2) → H)
            (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g))) :
      (↑B : Type u))
⊢ Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsMap f φ).f 2 ≫ (cochainsIso₂ B).hom) :
          (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₂ A).hom ≫ cochainsMap₂ f φ) :
          (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))

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

Premises used: Rep.Hom.hom, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 2) : Type u)
g : G × G
hf :
  ∀ (x : Fin 2),
    Eq (α := H)
      ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
          (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
              (a : G × G) → (i : Fin 2) → G)
            g)
          x :
        H)
      (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
          (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g) x :
        H)
⊢ Eq (α := (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
            (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              g))) :
      (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) :
              (a : H × H) → (i : Fin 2) → H)
            (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g))) :
      (↑B : Type u))

Tactic:
rcongr x
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x_1 : (↑((inhomogeneousCochains A).X 2) : Type u)
g : G × G
x : Fin 2
hf :
  Eq (α := H)
    ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
        (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
hf₁ :
  Eq (α := H)
    ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      H)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
        (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      H)
⊢ Eq (α := H)
    ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          g)
        x :
      H)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
        (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g) x :
      H)

Tactic:
fin_cases x
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 2) : Type u)
g : G × G
⊢ Eq (α := H)
    ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
        (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 2) : Type u)
g : G × G
⊢ Eq (α := H)
    ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      H)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
        (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      H)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
hf :
  ∀ (x : (↑((inhomogeneousCochains A).X 3) : Type u)) (g : G × G × G),
    Eq (α := (↑B : Type u))
      ((ModuleCat.Hom.hom ((cochainsMap f φ).f 3 ≫ (cochainsIso₃ B).hom) :
            (a : (↑((inhomogeneousCochains A).X 3) : Type u)) →
              (↑(ModuleCat.of k (G × G × G → (↑B : Type u))) : Type u))
          x g :
        (↑B : Type u))
      ((ModuleCat.Hom.hom ((cochainsIso₃ A).hom ≫ cochainsMap₃ f φ) :
            (a : (↑((inhomogeneousCochains A).X 3) : Type u)) →
              (↑(ModuleCat.of k (G × G × G → (↑B : Type u))) : Type u))
          x g :
        (↑B : Type u))
⊢ (cochainsMap f φ).f 3 ≫ (cochainsIso₃ B).hom = (cochainsIso₃ A).hom ≫ cochainsMap₃ f φ

Tactic:
ext x g
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 3) : Type u)
g : G × G × G
hf :
  Eq (α := (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
            ((Equiv.symm
                  (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                    ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
                (a : G × G × G) → (i : Fin (2 + 1)) → G)
              g))) :
      (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          ((Equiv.symm
                (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
                  ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
              (a : H × H × H) → (i : Fin (2 + 1)) → H)
            (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g))) :
      (↑B : Type u))
⊢ Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsMap f φ).f 3 ≫ (cochainsIso₃ B).hom) :
          (a : (↑((inhomogeneousCochains A).X 3) : Type u)) → (↑(ModuleCat.of k (G × G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₃ A).hom ≫ cochainsMap₃ f φ) :
          (a : (↑((inhomogeneousCochains A).X 3) : Type u)) → (↑(ModuleCat.of k (G × G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))

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

Premises used: Rep.Hom.hom, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 3) : Type u)
g : G × G × G
hf :
  ∀ (x : Fin 3),
    Eq (α := H)
      ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
          ((Equiv.symm
                (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                  ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
              (a : G × G × G) → (i : Fin (2 + 1)) → G)
            g)
          x :
        H)
      ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
                ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
            (a : H × H × H) → (i : Fin (2 + 1)) → H)
          (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g) x :
        H)
⊢ Eq (α := (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
            ((Equiv.symm
                  (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                    ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
                (a : G × G × G) → (i : Fin (2 + 1)) → G)
              g))) :
      (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          ((Equiv.symm
                (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
                  ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
              (a : H × H × H) → (i : Fin (2 + 1)) → H)
            (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g))) :
      (↑B : Type u))

Tactic:
rcongr x
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 3) : Type u)
g : G × G × G
⊢ Eq (α := H)
    ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
            (a : G × G × G) → (i : Fin (2 + 1)) → G)
          g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
    ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
              ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
          (a : H × H × H) → (i : Fin (2 + 1)) → H)
        (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)

Tactic:
rfl