awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
rw :
  HSub.hSub (α := (↑(groupCohomology A i) : Type u)) (β := (↑(groupCohomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
            x :
          (↑(groupCohomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
            y :
          (↑(groupCohomology A i) : Type u)) =
      0 ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈
      (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range
⊢ Eq (α := (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          x :
        (↑(groupCohomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          y :
        (↑(groupCohomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈
      (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range
have rw₁ : Eq (α := (↑(groupCohomology A i) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
          (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
        (x - y) :
      (↑(groupCohomology A i) : Type u))
    (0 : (↑(groupCohomology A i) : Type u)) ↔
  (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈
    (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range
Tactic: rw [← sub_eq_zero, ← map_sub, groupCohomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_2, u, u} k H
B : Rep.{u_2, u, u} k G
f₁ f₂ : G →* H
h : f₁ = f₂
φ : res f₁ A ⟶ B
T : Type u_1
F : (f : G →* H) → (φ : res f A ⟶ B) → T
⊢ F f₁ φ = F f₂ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ res x A ⟶ B) φ h)
have subst : F f₁ φ = F f₁ (Eq.rec (motive := fun (x : G →* H) (h : f₁ = x) ↦ res x A ⟶ B) φ sorry)
Tactic: subst h
Cleared hypotheses: f₂, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n i j : ℕ
hij : i + 1 = j
⊢ ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
      (inhomogeneousCochains B).d i j =
    (inhomogeneousCochains A).d i j ≫
      ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin j → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin j → G) ↦ (⇑f : (a : G) → H) ∘ x)
have subst : Eq (α := (inhomogeneousCochains A).X i ⟶ (inhomogeneousCochains B).X (i + 1))
  (ModuleCat.ofHom
      ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ
        LinearMap.funLeft k (↑A : Type u) fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
    (inhomogeneousCochains B).d i (i + 1))
  (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
    (ModuleCat.ofHom
      ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ
        LinearMap.funLeft k (↑A : Type u) fun (x : Fin (i + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x)))
Tactic: subst hij
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n i : ℕ
⊢ Eq (α := (inhomogeneousCochains A).X i ⟶ (inhomogeneousCochains B).X (i + 1))
    (ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
      (inhomogeneousCochains B).d i (i + 1))
    (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
      (ModuleCat.ofHom
        ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ
          LinearMap.funLeft k (↑A : Type u) fun (x : Fin (i + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x)))
have hf : ∀ (x : (↑((inhomogeneousCochains A).X i) : Type u)) (g : Fin (i + 1) → G),
  Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ
                  LinearMap.funLeft k (↑A : Type u) fun (x : Fin i → G) ↦ (⇑f : (a : G) → H) ∘ x) ≫
              (inhomogeneousCochains B).d i (i + 1)) :
          (a : (↑((inhomogeneousCochains A).X i) : Type u)) → (↑((inhomogeneousCochains B).X (i + 1)) : Type u))
        x g :
      (↑B : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y := (inhomogeneousCochains A).X (i + 1)) ((inhomogeneousCochains A).d i (i + 1))
              (ModuleCat.ofHom
                ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ
                  LinearMap.funLeft k (↑A : Type u) fun (x : Fin (i + 1) → G) ↦ (⇑f : (a : G) → H) ∘ x))) :
          (a : (↑((inhomogeneousCochains A).X i) : Type u)) → (↑((inhomogeneousCochains B).X (i + 1)) : Type u))
        x g :
      (↑B : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.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 := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
have rw : HomologicalComplex.homologyMap (cochainsMap (MonoidHom.id G) (φ ≫ ψ)) n =
  CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
Tactic: rw [map, cochainsMap_id_comp, HomologicalComplex.homologyMap_comp]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.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 (cochainsMap (MonoidHom.id G) (φ ≫ ψ)) n =
    CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
⊢ map (MonoidHom.id G) (φ ≫ ψ) n =
    CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
have rw₁ : Eq (α := groupCohomology A n ⟶ groupCohomology C n)
  (HomologicalComplex.homologyMap
    (CategoryStruct.comp (Y := inhomogeneousCochains B) (cochainsMap (MonoidHom.id G) φ)
      (cochainsMap (MonoidHom.id G) ψ))
    n)
  (CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n))
Tactic: rw [map, cochainsMap_id_comp, HomologicalComplex.homologyMap_comp]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.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 (cochainsMap (MonoidHom.id G) (φ ≫ ψ)) n =
    CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
rw₁ :
  Eq (α := groupCohomology A n ⟶ groupCohomology C n)
    (HomologicalComplex.homologyMap
      (CategoryStruct.comp (Y := inhomogeneousCochains B) (cochainsMap (MonoidHom.id G) φ)
        (cochainsMap (MonoidHom.id G) ψ))
      n)
    (CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n))
⊢ map (MonoidHom.id G) (φ ≫ ψ) n =
    CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)
have rw₂ : Eq (α := groupCohomology A n ⟶ groupCohomology C n)
  (CategoryStruct.comp (Y := HomologicalComplex.homology (inhomogeneousCochains B) n)
    (HomologicalComplex.homologyMap (cochainsMap (MonoidHom.id G) φ) n)
    (HomologicalComplex.homologyMap (cochainsMap (MonoidHom.id G) ψ) n))
  (CategoryStruct.comp (Y := groupCohomology B n) (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n))
Tactic: rw [map, cochainsMap_id_comp, HomologicalComplex.homologyMap_comp]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ (cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom = (cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ
have hf : ∀ (x : Fin 0 → H) (x_1 : (↑A : Type u)),
  Eq (α := (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom ((cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x_1 :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x_1 :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : Fin 0 → H
x_1 : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom ((cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x_1 :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x_1 :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))
have hf : Eq (α := (↑B : Type u))
  ((ModuleCat.Hom.hom
            ((ModuleCat.ofHom (LinearMap.funLeft k (↑A : Type u) fun (x : Fin 0 → G) ↦ default) ≫
                ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin 0 → G))) ≫
              (cochainsIso₀ B).hom) ∘ₗ
          LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
        (a : (↑A : Type u)) → (↑B : Type u))
      x_1 :
    (↑B : Type u))
  ((ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) ∘ₗ
          LinearMap.single k (fun (i : Fin 0 → H) ↦ (↑A : Type u)) x :
        (a : (↑A : Type u)) → (↑B : Type u))
      x_1 :
    (↑B : Type u))
Tactic: simp only [cochainsMap_f, Unique.eq_default (f ∘ _)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ (cochainsMap f φ).f 2 ≫ (cochainsIso₂ B).hom = (cochainsIso₂ A).hom ≫ cochainsMap₂ f φ
have hf : ∀ (x : (↑((inhomogeneousCochains A).X 2) : Type u)) (g : G × G),
  Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsMap f φ).f 2 ≫ (cochainsIso₂ B).hom) :
          (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₂ A).hom ≫ cochainsMap₂ f φ) :
          (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
Tactic: ext x g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 2) : Type u)
g : G × G
⊢ Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsMap f φ).f 2 ≫ (cochainsIso₂ B).hom) :
          (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₂ A).hom ≫ cochainsMap₂ f φ) :
          (a : (↑((inhomogeneousCochains A).X 2) : Type u)) → (↑(ModuleCat.of k (G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
have hf : Eq (α := (↑B : Type u))
  ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
      (x
        ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
          (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
              (a : G × G) → (i : Fin 2) → G)
            g))) :
    (↑B : Type u))
  ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
      (x
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
          (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g))) :
    (↑B : Type u))
Tactic: change φ.hom (x _) = φ.hom (x _)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 2) : Type u)
g : G × G
⊢ Eq (α := (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
            (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              g))) :
      (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) :
              (a : H × H) → (i : Fin 2) → H)
            (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g))) :
      (↑B : Type u))
have hf : ∀ (x : Fin 2),
  Eq (α := H)
    ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          g)
        x :
      H)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
        (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g) x :
      H)
Tactic: rcongr x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x_1 : (↑((inhomogeneousCochains A).X 2) : Type u)
g : G × G
x : Fin 2
⊢ Eq (α := H)
    ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          g)
        x :
      H)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
        (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g) x :
      H)
have hf : Eq (α := H)
  ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
      (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G) g)
      ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, sorry⟩) :
    H)
  (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
      (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g)
      ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, sorry⟩) :
    H)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x_1 : (↑((inhomogeneousCochains A).X 2) : Type u)
g : G × G
x : Fin 2
hf :
  Eq (α := H)
    ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
        (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g)
        ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
⊢ Eq (α := H)
    ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
        (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
          g)
        x :
      H)
    (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
        (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g) x :
      H)
have hf₁ : Eq (α := H)
  ((fun (x : Fin 2 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 2 → H))
      (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G) g)
      ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, sorry⟩) :
    H)
  (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ H) : H × H ≃ ((i : Fin 2) → H)) : (a : H × H) → (i : Fin 2) → H)
      (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H) g)
      ((fun (i : Fin ({ len := 1 : SimplexCategory }.len + 1)) ↦ i) ⟨1, sorry⟩) :
    H)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ (cochainsMap f φ).f 3 ≫ (cochainsIso₃ B).hom = (cochainsIso₃ A).hom ≫ cochainsMap₃ f φ
have hf : ∀ (x : (↑((inhomogeneousCochains A).X 3) : Type u)) (g : G × G × G),
  Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsMap f φ).f 3 ≫ (cochainsIso₃ B).hom) :
          (a : (↑((inhomogeneousCochains A).X 3) : Type u)) → (↑(ModuleCat.of k (G × G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₃ A).hom ≫ cochainsMap₃ f φ) :
          (a : (↑((inhomogeneousCochains A).X 3) : Type u)) → (↑(ModuleCat.of k (G × G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
Tactic: ext x g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 3) : Type u)
g : G × G × G
⊢ Eq (α := (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsMap f φ).f 3 ≫ (cochainsIso₃ B).hom) :
          (a : (↑((inhomogeneousCochains A).X 3) : Type u)) → (↑(ModuleCat.of k (G × G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₃ A).hom ≫ cochainsMap₃ f φ) :
          (a : (↑((inhomogeneousCochains A).X 3) : Type u)) → (↑(ModuleCat.of k (G × G × G → (↑B : Type u))) : Type u))
        x g :
      (↑B : Type u))
have hf : Eq (α := (↑B : Type u))
  ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
      (x
        ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
          ((Equiv.symm
                (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                  ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
              (a : G × G × G) → (i : Fin (2 + 1)) → G)
            g))) :
    (↑B : Type u))
  ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
      (x
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
                ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
            (a : H × H × H) → (i : Fin (2 + 1)) → H)
          (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g))) :
    (↑B : Type u))
Tactic: change φ.hom (x _) = φ.hom (x _)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑((inhomogeneousCochains A).X 3) : Type u)
g : G × G × G
⊢ Eq (α := (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
            ((Equiv.symm
                  (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                    ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
                (a : G × G × G) → (i : Fin (2 + 1)) → G)
              g))) :
      (↑B : Type u))
    ((Hom.hom φ : (a : (↑(res f A) : Type u)) → (↑B : Type u))
        (x
          ((Equiv.symm
                (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
                  ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
              (a : H × H × H) → (i : Fin (2 + 1)) → H)
            (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g))) :
      (↑B : Type u))
have hf : ∀ (x : Fin 3),
  Eq (α := H)
    ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
            (a : G × G × G) → (i : Fin (2 + 1)) → G)
          g)
        x :
      H)
    ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
              ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
          (a : H × H × H) → (i : Fin (2 + 1)) → H)
        (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g) x :
      H)
Tactic: rcongr x