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 : G
x : (↑A : Type u)
a_1 : H
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom (Hom.τ₂ (mapShortComplexH1 f 0)) ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                          X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                    X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))
    (((((ModuleCat.Hom.hom (Hom.τ₂ 0) :
                    (↑{ X₁ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G →₀ (↑A : Type u)),
                              X₃ := ModuleCat.of k (↑A : Type u), f := d₂₁ A, g := d₁₀ A, zero := ⋯ :
                              ShortComplex (ModuleCat k) }.X₂ :
                        Type u) →ₗ[k]
                      (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                              X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ :
                              ShortComplex (ModuleCat k) }.X₂ :
                        Type u)) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                          X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                    X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))

Tactic:
simp
-- 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
refine_2 :
  Eq (α := Quiver.Hom (V := ModuleCat k) (ModuleCat.of k (G →₀ (↑A : Type u))) (ModuleCat.of k (H →₀ (↑B : Type u))))
    (Hom.τ₂ (mapShortComplexH1 f 0)) (Hom.τ₂ 0)
refine_2₁ :
  ∀ (a : G) (x : (↑A : Type u)) (a_1 : H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₂ (mapShortComplexH1 f 0)) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
      (((((ModuleCat.Hom.hom (Hom.τ₂ 0) :
                      (↑{ X₁ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G →₀ (↑A : Type u)),
                                X₃ := ModuleCat.of k (↑A : Type u), f := d₂₁ A, g := d₁₀ A, zero := ⋯ :
                                ShortComplex (ModuleCat k) }.X₂ :
                          Type u) →ₗ[k]
                        (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                                X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ :
                                ShortComplex (ModuleCat k) }.X₂ :
                          Type u)) ∘ₗ
                    lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
⊢ Eq (α := (shortComplexH1 A).X₂ ⟶ (shortComplexH1 B).X₂) (Hom.τ₂ (mapShortComplexH1 f 0)) (Hom.τ₂ 0)

Tactic:
{ simp only [shortComplexH1]
    ext
    simp }

Premises used: groupHomology.shortComplexH1
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
h₁ :
  ∀ (x : (↑(shortComplexH1 A).X₁ : Type u)),
    Eq (α := (↑(shortComplexH1 A).X₁ : Type u))
      ((ModuleCat.Hom.hom (Hom.τ₁ (mapShortComplexH1 (MonoidHom.id G) (𝟙 A))) :
            (a : (↑(shortComplexH1 A).X₁ : Type u)) → (↑(shortComplexH1 A).X₁ : Type u))
          x :
        (↑(shortComplexH1 A).X₁ : Type u))
      ((ModuleCat.Hom.hom (Hom.τ₁ (𝟙 (shortComplexH1 A))) :
            (a : (↑(shortComplexH1 A).X₁ : Type u)) → (↑(shortComplexH1 A).X₁ : Type u))
          x :
        (↑(shortComplexH1 A).X₁ : Type u))
h₂ :
  ∀ (x : (↑(shortComplexH1 A).X₂ : Type u)),
    Eq (α := (↑(shortComplexH1 A).X₂ : Type u))
      ((ModuleCat.Hom.hom (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (𝟙 A))) :
            (a : (↑(shortComplexH1 A).X₂ : Type u)) → (↑(shortComplexH1 A).X₂ : Type u))
          x :
        (↑(shortComplexH1 A).X₂ : Type u))
      ((ModuleCat.Hom.hom (Hom.τ₂ (𝟙 (shortComplexH1 A))) :
            (a : (↑(shortComplexH1 A).X₂ : Type u)) → (↑(shortComplexH1 A).X₂ : Type u))
          x :
        (↑(shortComplexH1 A).X₂ : Type u))
h₃ :
  ∀ (x : (↑(shortComplexH1 A).X₃ : Type u)),
    Eq (α := (↑(shortComplexH1 A).X₃ : Type u))
      ((ModuleCat.Hom.hom (Hom.τ₃ (mapShortComplexH1 (MonoidHom.id G) (𝟙 A))) :
            (a : (↑(shortComplexH1 A).X₃ : Type u)) → (↑(shortComplexH1 A).X₃ : Type u))
          x :
        (↑(shortComplexH1 A).X₃ : Type u))
      ((ModuleCat.Hom.hom (Hom.τ₃ (𝟙 (shortComplexH1 A))) :
            (a : (↑(shortComplexH1 A).X₃ : Type u)) → (↑(shortComplexH1 A).X₃ : Type u))
          x :
        (↑(shortComplexH1 A).X₃ : Type u))
⊢ mapShortComplexH1 (MonoidHom.id G) (𝟙 A) = 𝟙 (shortComplexH1 A)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(shortComplexH1 A).X₁ : Type u)
⊢ Eq (α := (↑(shortComplexH1 A).X₁ : Type u))
    ((ModuleCat.Hom.hom (Hom.τ₁ (mapShortComplexH1 (MonoidHom.id G) (𝟙 A))) :
          (a : (↑(shortComplexH1 A).X₁ : Type u)) → (↑(shortComplexH1 A).X₁ : Type u))
        x :
      (↑(shortComplexH1 A).X₁ : Type u))
    ((ModuleCat.Hom.hom (Hom.τ₁ (𝟙 (shortComplexH1 A))) :
          (a : (↑(shortComplexH1 A).X₁ : Type u)) → (↑(shortComplexH1 A).X₁ : Type u))
        x :
      (↑(shortComplexH1 A).X₁ : Type u))

Tactic:
simp [shortComplexH1]

Premises used: groupHomology.shortComplexH1
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(shortComplexH1 A).X₂ : Type u)
⊢ Eq (α := (↑(shortComplexH1 A).X₂ : Type u))
    ((ModuleCat.Hom.hom (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (𝟙 A))) :
          (a : (↑(shortComplexH1 A).X₂ : Type u)) → (↑(shortComplexH1 A).X₂ : Type u))
        x :
      (↑(shortComplexH1 A).X₂ : Type u))
    ((ModuleCat.Hom.hom (Hom.τ₂ (𝟙 (shortComplexH1 A))) :
          (a : (↑(shortComplexH1 A).X₂ : Type u)) → (↑(shortComplexH1 A).X₂ : Type u))
        x :
      (↑(shortComplexH1 A).X₂ : Type u))

Tactic:
simp [shortComplexH1]

Premises used: groupHomology.shortComplexH1
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(shortComplexH1 A).X₃ : Type u)
⊢ Eq (α := (↑(shortComplexH1 A).X₃ : Type u))
    ((ModuleCat.Hom.hom (Hom.τ₃ (mapShortComplexH1 (MonoidHom.id G) (𝟙 A))) :
          (a : (↑(shortComplexH1 A).X₃ : Type u)) → (↑(shortComplexH1 A).X₃ : Type u))
        x :
      (↑(shortComplexH1 A).X₃ : Type u))
    ((ModuleCat.Hom.hom (Hom.τ₃ (𝟙 (shortComplexH1 A))) :
          (a : (↑(shortComplexH1 A).X₃ : Type u)) → (↑(shortComplexH1 A).X₃ : Type u))
        x :
      (↑(shortComplexH1 A).X₃ : Type u))

Tactic:
simp [shortComplexH1]

Premises used: groupHomology.shortComplexH1
-- 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
⊢ mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ

Tactic:
ShortComplex.hom_ext _ _ ?_ ?_ rfl

Premises used: CategoryTheory.ShortComplex.hom_ext, rfl
-- 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
refine_1 :
  (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁
refine_2 :
  (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂
⊢ mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ

Tactic:
refine ShortComplex.hom_ext _ _ ?_ ?_ rfl

Premises used: CategoryTheory.ShortComplex.hom_ext, rfl
-- 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
refine_1 :
  Hom.τ₁
      (mapShortComplexH1 (g.comp f)
        (φ ≫
          ofHom
            {
              toLinearMap :=
                (↑(Hom.hom ψ) :
                  [inst_4 : FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u) (↑C : Type u)] →
                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k) (↑B : Type u)
                          (↑C : Type u)] →
                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
              isIntertwining' := ⋯ })) =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁

Tactic:
simp only [shortComplexH1]

Premises used: groupHomology.shortComplexH1
-- 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
a : G × G
x : (↑A : Type u)
a_1 : K × K
⊢ Eq (α := (↑C : Type u))
    ((((ModuleCat.Hom.hom
                    (Hom.τ₁
                      (mapShortComplexH1 (g.comp f)
                        (φ ≫
                          ofHom
                            {
                              toLinearMap :=
                                (↑(Hom.hom ψ) :
                                  [inst_4 :
                                      FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u)
                                        (↑C : Type u)] →
                                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k)
                                          (↑B : Type u) (↑C : Type u)] →
                                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
                              isIntertwining' := ⋯ :
                              IntertwiningMap (MonoidHom.comp B.ρ f) ((MonoidHom.comp C.ρ g).comp f) }))) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (↑C : Type u), f := d₂₁ C, g := d₁₀ C, zero := ⋯ }.X₁ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (↑C : Type u), f := d₂₁ C, g := d₁₀ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : K × K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))
    ((((ModuleCat.Hom.hom (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁ ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (↑C : Type u), f := d₂₁ C, g := d₁₀ C, zero := ⋯ }.X₁ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (↑C : Type u), f := d₂₁ C, g := d₁₀ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : K × K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))

Tactic:
simp [Prod.map]

Premises used: Prod.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
refine_2 :
  Hom.τ₂
      (mapShortComplexH1 (g.comp f)
        (φ ≫
          ofHom
            {
              toLinearMap :=
                (↑(Hom.hom ψ) :
                  [inst_4 : FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u) (↑C : Type u)] →
                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k) (↑B : Type u)
                          (↑C : Type u)] →
                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
              isIntertwining' := ⋯ })) =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂

Tactic:
simp only [shortComplexH1]

Premises used: groupHomology.shortComplexH1
-- 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
a : G
x : (↑A : Type u)
a_1 : K
⊢ Eq (α := (↑C : Type u))
    ((((ModuleCat.Hom.hom
                    (Hom.τ₂
                      (mapShortComplexH1 (g.comp f)
                        (φ ≫
                          ofHom
                            {
                              toLinearMap :=
                                (↑(Hom.hom ψ) :
                                  [inst_4 :
                                      FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u)
                                        (↑C : Type u)] →
                                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k)
                                          (↑B : Type u) (↑C : Type u)] →
                                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
                              isIntertwining' := ⋯ :
                              IntertwiningMap (MonoidHom.comp B.ρ f) ((MonoidHom.comp C.ρ g).comp f) }))) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (↑C : Type u), f := d₂₁ C, g := d₁₀ C, zero := ⋯ }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (↑C : Type u), f := d₂₁ C, g := d₁₀ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))
    ((((ModuleCat.Hom.hom (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂ ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (↑C : Type u), f := d₂₁ C, g := d₁₀ C, zero := ⋯ }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (↑C : Type u), f := d₂₁ C, g := d₁₀ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))

Tactic:
simp [Prod.map]

Premises used: Prod.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
⊢ mapShortComplexH1 (MonoidHom.id G) (φ ≫ ψ) =
    CategoryStruct.comp (Y := shortComplexH1 B) (mapShortComplexH1 (MonoidHom.id G) φ)
      (mapShortComplexH1 (MonoidHom.id G) ψ)

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

Premises used: groupHomology.mapShortComplexH1_comp, SemilinearMapClass.semilinearMap, 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
n : ℕ
x : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)
h : x ∈ cycles₁ A
⊢ Eq (α := (↑(shortComplexH1 B).X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((mapShortComplexH1 f φ).τ₂ ≫ (shortComplexH1 B).g) :
          (a : (↑(shortComplexH1 A).X₂ : Type u)) → (↑(shortComplexH1 B).X₃ : Type u))
        x :
      (↑(shortComplexH1 B).X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH1 A).g ≫ (mapShortComplexH1 f φ).τ₃) :
          (a : (↑(shortComplexH1 A).X₂ : Type u)) → (↑(shortComplexH1 B).X₃ : Type u))
        x :
      (↑(shortComplexH1 B).X₃ : Type u))

Tactic:
have := congr($((mapShortComplexH1 f φ).comm₂₃) 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
n : ℕ
x : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)
h : x ∈ cycles₁ A
this :
  Eq (α := (↑(shortComplexH1 B).X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((mapShortComplexH1 f φ).τ₂ ≫ (shortComplexH1 B).g) :
          (a : (↑(shortComplexH1 A).X₂ : Type u)) → (↑(shortComplexH1 B).X₃ : Type u))
        x :
      (↑(shortComplexH1 B).X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH1 A).g ≫ (mapShortComplexH1 f φ).τ₃) :
          (a : (↑(shortComplexH1 A).X₂ : Type u)) → (↑(shortComplexH1 B).X₃ : Type u))
        x :
      (↑(shortComplexH1 B).X₃ : Type u))
⊢ Membership.mem (α := (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u)) (cycles₁ B)
    ((ModuleCat.Hom.hom (chainsMap₁ f φ) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))

Tactic:
simp_all [cycles₁, shortComplexH1]

Premises used: groupHomology.cycles₁, groupHomology.shortComplexH1
-- 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
⊢ ModuleCat.Hom.hom (mapCycles₁ f φ) = (ModuleCat.Hom.hom (chainsMap₁ f φ)).restrict ⋯

Tactic:
rfl

Premises used: Set.Mem, LinearMap.restrict, groupHomology.cycles₁, LinearMap.codRestrict, rfl
-- 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
rw :
  mapCycles₁ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    cyclesMap' (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ) (shortComplexH1 A).moduleCatLeftHomologyData
      (shortComplexH1 C).moduleCatLeftHomologyData
rw₁ rw₂ :
  mapCycles₁ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    cyclesMap' (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ))
      (shortComplexH1 A).moduleCatLeftHomologyData (shortComplexH1 C).moduleCatLeftHomologyData
⊢ mapCycles₁ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) = mapCycles₁ f φ ≫ mapCycles₁ g ψ

Tactic:
rw [← cyclesMap'_comp, ← mapShortComplexH1_comp]

Premises used: CategoryTheory.ShortComplex.cyclesMap'_comp, groupHomology.mapShortComplexH1_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
⊢ mapCycles₁ (MonoidHom.id G) (φ ≫ ψ) =
    CategoryStruct.comp (Y := ModuleCat.of k ↥(cycles₁ B)) (mapCycles₁ (MonoidHom.id G) φ)
      (mapCycles₁ (MonoidHom.id G) ψ)

Tactic:
mapCycles₁_comp (MonoidHom.id G) (MonoidHom.id G) _ _

Premises used: groupHomology.mapCycles₁_comp, SemilinearMapClass.semilinearMap, 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
⊢ mapCycles₁ f φ ≫ (shortComplexH1 B).moduleCatLeftHomologyData.i =
    (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ chainsMap₁ f φ

Tactic:
simp
-- 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 : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)
⊢ Eq (α := H →₀ (↑B : Type u))
    ((↑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (mapCycles₁ f φ) :
              (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ B)) : Type u))
            x) :
        H →₀ (↑B : Type u)) :
      H →₀ (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsMap₁ f φ) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
        (↑x : G →₀ (↑A : Type u)) :
      (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))

Tactic:
rfl

Premises used: Finsupp.onFinset, Finsupp.mapRange, rfl