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
φ : A ⟶ res f B
n i j : ℕ
hij : j + 1 = i
⊢ ModuleCat.ofHom
        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
          lmapDomain (↑A : Type u) k fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
      (inhomogeneousChains B).d i j =
    (inhomogeneousChains A).d i j ≫
      ModuleCat.ofHom
        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
          lmapDomain (↑A : Type u) k fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x)
have subst : Eq (α := (inhomogeneousChains A).X (j + 1) ⟶ (inhomogeneousChains B).X j)
  (CategoryStruct.comp (Y := (inhomogeneousChains B).X (j + 1))
    (ModuleCat.ofHom
      (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
        lmapDomain (↑A : Type u) k fun (x : Fin (j + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))
    ((inhomogeneousChains B).d (j + 1) j))
  ((inhomogeneousChains A).d (j + 1) j ≫
    ModuleCat.ofHom
      (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
        lmapDomain (↑A : Type u) k fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x))
Tactic: subst hij
Cleared hypotheses: i, hij
-- 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
φ : A ⟶ res f B
n j : ℕ
⊢ Eq (α := (inhomogeneousChains A).X (j + 1) ⟶ (inhomogeneousChains B).X j)
    (CategoryStruct.comp (Y := (inhomogeneousChains B).X (j + 1))
      (ModuleCat.ofHom
        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
          lmapDomain (↑A : Type u) k fun (x : Fin (j + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))
      ((inhomogeneousChains B).d (j + 1) j))
    ((inhomogeneousChains A).d (j + 1) j ≫
      ModuleCat.ofHom
        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
          lmapDomain (↑A : Type u) k fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x))
have h : ∀ (g : Fin (j + 1) → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (a : Fin j → H),
  Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom
                  (ModuleCat.ofHom (lsingle g) ≫
                    CategoryStruct.comp (Y := (inhomogeneousChains B).X (j + 1))
                      (ModuleCat.ofHom
                        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
                          lmapDomain (↑A : Type u) k fun (x : Fin (j + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))
                      ((inhomogeneousChains B).d (j + 1) j)) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X j) : Type u))
              x :
            (↑((inhomogeneousChains B).X j) : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((((ModuleCat.Hom.hom
                  (ModuleCat.ofHom (lsingle g) ≫
                    (inhomogeneousChains A).d (j + 1) j ≫
                      ModuleCat.ofHom
                        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
                          lmapDomain (↑A : Type u) k fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x)) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X j) : Type u))
              x :
            (↑((inhomogeneousChains B).X j) : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑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
φ : A ⟶ res f B
n j : ℕ
g : Fin (j + 1) → G
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
a : Fin j → H
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom
                  (ModuleCat.ofHom (lsingle g) ≫
                    CategoryStruct.comp (Y := (inhomogeneousChains B).X (j + 1))
                      (ModuleCat.ofHom
                        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
                          lmapDomain (↑A : Type u) k fun (x : Fin (j + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))
                      ((inhomogeneousChains B).d (j + 1) j)) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X j) : Type u))
              x :
            (↑((inhomogeneousChains B).X j) : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((((ModuleCat.Hom.hom
                  (ModuleCat.ofHom (lsingle g) ≫
                    (inhomogeneousChains A).d (j + 1) j ≫
                      ModuleCat.ofHom
                        (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ
                          lmapDomain (↑A : Type u) k fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x)) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains B).X j) : Type u))
              x :
            (↑((inhomogeneousChains B).X j) : Type u)) :
          (a : Fin j → H) → (↑B : Type u))
        a :
      (↑B : Type u))
have h : Eq (α := (↑B : Type u))
  (((single (fun (i : Fin j) ↦ (f : (a : G) → H) (g i.succ))
            ((((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((f : (a : G) → H) (g 0))⁻¹ :
                  (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                (a : (↑B : Type u)) → (↑B : Type u))
              ((Hom.hom φ : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))) :
          ((i : Fin j) → H) →₀ (↑B : Type u)) :
        (a : Fin j → H) → (↑B : Type u))
      a :
    (↑B : Type u))
  (((single (Function.comp (β := G) (⇑f : (a : G) → H) fun (i : Fin j) ↦ g i.succ)
            ((((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((f : (a : G) → H) (g 0))⁻¹ :
                  (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                (a : (↑B : Type u)) → (↑B : Type u))
              ((Hom.hom φ : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))) :
          (Fin j → H) →₀ (↑B : Type u)) :
        (a : Fin j → H) → (↑B : Type u))
      a :
    (↑B : Type u))
Tactic: simp [Fin.comp_contractNth, map_add, inhomogeneousChains.d, Rep.hom_comm_apply φ]
-- 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
φ : A ⟶ res f B
n : ℕ
x : Fin n → G
⊢ ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f n =
    ModuleCat.ofHom (lsingle ((⇑f : (a : G) → H) ∘ x) ∘ₗ (Hom.hom φ).toLinearMap)
have 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))
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 B : Rep k G
i : ℕ
φ : A ⟶ B
⊢ ModuleCat.Hom.hom (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) φ) i) =
    mapRange.linearMap (Hom.hom φ).toLinearMap
have 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))
Tactic: refine lhom_ext fun _ _ => ?_
-- 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
⊢ chainsMap (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) = chainsMap f φ ≫ chainsMap g ψ
have 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))
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
⊢ Eq (α := inhomogeneousChains A ⟶ inhomogeneousChains B) (chainsMap f 0) 0
have 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: 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 B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ map (MonoidHom.id G) (φ ≫ ψ) n =
    CategoryStruct.comp (Y := groupHomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
have rw : HomologicalComplex.homologyMap (chainsMap (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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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)
⊢ map (MonoidHom.id G) (φ ≫ ψ) n =
    CategoryStruct.comp (Y := groupHomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
have 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))
Tactic: rw [map, chainsMap_id_comp, HomologicalComplex.homologyMap_comp]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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))
⊢ map (MonoidHom.id G) (φ ≫ ψ) n =
    CategoryStruct.comp (Y := groupHomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
have 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))
Tactic: rw [map, chainsMap_id_comp, HomologicalComplex.homologyMap_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
φ : A ⟶ res f B
⊢ (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom = (chainsIso₀ A).hom ≫ Hom.toModuleCatHom φ
have 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))
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
φ : A ⟶ res f B
⊢ (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom = (chainsIso₁ A).hom ≫ chainsMap₁ f φ
have 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))
Tactic: ext x
-- 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
φ : A ⟶ res f B
⊢ (chainsMap f φ).f 2 ≫ (chainsIso₂ B).hom = (chainsIso₂ A).hom ≫ chainsMap₂ f φ
have 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))
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
φ : A ⟶ res f B
⊢ (chainsMap f φ).f 3 ≫ (chainsIso₃ B).hom = (chainsIso₃ A).hom ≫ chainsMap₃ f φ
have h : ∀ (g : Fin 3 → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (a : H × H × H),
  Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsMap f φ).f 3 ≫ (chainsIso₃ B).hom) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) →
                  (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u))
              x :
            (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u)) :
          (a : H × 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 × H →₀ (↑B : Type u))) : Type u))
              x :
            (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u)) :
          (a : H × H × H) → (↑B : Type u))
        a :
      (↑B : 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 B : Rep k G
f : A ⟶ B
⊢ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = (H0Iso A).hom ≫ CategoryTheory.Functor.map (coinvariantsFunctor k G) f
have rw : H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom =
  H0π A ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (coinvariantsFunctor k G) f
Tactic: rw [← cancel_epi (H0π A)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
f : A ⟶ B
⊢ H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom =
    H0π A ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (coinvariantsFunctor k G) f
have hf : ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
  Eq (α := (↑(Functor.obj (coinvariantsFunctor k G) B) : Type u))
    ((ModuleCat.Hom.hom (H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((coinvariantsFunctor k G).obj B) : Type u))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) B) : Type u))
    ((ModuleCat.Hom.hom (H0π A ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (coinvariantsFunctor k G) f) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((coinvariantsFunctor k G).obj B) : Type u))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) B) : Type u))
Tactic: ext
-- 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_1 : Rep k G
B_1 : Rep k H
f_1 : G →* H
φ : Quiver.Hom.{?u.311982, max u (?u.311982 + 1)} A_1 (res f_1 B_1)
n : ℕ
A B : Rep k G
f : A ⟶ B
inst_3 : Epi f
Z : ModuleCat k
g h : groupHomology B 0 ⟶ Z
hgh : Eq (α := groupHomology A 0 ⟶ Z) (map (MonoidHom.id G) f 0 ≫ g) (map (MonoidHom.id G) f 0 ≫ h)
⊢ g = h
have hgh₁ : H0π A ≫ map (MonoidHom.id G) f 0 ≫ g = H0π A ≫ map (MonoidHom.id G) f 0 ≫ h
Tactic: simp only [← cancel_epi (H0π A)] at hgh
Cleared hypotheses: hgh
-- 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
φ : A ⟶ res f B
n : ℕ
⊢ chainsMap₂ f φ ≫ d₂₁ B = d₂₁ A ≫ chainsMap₁ f φ
have hf : ∀ (a : G × G) (x : (↑A : Type u)),
  Eq (α := (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
    ((ModuleCat.Hom.hom (chainsMap₂ f φ ≫ d₂₁ B) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
    ((ModuleCat.Hom.hom (d₂₁ A ≫ chainsMap₁ f φ) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
Tactic: ext : 3
-- 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
φ : A ⟶ res f B
n : ℕ
⊢ chainsMap₁ f φ ≫ (shortComplexH1 B).g = (shortComplexH1 A).g ≫ Hom.toModuleCatHom φ
have simp : chainsMap₁ f φ ≫ d₁₀ B = d₁₀ A ≫ Hom.toModuleCatHom φ
Tactic: simp only [shortComplexH1]
-- 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
φ : A ⟶ res f B
n : ℕ
⊢ chainsMap₁ f φ ≫ d₁₀ B = d₁₀ A ≫ Hom.toModuleCatHom φ
have hf : ∀ (a : G) (x : (↑A : Type u)),
  Eq (α := (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom (chainsMap₁ f φ ≫ d₁₀ B) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A ≫ Hom.toModuleCatHom φ) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))
Tactic: ext : 3
-- 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 (α := shortComplexH1 A ⟶ shortComplexH1 B) (mapShortComplexH1 f 0) 0
have refine_1 : Eq (α := (shortComplexH1 A).X₁ ⟶ (shortComplexH1 B).X₁) (Hom.τ₁ (mapShortComplexH1 f 0)) (Hom.τ₁ 0)
Tactic: refine ShortComplex.hom_ext _ _ ?_ ?_ rfl
-- 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 (α := (shortComplexH1 A).X₁ ⟶ (shortComplexH1 B).X₁) (Hom.τ₁ (mapShortComplexH1 f 0)) (Hom.τ₁ 0)
⊢ Eq (α := shortComplexH1 A ⟶ shortComplexH1 B) (mapShortComplexH1 f 0) 0
have refine_2 : Eq (α := (shortComplexH1 A).X₂ ⟶ (shortComplexH1 B).X₂) (Hom.τ₂ (mapShortComplexH1 f 0)) (Hom.τ₂ 0)
Tactic: refine ShortComplex.hom_ext _ _ ?_ ?_ rfl