awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
refine_2 :
  Hom.τ₂ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) =
    Hom.τ₂
      (𝟙
        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })
⊢ Hom.τ₂ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) = Hom.τ₂ (𝟙 (shortComplexH2 A))
have refine_2₁ : ∀ (a : G × G) (x : (↑A : Type u)) (a_1 : G × G),
  Eq (α := (↑A : Type u))
    ((((ModuleCat.Hom.hom (Hom.τ₂ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A))) ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                    X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : G × G) → (↑A : Type u))
        a_1 :
      (↑A : Type u))
    ((((ModuleCat.Hom.hom
                    (Hom.τ₂
                      (𝟙
                        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                          X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                          f := d₃₂ A, g := d₂₁ A, zero := sorry : ShortComplex (ModuleCat k) })) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                    X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : G × G) → (↑A : Type u))
        a_1 :
      (↑A : Type u))
Tactic: { simp only [shortComplexH2]
    ext
    simp }
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) =
    Hom.τ₃
      (𝟙
        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })
have refine_3 : ∀ (a : G) (x : (↑A : Type u)) (a_1 : G),
  Eq (α := (↑A : Type u))
    ((((ModuleCat.Hom.hom (Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A))) ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry }.X₃ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                    X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry :
                    ShortComplex (ModuleCat k) }.X₃ :
              Type u)) :
          (a : G) → (↑A : Type u))
        a_1 :
      (↑A : Type u))
    ((((ModuleCat.Hom.hom
                    (Hom.τ₃
                      (𝟙
                        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                          X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                          f := d₃₂ A, g := d₂₁ A, zero := sorry : ShortComplex (ModuleCat k) })) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry }.X₃ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                    X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry :
                    ShortComplex (ModuleCat k) }.X₃ :
              Type u)) :
          (a : G) → (↑A : Type u))
        a_1 :
      (↑A : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) = Hom.τ₃ (𝟙 (shortComplexH2 A))
have refine_3 : Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) =
  Hom.τ₃
    (𝟙
      { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
        X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry : ShortComplex (ModuleCat k) })
Tactic: { simp only [shortComplexH2]
    ext
    simp }
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
refine_3 :
  Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) =
    Hom.τ₃
      (𝟙
        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })
⊢ Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) = Hom.τ₃ (𝟙 (shortComplexH2 A))
have refine_3₁ : ∀ (a : G) (x : (↑A : Type u)) (a_1 : G),
  Eq (α := (↑A : Type u))
    ((((ModuleCat.Hom.hom (Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A))) ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry }.X₃ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                    X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry :
                    ShortComplex (ModuleCat k) }.X₃ :
              Type u)) :
          (a : G) → (↑A : Type u))
        a_1 :
      (↑A : Type u))
    ((((ModuleCat.Hom.hom
                    (Hom.τ₃
                      (𝟙
                        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                          X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                          f := d₃₂ A, g := d₂₁ A, zero := sorry : ShortComplex (ModuleCat k) })) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry }.X₃ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                    X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := sorry :
                    ShortComplex (ModuleCat k) }.X₃ :
              Type u)) :
          (a : G) → (↑A : Type u))
        a_1 :
      (↑A : Type u))
Tactic: { simp only [shortComplexH2]
    ext
    simp }
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ
have refine_1 : (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
  (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
Tactic: refine ShortComplex.hom_ext _ _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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 :
  (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
⊢ mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ
have refine_2 : (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
  (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
Tactic: refine ShortComplex.hom_ext _ _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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 :
  (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
refine_2 :
  (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
⊢ mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ
have refine_3 : (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₃ =
  (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃
Tactic: refine ShortComplex.hom_ext _ _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
have refine_1 : Hom.τ₁
    (mapShortComplexH2 (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' := sorry })) =
  (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
Tactic: simp only [shortComplexH2]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
have refine_1 : Hom.τ₁
    (mapShortComplexH2 (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' := sorry })) =
  (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
Tactic: { simp only [shortComplexH2]
    ext
    simp [Prod.map] }
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
have refine_2 : Hom.τ₂
    (mapShortComplexH2 (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' := sorry })) =
  (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
Tactic: simp only [shortComplexH2]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
have refine_2 : Hom.τ₂
    (mapShortComplexH2 (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' := sorry })) =
  (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
Tactic: { simp only [shortComplexH2]
    ext
    simp [Prod.map] }
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₃ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃
have refine_3 : Hom.τ₃
    (mapShortComplexH2 (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' := sorry })) =
  (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃
Tactic: simp only [shortComplexH2]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₃ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃
have refine_3 : Hom.τ₃
    (mapShortComplexH2 (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' := sorry })) =
  (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃
Tactic: { simp only [shortComplexH2]
    ext
    simp [Prod.map] }
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (hypothesis)
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 × G →₀ (↑A : Type u))) : Type u)
h : x ∈ cycles₂ A
⊢ Membership.mem (α := (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u)) (cycles₂ B)
    ((ModuleCat.Hom.hom (chainsMap₂ f φ) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑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))
have this : Eq (α := (↑(shortComplexH2 B).X₃ : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) ((mapShortComplexH2 f φ).τ₂ ≫ (shortComplexH2 B).g) :
        (a : (↑(shortComplexH2 A).X₂ : Type u)) → (↑(shortComplexH2 B).X₃ : Type u))
      x :
    (↑(shortComplexH2 B).X₃ : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) ((shortComplexH2 A).g ≫ (mapShortComplexH2 f φ).τ₃) :
        (a : (↑(shortComplexH2 A).X₂ : Type u)) → (↑(shortComplexH2 B).X₃ : Type u))
      x :
    (↑(shortComplexH2 B).X₃ : Type u))
Tactic: have := congr($((mapShortComplexH2 f φ).comm₂₃) x)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
⊢ mapCycles₂ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) = mapCycles₂ f φ ≫ mapCycles₂ g ψ
have rw : mapCycles₂ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
  cyclesMap' (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ) (shortComplexH2 A).moduleCatLeftHomologyData
    (shortComplexH2 C).moduleCatLeftHomologyData
Tactic: rw [← cyclesMap'_comp, ← mapShortComplexH2_comp]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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' (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ) (shortComplexH2 A).moduleCatLeftHomologyData
      (shortComplexH2 C).moduleCatLeftHomologyData
⊢ mapCycles₂ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) = mapCycles₂ f φ ≫ mapCycles₂ g ψ
have rw₁ : mapCycles₂ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
  cyclesMap' (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ))
    (shortComplexH2 A).moduleCatLeftHomologyData (shortComplexH2 C).moduleCatLeftHomologyData
Tactic: rw [← cyclesMap'_comp, ← mapShortComplexH2_comp]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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_1 : G →* H
φ : Quiver.Hom.{?u.1130867, max u (?u.1130867 + 1)} A (res f_1 B)
n_1 n : ℕ
X Y Z : Rep k G
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := groupHomology X n ⟶ groupHomology Z n) (map (MonoidHom.id G) (f ≫ g) n)
    (CategoryStruct.comp (Y := groupHomology Y n) (map (MonoidHom.id G) f n) (map (MonoidHom.id G) g n))
have simp : Eq (α := groupHomology X n ⟶ groupHomology Z n) (map (MonoidHom.id G) (f ≫ g) n)
  (HomologicalComplex.homologyMap
    (chainsMap (MonoidHom.comp (MonoidHom.id G) (MonoidHom.id G))
      (f ≫
        ofHom
          {
            toLinearMap :=
              (↑(Hom.hom g) :
                [inst_3 :
                    FunLike (Y.ρ.IntertwiningMap (MonoidHom.comp Z.ρ (MonoidHom.id G))) (↑Y : Type u) (↑Z : Type u)] →
                  [SemilinearMapClass (Y.ρ.IntertwiningMap (MonoidHom.comp Z.ρ (MonoidHom.id G))) (RingHom.id k)
                        (↑Y : Type u) (↑Z : Type u)] →
                    (↑Y : Type u) →ₗ[k] (↑Z : Type u)),
            isIntertwining' := sorry }))
    n)
Tactic: simp only [← HomologicalComplex.homologyMap_comp, ← chainsMap_comp]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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
φ_1 : Quiver.Hom.{?u.1135932, max u (?u.1135932 + 1)} A (res f B)
n_1 n : ℕ
X Y : Rep k H
φ : X ⟶ Y
⊢ Eq (α := Functor.obj (resFunctor f ⋙ functor k G n) X ⟶ Functor.obj (functor k H n) Y)
    (CategoryTheory.Functor.map (resFunctor f ⋙ functor k G n) φ ≫ map f (𝟙 (res f Y)) n)
    (map f (𝟙 (res f X)) n ≫ CategoryTheory.Functor.map (functor k H n) φ)
have simp : Eq (α := cycles (of (MonoidHom.comp X.ρ f)) n ⟶ groupHomology Y n)
  (HomologicalComplex.cyclesMap
      (chainsMap (f.comp (MonoidHom.id G))
        (CategoryStruct.comp (Y := res (MonoidHom.id G) (of (MonoidHom.comp Y.ρ f)))
          (ofHom
            {
              toLinearMap :=
                (↑(Hom.hom φ) :
                  [inst_3 : FunLike (X.ρ.IntertwiningMap Y.ρ) (↑X : Type u) (↑Y : Type u)] →
                    [SemilinearMapClass (X.ρ.IntertwiningMap Y.ρ) (RingHom.id k) (↑X : Type u) (↑Y : Type u)] →
                      (↑X : Type u) →ₗ[k] (↑Y : Type u)),
              isIntertwining' := sorry })
          (ofHom
            {
              toLinearMap :=
                (↑(IntertwiningMap.id (MonoidHom.comp Y.ρ f)) :
                  [inst_3 :
                      FunLike (IntertwiningMap (MonoidHom.comp Y.ρ f) (MonoidHom.comp Y.ρ f)) (↑Y : Type u)
                        (↑Y : Type u)] →
                    [SemilinearMapClass (IntertwiningMap (MonoidHom.comp Y.ρ f) (MonoidHom.comp Y.ρ f)) (RingHom.id k)
                          (↑Y : Type u) (↑Y : Type u)] →
                      (↑Y : Type u) →ₗ[k] (↑Y : Type u)),
              isIntertwining' := sorry })))
      n ≫
    HomologicalComplex.homologyπ (inhomogeneousChains Y) n)
  (HomologicalComplex.cyclesMap
      (chainsMap (MonoidHom.comp (MonoidHom.id H) f)
        (ofHom
          {
            toLinearMap :=
              (↑(Hom.hom φ) :
                [inst_3 :
                    FunLike (X.ρ.IntertwiningMap (MonoidHom.comp Y.ρ (MonoidHom.id H))) (↑X : Type u) (↑Y : Type u)] →
                  [SemilinearMapClass (X.ρ.IntertwiningMap (MonoidHom.comp Y.ρ (MonoidHom.id H))) (RingHom.id k)
                        (↑X : Type u) (↑Y : Type u)] →
                    (↑X : Type u) →ₗ[k] (↑Y : Type u)),
            isIntertwining' := sorry }))
      n ≫
    HomologicalComplex.homologyπ (inhomogeneousChains Y) n)
Tactic: simp only [← cancel_epi (groupHomology.π _ n), functor_obj, Functor.comp_obj, Functor.comp_map,
      functor_map, HomologicalComplex.homologyπ_naturality_assoc,
      HomologicalComplex.homologyπ_naturality, ← HomologicalComplex.cyclesMap_comp_assoc,
      ← chainsMap_comp, res_obj_ρ, Rep.hom_id, Category.id_comp]