awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B : Rep k G
f : G →* H
φ : Quiver.Hom.{?u.266374, max (?u.266374 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
x : ↥(cocycles₁ (A.quotientToInvariants S))
hx :
  Eq (α := (↑(H1InfRes A S).X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1InfRes A S).f :
          (a : (↑(H1InfRes A S).X₁ : Type u)) → (↑(H1InfRes A S).X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S)))
                (H1π (A.quotientToInvariants S)) :
              (a : (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u)) →
                (↑(H1 (A.quotientToInvariants S)) : Type u))
            x :
          (↑(H1 (A.quotientToInvariants S)) : Type u)) :
      (↑(H1InfRes A S).X₂ : Type u))
    (0 : (↑(H1InfRes A S).X₂ : Type u))
⊢ Eq (α := (↑(groupCohomology A 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π (of A.ρ)) :
          (a : ↥(cocycles₁ (of A.ρ))) → (↑(groupCohomology (of A.ρ) 1) : Type u))
        (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) (Y :=
                  ModuleCat.of k ↥(cocycles₁ (of A.ρ)))
                  (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) :
                    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S)))
                      (ModuleCat.of k ↥(cocycles₁ (of A.ρ)))) :
                (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u) →ₗ[k]
                  (↑(ModuleCat.of k ↥(cocycles₁ (of A.ρ))) : Type u)) :
              (a : ↥(cocycles₁ (A.quotientToInvariants S))) → ↥(cocycles₁ (of A.ρ)))
            x :
          ↥(cocycles₁ (of A.ρ))) :
      (↑(groupCohomology (of A.ρ) 1) : Type u))
    (0 : (↑(H1InfRes A S).X₂ : Type u))

Tactic:
simp_all only [H1InfRes_X₂, H1InfRes_X₁, H1InfRes_f, H1π_comp_map_apply (QuotientGroup.mk' S)]

Premises used: groupCohomology.H1InfRes_X₂, groupCohomology.H1InfRes_X₁, QuotientGroup.mk', groupCohomology.H1π_comp_map_apply, groupCohomology.H1InfRes_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B : Rep k G
f : G →* H
φ : Quiver.Hom.{?u.266374, max (?u.266374 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
x : (↑(H1InfRes A S).X₁ : Type u)
hx :
  Eq (α := (↑(H1InfRes A S).X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1InfRes A S).f :
          (a : (↑(H1InfRes A S).X₁ : Type u)) → (↑(H1InfRes A S).X₂ : Type u))
        x :
      (↑(H1InfRes A S).X₂ : Type u))
    (0 : (↑(H1InfRes A S).X₂ : Type u))
h :
  ∀ (x : ↥(cocycles₁ (A.quotientToInvariants S)))
    (hx :
      Eq (α := (↑(H1InfRes A S).X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (H1InfRes A S).f :
              (a : (↑(H1InfRes A S).X₁ : Type u)) → (↑(H1InfRes A S).X₂ : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S)))
                    (H1π (A.quotientToInvariants S)) :
                  (a : (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u)) →
                    (↑(H1 (A.quotientToInvariants S)) : Type u))
                x :
              (↑(H1 (A.quotientToInvariants S)) : Type u)) :
          (↑(H1InfRes A S).X₂ : Type u))
        (0 : (↑(H1InfRes A S).X₂ : Type u))),
    Eq (α := (↑(H1InfRes A S).X₁ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S)))
              (H1π (A.quotientToInvariants S)) :
            (a : (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u)) →
              (↑(H1 (A.quotientToInvariants S)) : Type u))
          x :
        (↑(H1 (A.quotientToInvariants S)) : Type u))
      (0 : (↑(H1InfRes A S).X₁ : Type u))
⊢ x = 0

Tactic:
induction x using H1_induction_on with | @h x =>
  simp_all only [H1InfRes_X₂, H1InfRes_X₁, H1InfRes_f, H1π_comp_map_apply (QuotientGroup.mk' S)]
  rcases (H1π_eq_zero_iff _).1 hx with ⟨y, hy⟩
  refine (H1π_eq_zero_iff _).2 ⟨⟨y, fun s => ?_⟩, funext fun g => QuotientGroup.induction_on g
    fun g => Subtype.ext <| by simpa [-SetLike.coe_eq_coe] using congr_fun hy g⟩
  simpa [coe_mapCocycles₁ (x := x), sub_eq_zero, (QuotientGroup.eq_one_iff s.1).2 s.2] using
    congr_fun hy s.1

Premises used: groupCohomology.coe_mapCocycles₁, sub_eq_zero, groupCohomology.H1InfRes_X₂, groupCohomology.H1π_eq_zero_iff, groupCohomology.H1InfRes_X₁, QuotientGroup.mk', groupCohomology.H1π_comp_map_apply, Iff.mp, groupCohomology.H1InfRes_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
rw : (ModuleCat.Hom.hom (H1InfRes A S).g).ker ≤ (ModuleCat.Hom.hom (H1InfRes A S).f).range
⊢ (H1InfRes A S).Exact

Tactic:
rw [moduleCat_exact_iff_ker_sub_range]

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
x : ↥(cocycles₁ A)
hx :
  Membership.mem (α := (↑(H1InfRes A S).X₂ : Type u)) (ModuleCat.Hom.hom (H1InfRes A S).g).ker
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π A) :
          (a : (↑(ModuleCat.of k ↥(cocycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
        x :
      (↑(H1 A) : Type u))
⊢ Eq (α := (↑(groupCohomology (res S.subtype A) 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π (res S.subtype A)) :
          (a : ↥(cocycles₁ (res S.subtype A))) → (↑(groupCohomology (res S.subtype A) 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (mapCocycles₁ S.subtype (𝟙 (res S.subtype A))) :
              (a : ↥(cocycles₁ A)) → ↥(cocycles₁ (res S.subtype A)))
            x :
          ↥(cocycles₁ (res S.subtype A))) :
      (↑(groupCohomology (res S.subtype A) 1) : Type u))
    (0 : (↑(groupCohomology (res S.subtype A) 1) : Type u))

Tactic:
simp_all only [H1InfRes_X₂, H1InfRes_X₃, H1InfRes_g, H1InfRes_X₁, LinearMap.mem_ker,
    H1π_comp_map_apply S.subtype, H1InfRes_f]

Premises used: Subgroup.subtype, groupCohomology.H1InfRes_X₂, groupCohomology.H1InfRes_X₃, LinearMap.mem_ker, groupCohomology.H1InfRes_X₁, groupCohomology.H1π_comp_map_apply, groupCohomology.H1InfRes_g, groupCohomology.H1InfRes_f
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
x : ↥(cocycles₁ A)
hx :
  Eq (α := (↑(groupCohomology (res S.subtype A) 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π (res S.subtype A)) :
          (a : ↥(cocycles₁ (res S.subtype A))) → (↑(groupCohomology (res S.subtype A) 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (mapCocycles₁ S.subtype (𝟙 (res S.subtype A))) :
              (a : ↥(cocycles₁ A)) → ↥(cocycles₁ (res S.subtype A)))
            x :
          ↥(cocycles₁ (res S.subtype A))) :
      (↑(groupCohomology (res S.subtype A) 1) : Type u))
    (0 : (↑(groupCohomology (res S.subtype A) 1) : Type u))
h :
  ∀ (y : (↑A : Type u))
    (hy :
      Eq (α := ↥S → (↑(res S.subtype A) : Type u))
        ((ModuleCat.Hom.hom (d₀₁ (res S.subtype A)) :
              (a : (↑(ModuleCat.of k (↑(res S.subtype A) : Type u)) : Type u)) → ↥S → (↑(res S.subtype A) : Type u))
            y :
          ↥S → (↑(res S.subtype A) : Type u))
        ((⇑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                      ModuleCat.carrier) (mapCocycles₁ S.subtype (𝟙 (res S.subtype A))) :
                    (a : ↥(cocycles₁ A)) → ↥(cocycles₁ (res S.subtype A)))
                  x :
                ↥(cocycles₁ (res S.subtype A))) :
            (a : ↥S) → (↑(res S.subtype A) : Type u)) :
          (a : ↥S) → (↑(res S.subtype A) : Type u))),
    Membership.mem (α := (↑(groupCohomology A 1) : Type u)) (γ := Submodule k (↑(groupCohomology A 1) : Type u))
      (LinearMap.range (M := (↑(groupCohomology (A.quotientToInvariants S) 1) : Type u))
        (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1π A) :
            (a : ↥(cocycles₁ A)) → (↑(H1 A) : Type u))
          x :
        (↑(H1 A) : Type u))
⊢ Membership.mem (α := (↑(groupCohomology A 1) : Type u)) (γ := Submodule k (↑(groupCohomology A 1) : Type u))
    (LinearMap.range (M := (↑(groupCohomology (A.quotientToInvariants S) 1) : Type u))
      (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π A) :
          (a : ↥(cocycles₁ A)) → (↑(H1 A) : Type u))
        x :
      (↑(H1 A) : Type u))

Tactic:
rcases (H1π_eq_zero_iff _).1 hx with ⟨(y : A), hy⟩

Premises used: groupCohomology.H1π_eq_zero_iff, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
x : ↥(cocycles₁ A)
hx :
  Eq (α := (↑(groupCohomology (res S.subtype A) 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π (res S.subtype A)) :
          (a : ↥(cocycles₁ (res S.subtype A))) → (↑(groupCohomology (res S.subtype A) 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (mapCocycles₁ S.subtype (𝟙 (res S.subtype A))) :
              (a : ↥(cocycles₁ A)) → ↥(cocycles₁ (res S.subtype A)))
            x :
          ↥(cocycles₁ (res S.subtype A))) :
      (↑(groupCohomology (res S.subtype A) 1) : Type u))
    (0 : (↑(groupCohomology (res S.subtype A) 1) : Type u))
y : (↑A : Type u)
hy :
  Eq (α := ↥S → (↑(res S.subtype A) : Type u))
    ((ModuleCat.Hom.hom (d₀₁ (res S.subtype A)) :
          (a : (↑(ModuleCat.of k (↑(res S.subtype A) : Type u)) : Type u)) → ↥S → (↑(res S.subtype A) : Type u))
        y :
      ↥S → (↑(res S.subtype A) : Type u))
    ((⇑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (mapCocycles₁ S.subtype (𝟙 (res S.subtype A))) :
                (a : ↥(cocycles₁ A)) → ↥(cocycles₁ (res S.subtype A)))
              x :
            ↥(cocycles₁ (res S.subtype A))) :
        (a : ↥S) → (↑(res S.subtype A) : Type u)) :
      (a : ↥S) → (↑(res S.subtype A) : Type u))
⊢ ∀ (g h : G),
    (x : (a : G) → (↑A : Type u)) (g * h) =
      HAdd.hAdd (α := (↑A : Type u)) (β := (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            ((x : (a : G) → (↑A : Type u)) h : (↑A : Type u)) :
          (↑A : Type u))
        ((x : (a : G) → (↑A : Type u)) g : (↑A : Type u))

Tactic:
have h1 := (mem_cocycles₁_iff x).1 x.2
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
x : ↥(cocycles₁ A)
hx :
  Eq (α := (↑(groupCohomology (res S.subtype A) 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π (res S.subtype A)) :
          (a : ↥(cocycles₁ (res S.subtype A))) → (↑(groupCohomology (res S.subtype A) 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (mapCocycles₁ S.subtype (𝟙 (res S.subtype A))) :
              (a : ↥(cocycles₁ A)) → ↥(cocycles₁ (res S.subtype A)))
            x :
          ↥(cocycles₁ (res S.subtype A))) :
      (↑(groupCohomology (res S.subtype A) 1) : Type u))
    (0 : (↑(groupCohomology (res S.subtype A) 1) : Type u))
y : (↑A : Type u)
hy :
  Eq (α := ↥S → (↑(res S.subtype A) : Type u))
    ((ModuleCat.Hom.hom (d₀₁ (res S.subtype A)) :
          (a : (↑(ModuleCat.of k (↑(res S.subtype A) : Type u)) : Type u)) → ↥S → (↑(res S.subtype A) : Type u))
        y :
      ↥S → (↑(res S.subtype A) : Type u))
    ((⇑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (mapCocycles₁ S.subtype (𝟙 (res S.subtype A))) :
                (a : ↥(cocycles₁ A)) → ↥(cocycles₁ (res S.subtype A)))
              x :
            ↥(cocycles₁ (res S.subtype A))) :
        (a : ↥S) → (↑(res S.subtype A) : Type u)) :
      (a : ↥S) → (↑(res S.subtype A) : Type u))
h1 :
  ∀ (g h : G),
    (x : (a : G) → (↑A : Type u)) (g * h) =
      HAdd.hAdd (α := (↑A : Type u)) (β := (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            ((x : (a : G) → (↑A : Type u)) h : (↑A : Type u)) :
          (↑A : Type u))
        ((x : (a : G) → (↑A : Type u)) g : (↑A : Type u))
⊢ ∀ s ∈ S,
    (x : (a : G) → (↑A : Type u)) s =
      HSub.hSub (α := (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            y :
          (↑A : Type u))
        y

Tactic:
have h2 : ∀ s ∈ S, x s = A.ρ s y - y :=
    fun s hs => funext_iff.1 hy.symm ⟨s, hs⟩
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_1, u, u} k H
B : Rep.{u_1, u, u} k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
hf :
  ∀ (x : (↑(shortComplexH2 A).X₁ : Type (max u u_1))),
    Eq (α := (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
      ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH2 B).f) :
            (a : (↑(shortComplexH2 A).X₁ : Type (max u u_1))) → (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
          x :
        (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
      ((ModuleCat.Hom.hom ((shortComplexH2 A).f ≫ cochainsMap₂ f φ) :
            (a : (↑(shortComplexH2 A).X₁ : Type (max u u_1))) → (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
          x :
        (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
⊢ cochainsMap₁ f φ ≫ (shortComplexH2 B).f = (shortComplexH2 A).f ≫ cochainsMap₂ f φ

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_1, u, u} k H
B : Rep.{u_1, u, u} k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : (↑(shortComplexH2 A).X₁ : Type (max u u_1))
hf :
  ∀ (g : G × G),
    Eq.{u_1 + 1} (α := (↑B : Type u_1))
      ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH2 B).f) :
            (a : (↑(shortComplexH2 A).X₁ : Type (max u u_1))) → (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
          x g :
        (↑B : Type u_1))
      ((ModuleCat.Hom.hom ((shortComplexH2 A).f ≫ cochainsMap₂ f φ) :
            (a : (↑(shortComplexH2 A).X₁ : Type (max u u_1))) → (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
          x g :
        (↑B : Type u_1))
⊢ Eq (α := (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
    ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH2 B).f) :
          (a : (↑(shortComplexH2 A).X₁ : Type (max u u_1))) → (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
        x :
      (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH2 A).f ≫ cochainsMap₂ f φ) :
          (a : (↑(shortComplexH2 A).X₁ : Type (max u u_1))) → (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
        x :
      (↑(shortComplexH2 B).X₂ : Type (max u u_1)))

Tactic:
funext g

Premises used: CategoryTheory.ShortComplex.g
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_1, u, u} k H
B : Rep.{u_1, u, u} k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : (↑(shortComplexH2 A).X₁ : Type (max u u_1))
g : G × G
⊢ Eq.{u_1 + 1} (α := (↑B : Type u_1))
    ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH2 B).f) :
          (a : (↑(shortComplexH2 A).X₁ : Type (max u u_1))) → (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
        x g :
      (↑B : Type u_1))
    ((ModuleCat.Hom.hom ((shortComplexH2 A).f ≫ cochainsMap₂ f φ) :
          (a : (↑(shortComplexH2 A).X₁ : Type (max u u_1))) → (↑(shortComplexH2 B).X₂ : Type (max u u_1)))
        x g :
      (↑B : Type u_1))

Tactic:
simp [shortComplexH2, ← hom_comm_apply φ]

Premises used: groupCohomology.shortComplexH2, Rep.hom_comm_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_1, u, u} k H
B : Rep.{u_1, u, u} k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
hf :
  ∀ (x : (↑(shortComplexH2 A).X₂ : Type (max u u_1))),
    Eq (α := (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
      ((ModuleCat.Hom.hom (cochainsMap₂ f φ ≫ (shortComplexH2 B).g) :
            (a : (↑(shortComplexH2 A).X₂ : Type (max u u_1))) → (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
          x :
        (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
      ((ModuleCat.Hom.hom ((shortComplexH2 A).g ≫ cochainsMap₃ f φ) :
            (a : (↑(shortComplexH2 A).X₂ : Type (max u u_1))) → (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
          x :
        (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
⊢ cochainsMap₂ f φ ≫ (shortComplexH2 B).g = (shortComplexH2 A).g ≫ cochainsMap₃ f φ

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_1, u, u} k H
B : Rep.{u_1, u, u} k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : (↑(shortComplexH2 A).X₂ : Type (max u u_1))
hf :
  ∀ (g : G × G × G),
    Eq.{u_1 + 1} (α := (↑B : Type u_1))
      ((ModuleCat.Hom.hom (cochainsMap₂ f φ ≫ (shortComplexH2 B).g) :
            (a : (↑(shortComplexH2 A).X₂ : Type (max u u_1))) → (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
          x g :
        (↑B : Type u_1))
      ((ModuleCat.Hom.hom ((shortComplexH2 A).g ≫ cochainsMap₃ f φ) :
            (a : (↑(shortComplexH2 A).X₂ : Type (max u u_1))) → (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
          x g :
        (↑B : Type u_1))
⊢ Eq (α := (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
    ((ModuleCat.Hom.hom (cochainsMap₂ f φ ≫ (shortComplexH2 B).g) :
          (a : (↑(shortComplexH2 A).X₂ : Type (max u u_1))) → (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH2 A).g ≫ cochainsMap₃ f φ) :
          (a : (↑(shortComplexH2 A).X₂ : Type (max u u_1))) → (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH2 B).X₃ : Type (max u u_1)))

Tactic:
funext g

Premises used: CategoryTheory.ShortComplex.g
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_1, u, u} k H
B : Rep.{u_1, u, u} k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : (↑(shortComplexH2 A).X₂ : Type (max u u_1))
g : G × G × G
⊢ Eq.{u_1 + 1} (α := (↑B : Type u_1))
    ((ModuleCat.Hom.hom (cochainsMap₂ f φ ≫ (shortComplexH2 B).g) :
          (a : (↑(shortComplexH2 A).X₂ : Type (max u u_1))) → (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
        x g :
      (↑B : Type u_1))
    ((ModuleCat.Hom.hom ((shortComplexH2 A).g ≫ cochainsMap₃ f φ) :
          (a : (↑(shortComplexH2 A).X₂ : Type (max u u_1))) → (↑(shortComplexH2 B).X₃ : Type (max u u_1)))
        x g :
      (↑B : Type u_1))

Tactic:
simp [shortComplexH2, ← hom_comm_apply φ]

Premises used: groupCohomology.shortComplexH2, Rep.hom_comm_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_1, u, u} k H
B : Rep.{u_1, u, u} k G
f : G →* H
⊢ Eq (α := shortComplexH2 A ⟶ shortComplexH2 B) (mapShortComplexH2 f 0) 0

Tactic:
rfl

Premises used: groupCohomology.mapShortComplexH2, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k H : Type u
inst : CommRing k
inst_1 : Group H
A : Rep.{u_1, u, u} k H
⊢ mapShortComplexH2 (MonoidHom.id H) (𝟙 A) = 𝟙 (shortComplexH2 A)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep.{u_1, u, u} k K
B : Rep.{u_1, u, u} k H
C : Rep.{u_1, u, u} k G
f : H →* K
g : G →* H
φ : res f A ⟶ B
ψ : res g B ⟶ C
⊢ mapShortComplexH2 (f.comp g) (CategoryTheory.Functor.map (resFunctor g) φ ≫ ψ) =
    mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ

Tactic:
rfl

Premises used: Prod.map, groupCohomology.mapShortComplexH2, CategoryTheory.ShortComplex.Hom.comp, LinearMap.compLeft, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B C : Rep.{u_1, u, u} k G
φ : A ⟶ B
ψ : B ⟶ C
⊢ mapShortComplexH2 (MonoidHom.id G) (φ ≫ ψ) =
    CategoryStruct.comp (Y := shortComplexH2 B) (mapShortComplexH2 (MonoidHom.id G) φ)
      (mapShortComplexH2 (MonoidHom.id G) ψ)

Tactic:
rfl

Premises used: Prod.map, groupCohomology.mapShortComplexH2, CategoryTheory.ShortComplex.Hom.comp, LinearMap.compLeft, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_1, u, u} k H
B : Rep.{u_1, u, u} k G
f : G →* H
φ : res f A ⟶ B
⊢ mapCocycles₂ f φ ≫ (shortComplexH2 B).moduleCatLeftHomologyData.i =
    (shortComplexH2 A).moduleCatLeftHomologyData.i ≫ cochainsMap₂ f φ

Tactic:
simp