awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k (G × G →₀ (↑A : Type u))) (ModuleCat.of k (H × H →₀ (↑B : Type u))))
    (Hom.τ₁ (mapShortComplexH1 f 0)) (Hom.τ₁ 0)
have refine_1 : ∀ (a : G × G) (x : (↑A : Type u)) (a_1 : H × 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 := sorry }.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 := sorry :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : H × 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 := sorry :
                              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 := sorry :
                              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 := sorry }.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 := sorry :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : H × H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))
Tactic: ext
-- 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
refine_1 :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k (G × G →₀ (↑A : Type u))) (ModuleCat.of k (H × H →₀ (↑B : Type u))))
    (Hom.τ₁ (mapShortComplexH1 f 0)) (Hom.τ₁ 0)
⊢ Eq (α := (shortComplexH1 A).X₁ ⟶ (shortComplexH1 B).X₁) (Hom.τ₁ (mapShortComplexH1 f 0)) (Hom.τ₁ 0)
have refine_1₁ : ∀ (a : G × G) (x : (↑A : Type u)) (a_1 : H × 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 := sorry }.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 := sorry :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : H × 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 := sorry :
                              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 := sorry :
                              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 := sorry }.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 := sorry :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : H × H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))
Tactic: { simp only [shortComplexH1]
    ext
    simp }
-- 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
⊢ 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)
have 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 := sorry }.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 := sorry :
                    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 := sorry :
                              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 := sorry :
                              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 := sorry }.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 := sorry :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))
Tactic: ext
-- 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
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)
⊢ Eq (α := (shortComplexH1 A).X₂ ⟶ (shortComplexH1 B).X₂) (Hom.τ₂ (mapShortComplexH1 f 0)) (Hom.τ₂ 0)
have 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 := sorry }.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 := sorry :
                    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 := sorry :
                              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 := sorry :
                              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 := sorry }.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 := sorry :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))
Tactic: { simp only [shortComplexH1]
    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
⊢ mapShortComplexH1 (MonoidHom.id G) (𝟙 A) = 𝟙 (shortComplexH1 A)
have 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))
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
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)
have 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))
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
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)
have 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))
Tactic: 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
⊢ mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ
have refine_1 : (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
  (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁
Tactic: refine ShortComplex.hom_ext _ _ ?_ ?_ rfl
-- 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 :
  (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 ψ
have refine_2 : (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
  (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂
Tactic: refine ShortComplex.hom_ext _ _ ?_ ?_ rfl
-- 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
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁
have 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' := sorry })) =
  (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁
Tactic: simp only [shortComplexH1]
-- 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
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁
have 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' := sorry })) =
  (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁
Tactic: { simp only [shortComplexH1]
    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
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂
have 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' := sorry })) =
  (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂
Tactic: simp only [shortComplexH1]
-- 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
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂
have 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' := sorry })) =
  (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂
Tactic: { simp only [shortComplexH1]
    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 →₀ (↑A : Type u))) : Type u)
h : x ∈ cycles₁ A
⊢ 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))
have 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))
Tactic: have := congr($((mapShortComplexH1 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' (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ) (shortComplexH1 A).moduleCatLeftHomologyData
    (shortComplexH1 C).moduleCatLeftHomologyData
Tactic: rw [← cyclesMap'_comp, ← mapShortComplexH1_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' (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ) (shortComplexH1 A).moduleCatLeftHomologyData
      (shortComplexH1 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' (mapShortComplexH1 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ))
    (shortComplexH1 A).moduleCatLeftHomologyData (shortComplexH1 C).moduleCatLeftHomologyData
Tactic: rw [← cyclesMap'_comp, ← mapShortComplexH1_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
φ : A ⟶ res 1 B
⊢ Eq (α := groupHomology A 1 ⟶ groupHomology B 1) (map 1 φ 1) 0
have simp : mapCycles₁ 1 φ ≫ H1π B = 0
Tactic: simp only [← cancel_epi (H1π A), H1π_comp_map, Limits.comp_zero]
-- 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
φ : A ⟶ res 1 B
⊢ mapCycles₁ 1 φ ≫ H1π B = 0
have hf : ∀ (x : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)),
  Eq (α := (↑(H1 B) : Type u))
    ((ModuleCat.Hom.hom (mapCycles₁ 1 φ ≫ H1π B) : (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 B) : Type u))
        x :
      (↑(H1 B) : Type u))
    ((ModuleCat.Hom.hom 0 : (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 B) : Type u)) x :
      (↑(H1 B) : Type u))
Tactic: ext x