awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
x : Fin n → G
hf :
  ∀ (x_1 : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (a : Fin n → H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f n) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X n) : Type u))
                x_1 :
              (↑((inhomogeneousChains B).X n) : Type u)) :
            (a : Fin n → H) → (↑B : Type u))
          a :
        (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle ((⇑f : (a : G) → H) ∘ x) ∘ₗ (Hom.hom φ).toLinearMap)) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X n) : Type u))
                x_1 :
              (↑((inhomogeneousChains B).X n) : Type u)) :
            (a : Fin n → H) → (↑B : Type u))
          a :
        (↑B : Type u))
⊢ ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f n =
    ModuleCat.ofHom (lsingle ((⇑f : (a : G) → H) ∘ x) ∘ₗ (Hom.hom φ).toLinearMap)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
x : Fin n → G
x_1 : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
a : Fin n → H
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f n) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X n) : Type u))
              x_1 :
            (↑((inhomogeneousChains B).X n) : Type u)) :
          (a : Fin n → H) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle ((⇑f : (a : G) → H) ∘ x) ∘ₗ (Hom.hom φ).toLinearMap)) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X n) : Type u))
              x_1 :
            (↑((inhomogeneousChains B).X n) : Type u)) :
          (a : Fin n → H) → (↑B : Type u))
        a :
      (↑B : Type u))

Tactic:
simp [chainsMap_f]

Premises used: groupHomology.chainsMap_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
x : Fin n → G
a : (↑A : Type u)
⊢ Eq (α := (↑((inhomogeneousChains B).X n) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((chainsMap f φ).f n) :
          (a : (↑((inhomogeneousChains A).X n) : Type u)) → (↑((inhomogeneousChains B).X n) : Type u))
        (single x a) :
      (↑((inhomogeneousChains B).X n) : Type u))
    (single ((⇑f : (a : G) → H) ∘ x) ((Hom.hom φ : (a : (↑A : Type u)) → (↑(res f B) : Type u)) a) :
      (Fin n → H) →₀ (↑(res f B) : Type u))

Tactic:
simp [chainsMap_f]

Premises used: groupHomology.chainsMap_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ chainsMap (MonoidHom.id G) (𝟙 A) = 𝟙 (inhomogeneousChains A)

Tactic:
HomologicalComplex.hom_ext _ _ fun _ => ModuleCat.hom_ext <| lhom_ext' fun _ =>
    ModuleCat.hom_ext_iff.1 <| lsingle_comp_chainsMap_f (k := k) (MonoidHom.id G) ..

Premises used: HomologicalComplex.hom_ext, Finsupp.lhom_ext', CategoryTheory.CategoryStruct.id, ModuleCat.hom_ext_iff, groupHomology.lsingle_comp_chainsMap_f, MonoidHom.id, Iff.mp, ModuleCat.hom_ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
i : ℕ
φ : A ⟶ B
⊢ ModuleCat.Hom.hom (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) φ) i) =
    mapRange.linearMap (Hom.hom φ).toLinearMap

Tactic:
lhom_ext fun _ _ => ?_

Premises used: Finsupp.lhom_ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
i : ℕ
φ : A ⟶ B
refine :
  ∀ (x : Fin i → G) (x_1 : (↑A : Type u)),
    Eq (α := (↑((inhomogeneousChains B).X i) : Type u))
      ((ModuleCat.Hom.hom (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) φ) i) :
            (a : (Fin i → G) →₀ (↑A : Type u)) → (↑((inhomogeneousChains B).X i) : Type u))
          (single x x_1) :
        (↑((inhomogeneousChains B).X i) : Type u))
      ((mapRange.linearMap (Hom.hom φ).toLinearMap :
            (a : (Fin i → G) →₀ (↑A : Type u)) → (↑((inhomogeneousChains B).X i) : Type u))
          (single x x_1) :
        (↑((inhomogeneousChains B).X i) : Type u))
⊢ ModuleCat.Hom.hom (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) φ) i) =
    mapRange.linearMap (Hom.hom φ).toLinearMap

Tactic:
refine lhom_ext fun _ _ => ?_

Premises used: Finsupp.lhom_ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
i : ℕ
φ : A ⟶ B
x : Fin i → G
x_1 : (↑A : Type u)
⊢ Eq (α := (↑((inhomogeneousChains B).X i) : Type u))
    ((ModuleCat.Hom.hom (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) φ) i) :
          (a : (Fin i → G) →₀ (↑A : Type u)) → (↑((inhomogeneousChains B).X i) : Type u))
        (single x x_1) :
      (↑((inhomogeneousChains B).X i) : Type u))
    ((mapRange.linearMap (Hom.hom φ).toLinearMap :
          (a : (Fin i → G) →₀ (↑A : Type u)) → (↑((inhomogeneousChains B).X i) : Type u))
        (single x x_1) :
      (↑((inhomogeneousChains B).X i) : Type u))

Tactic:
simp [chainsMap_f, MonoidHom.coe_id]

Premises used: MonoidHom.coe_id, groupHomology.chainsMap_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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 G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
h :
  ∀ (i : ℕ) (g_1 : Fin i → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (a : Fin i → K),
    Eq (α := (↑C : Type u))
      ((((ModuleCat.Hom.hom
                    (ModuleCat.ofHom (lsingle g_1) ≫
                      (chainsMap (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).f i) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains C).X i) : Type u))
                x :
              (↑((inhomogeneousChains C).X i) : Type u)) :
            (a : Fin i → K) → (↑C : Type u))
          a :
        (↑C : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g_1) ≫ (chainsMap f φ ≫ chainsMap g ψ).f i) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains C).X i) : Type u))
                x :
              (↑((inhomogeneousChains C).X i) : Type u)) :
            (a : Fin i → K) → (↑C : Type u))
          a :
        (↑C : Type u))
⊢ chainsMap (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) = chainsMap f φ ≫ chainsMap g ψ

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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 G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
i : ℕ
g_1 : Fin i → G
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
a : Fin i → K
⊢ Eq (α := (↑C : Type u))
    ((((ModuleCat.Hom.hom
                  (ModuleCat.ofHom (lsingle g_1) ≫
                    (chainsMap (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).f i) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains C).X i) : Type u))
              x :
            (↑((inhomogeneousChains C).X i) : Type u)) :
          (a : Fin i → K) → (↑C : Type u))
        a :
      (↑C : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g_1) ≫ (chainsMap f φ ≫ chainsMap g ψ).f i) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains C).X i) : Type u))
              x :
            (↑((inhomogeneousChains C).X i) : Type u)) :
          (a : Fin i → K) → (↑C : Type u))
        a :
      (↑C : Type u))

Tactic:
simp [chainsMap_f, Function.comp_assoc]

Premises used: Function.comp_assoc, groupHomology.chainsMap_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
⊢ chainsMap (MonoidHom.id G) (φ ≫ ψ) =
    CategoryStruct.comp (Y := inhomogeneousChains B) (chainsMap (MonoidHom.id G) φ) (chainsMap (MonoidHom.id G) ψ)

Tactic:
chainsMap_comp (MonoidHom.id G) (MonoidHom.id G) _ _

Premises used: SemilinearMapClass.semilinearMap, groupHomology.chainsMap_comp, MonoidHom.id
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
h :
  ∀ (i : ℕ) (g : Fin i → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (a : Fin i → H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ HomologicalComplex.Hom.f (chainsMap f 0) i) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X i) : Type u))
                x :
              (↑((inhomogeneousChains B).X i) : Type u)) :
            (a : Fin i → H) → (↑B : Type u))
          a :
        (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ HomologicalComplex.Hom.f 0 i) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X i) : Type u))
                x :
              (↑((inhomogeneousChains B).X i) : Type u)) :
            (a : Fin i → H) → (↑B : Type u))
          a :
        (↑B : Type u))
⊢ Eq (α := inhomogeneousChains A ⟶ inhomogeneousChains B) (chainsMap f 0) 0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
i : ℕ
g : Fin i → G
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
a : Fin i → H
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ HomologicalComplex.Hom.f (chainsMap f 0) i) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X i) : Type u))
              x :
            (↑((inhomogeneousChains B).X i) : Type u)) :
          (a : Fin i → H) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ HomologicalComplex.Hom.f 0 i) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X i) : Type u))
              x :
            (↑((inhomogeneousChains B).X i) : Type u)) :
          (a : Fin i → H) → (↑B : Type u))
        a :
      (↑B : Type u))

Tactic:
simp [chainsMap_f, LinearMap.zero_apply (M₂ := B)]

Premises used: LinearMap.zero_apply, groupHomology.chainsMap_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
hf : Function.Injective (α := G) (β := H) (⇑f : (a : G) → H)
inst_3 : Mono φ
i : ℕ
⊢ Mono ((chainsMap f φ).f i)

Tactic:
simpa [ModuleCat.mono_iff_injective] using
    (mapRange_injective φ.hom (map_zero _) <| (Rep.mono_iff_injective φ).1
    inferInstance).comp (mapDomain_injective hf.comp_left)

Premises used: inferInstance, map_zero, ModuleCat.mono_iff_injective, Finsupp.mapRange_injective, Function.Injective.comp, Rep.Hom.hom, Iff.mp, Function.Injective.comp_left, DFunLike.coe, Rep.mono_iff_injective, Finsupp.mapDomain_injective
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k G
B_1 : Rep k H
f : G →* H
φ_1 : Quiver.Hom.{?u.186179, max u (?u.186179 + 1)} A_1 (res f B_1)
n : ℕ
A B : Rep k G
φ : A ⟶ B
inst_3 : Mono φ
i : ℕ
⊢ Mono (C := ModuleCat k) (X := (inhomogeneousChains A).X i) (Y := (inhomogeneousChains B).X i)
    (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) φ) i)

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

Premises used: groupHomology.chainsMap_f_map_mono, MonoidHom.id
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
hf : Function.Surjective (α := G) (β := H) (⇑f : (a : G) → H)
inst_3 : Epi φ
i : ℕ
⊢ Epi ((chainsMap f φ).f i)

Tactic:
simpa [ModuleCat.epi_iff_surjective] using
    (mapRange_surjective φ.hom (map_zero _) ((Rep.epi_iff_surjective φ).1 inferInstance)).comp
    (mapDomain_surjective hf.comp_left)

Premises used: Function.Surjective.comp_left, Finsupp.mapDomain_surjective, ModuleCat.epi_iff_surjective, inferInstance, map_zero, Finsupp.mapRange_surjective, Rep.Hom.hom, Iff.mp, Function.Surjective.comp, Rep.epi_iff_surjective, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k G
B_1 : Rep k H
f : G →* H
φ_1 : Quiver.Hom.{?u.197789, max u (?u.197789 + 1)} A_1 (res f B_1)
n : ℕ
A B : Rep k G
φ : A ⟶ B
inst_3 : Epi φ
i : ℕ
⊢ Epi (C := ModuleCat k) (X := (inhomogeneousChains A).X i) (Y := (inhomogeneousChains B).X i)
    (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) φ) i)

Tactic:
chainsMap_f_map_epi _ _ (fun x => ⟨x, rfl⟩) _

Premises used: groupHomology.chainsMap_f_map_epi, Exists.intro
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ cyclesMap (MonoidHom.id G) (𝟙 A) n = 𝟙 (cycles A n)

Tactic:
simp [cyclesMap]

Premises used: groupHomology.cyclesMap
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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 G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
n : ℕ
⊢ cyclesMap (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) n = cyclesMap f φ n ≫ cyclesMap g ψ n

Tactic:
simp [cyclesMap, ← HomologicalComplex.cyclesMap_comp, ← chainsMap_comp]

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

Tactic:
simp [cyclesMap, chainsMap_id_comp, HomologicalComplex.cyclesMap_comp]

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

Tactic:
simp [map, cyclesMap]

Premises used: groupHomology.cyclesMap, groupHomology.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ map (MonoidHom.id G) (𝟙 A) n = 𝟙 (groupHomology A n)

Tactic:
simp [map, groupHomology]

Premises used: groupHomology, groupHomology.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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 G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
n : ℕ
⊢ map (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) n = map f φ n ≫ map g ψ n

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

Premises used: HomologicalComplex.homologyMap_comp, groupHomology.chainsMap_comp, groupHomology.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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 (chainsMap (MonoidHom.id G) (φ ≫ ψ)) n =
    CategoryStruct.comp (Y := groupHomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
rw₁ :
  Eq (α := groupHomology A n ⟶ groupHomology C n)
    (HomologicalComplex.homologyMap
      (CategoryStruct.comp (Y := inhomogeneousChains B) (chainsMap (MonoidHom.id G) φ) (chainsMap (MonoidHom.id G) ψ))
      n)
    (CategoryStruct.comp (Y := groupHomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n))
rw₂ rw₃ :
  Eq (α := groupHomology A n ⟶ groupHomology C n)
    (CategoryStruct.comp (Y := HomologicalComplex.homology (inhomogeneousChains B) n)
      (HomologicalComplex.homologyMap (chainsMap (MonoidHom.id G) φ) n)
      (HomologicalComplex.homologyMap (chainsMap (MonoidHom.id G) ψ) n))
    (CategoryStruct.comp (Y := groupHomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n))
⊢ map (MonoidHom.id G) (φ ≫ ψ) n =
    CategoryStruct.comp (Y := groupHomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)

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

Premises used: HomologicalComplex.homologyMap_comp, groupHomology.chainsMap_id_comp, groupHomology.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
h :
  ∀ (g : Fin 0 → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑B : Type u)) : Type u))
      ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom) :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑B : Type u)) : Type u))
      ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑B : Type u)) : Type u))
⊢ (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom = (chainsIso₀ A).hom ≫ Hom.toModuleCatHom φ

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
g : Fin 0 → G
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))

Tactic:
simp [chainsMap_f, Unique.eq_default (α := Fin 0 → G), Unique.eq_default (α := Fin 0 → H),
    chainsIso₀]

Premises used: Unique.eq_default, groupHomology.chainsIso₀, groupHomology.chainsMap_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
h :
  ∀ (x : Fin 1 → G) (x_1 : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (a : H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
                x_1 :
              (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u)) :
            (a : H) → (↑B : Type u))
          a :
        (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle x) ≫ (chainsIso₁ A).hom ≫ chainsMap₁ f φ) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
                x_1 :
              (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u)) :
            (a : H) → (↑B : Type u))
          a :
        (↑B : Type u))
⊢ (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom = (chainsIso₁ A).hom ≫ chainsMap₁ f φ

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
x : Fin 1 → G
x_1 : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
a : H
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
              x_1 :
            (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u)) :
          (a : H) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle x) ≫ (chainsIso₁ A).hom ≫ chainsMap₁ f φ) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
              x_1 :
            (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u)) :
          (a : H) → (↑B : Type u))
        a :
      (↑B : Type u))

Tactic:
simp [chainsMap_f, chainsIso₁]

Premises used: groupHomology.chainsIso₁, groupHomology.chainsMap_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
h :
  ∀ (g : Fin 2 → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (a : H × H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsMap f φ).f 2 ≫ (chainsIso₂ B).hom) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) →
                    (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
                x :
              (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u)) :
            (a : H × H) → (↑B : Type u))
          a :
        (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsIso₂ A).hom ≫ chainsMap₂ f φ) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) →
                    (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
                x :
              (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u)) :
            (a : H × H) → (↑B : Type u))
          a :
        (↑B : Type u))
⊢ (chainsMap f φ).f 2 ≫ (chainsIso₂ B).hom = (chainsIso₂ A).hom ≫ chainsMap₂ f φ

Tactic:
ext