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 : 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 (α := 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)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      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)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      H)

Tactic:
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 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 (α := 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)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨2, ⋯⟩) :
      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)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨2, ⋯⟩) :
      H)

Tactic:
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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ map f φ 0 ≫ (H0Iso B).hom ≫ (shortComplexH0 B).f = (H0Iso A).hom ≫ (shortComplexH0 A).f ≫ Hom.toModuleCatHom φ

Tactic:
simp [← cancel_epi (π _ _)]

Premises used: groupCohomology.π, CategoryTheory.cancel_epi
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
f : A ⟶ B
simp :
  (H0Iso A).hom ≫ (shortComplexH0 A).f ≫ Hom.toModuleCatHom f =
    (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f ≫ (shortComplexH0 B).f
⊢ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f

Tactic:
simp only [← cancel_mono (shortComplexH0 B).f, Category.assoc, map_H0Iso_hom_f]

Premises used: CategoryTheory.Category.assoc, groupCohomology.map_H0Iso_hom_f, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.f, groupCohomology.shortComplexH0
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
f : A ⟶ B
⊢ (H0Iso A).hom ≫ (shortComplexH0 A).f ≫ Hom.toModuleCatHom f =
    (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f ≫ (shortComplexH0 B).f

Tactic:
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_1 : Rep k H
B_1 : Rep k G
f_1 : G →* H
φ : Quiver.Hom.{?u.156077, max (?u.156077 + 1) u} (res f_1 A_1) B_1
n : ℕ
A B : Rep k G
f : A ⟶ B
inst_3 : Mono f
Z : ModuleCat k
g h : Z ⟶ groupCohomology A 0
hgh : Eq (α := Z ⟶ groupCohomology B 0) (g ≫ map (MonoidHom.id G) f 0) (h ≫ map (MonoidHom.id G) f 0)
⊢ Eq (α := Z ⟶ ModuleCat.of k ↥B.ρ.invariants)
    (g ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f)
    (h ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f)

Tactic:
simp only [← cancel_mono (H0Iso B).hom, Category.assoc, map_id_comp_H0Iso_hom] at hgh

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, groupCohomology.map_id_comp_H0Iso_hom, groupCohomology.H0Iso, CategoryTheory.Iso.hom
-- 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_1 : Rep k G
f_1 : G →* H
φ : Quiver.Hom.{?u.156077, max (?u.156077 + 1) u} (res f_1 A_1) B_1
n : ℕ
A B : Rep k G
f : A ⟶ B
inst_3 : Mono f
Z : ModuleCat k
g h : Z ⟶ groupCohomology A 0
hgh :
  Eq (α := Z ⟶ ModuleCat.of k ↥B.ρ.invariants)
    (g ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f)
    (h ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (invariantsFunctor k G) f)
⊢ g = h

Tactic:
simp_all [cancel_mono]

Premises used: CategoryTheory.cancel_mono
-- 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ cocyclesMap f φ 0 ≫ (cocyclesIso₀ B).hom ≫ (shortComplexH0 B).f =
    (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ Hom.toModuleCatHom φ

Tactic:
simp
-- 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
hf :
  ∀ (x : (↑(shortComplexH1.{u, u_1} A).X₁ : Type (max u u_1))),
    Eq (α := (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
      ((ModuleCat.Hom.hom (Hom.toModuleCatHom φ ≫ (shortComplexH1.{u, u_1} B).f) :
            (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
          x :
        (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
      ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).f ≫ cochainsMap₁ f φ) :
            (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
          x :
        (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
⊢ Hom.toModuleCatHom φ ≫ (shortComplexH1.{u, u_1} B).f = (shortComplexH1.{u, u_1} 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : (↑(shortComplexH1.{u, u_1} A).X₁ : Type (max u u_1))
hf :
  ∀ (g : G),
    Eq (α := (↑B : Type (max u u_1)))
      ((ModuleCat.Hom.hom (Hom.toModuleCatHom φ ≫ (shortComplexH1.{u, u_1} B).f) :
            (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
          x g :
        (↑B : Type (max u u_1)))
      ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).f ≫ cochainsMap₁ f φ) :
            (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
          x g :
        (↑B : Type (max u u_1)))
⊢ Eq (α := (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
    ((ModuleCat.Hom.hom (Hom.toModuleCatHom φ ≫ (shortComplexH1.{u, u_1} B).f) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₂ : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).f ≫ cochainsMap₁ f φ) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : (↑(shortComplexH1.{u, u_1} A).X₁ : Type (max u u_1))
g : G
⊢ Eq (α := (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom (Hom.toModuleCatHom φ ≫ (shortComplexH1.{u, u_1} B).f) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x g :
      (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).f ≫ cochainsMap₁ f φ) :
          (a : (↑(shortComplexH1 A).X₁ : Type (max u u_1))) → (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x g :
      (↑B : Type (max u u_1)))

Tactic:
simpa [shortComplexH1, d₀₁, cochainsMap₁] using (hom_comm_apply φ g x).symm

Premises used: groupCohomology.cochainsMap₁, groupCohomology.d₀₁, Rep.hom_comm_apply, Eq.symm, groupCohomology.shortComplexH1
-- 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
hf :
  ∀ (x : (↑(shortComplexH1.{u, u_1} A).X₂ : Type (max u u_1))),
    Eq (α := (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
      ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH1.{u, u_1} B).g) :
            (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
          x :
        (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
      ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).g ≫ cochainsMap₂ f φ) :
            (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
          x :
        (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
⊢ cochainsMap₁ f φ ≫ (shortComplexH1.{u, u_1} B).g = (shortComplexH1.{u, u_1} 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : (↑(shortComplexH1.{u, u_1} A).X₂ : Type (max u u_1))
hf :
  ∀ (g : G × G),
    Eq (α := (↑B : Type (max u u_1)))
      ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH1.{u, u_1} B).g) :
            (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
          x g :
        (↑B : Type (max u u_1)))
      ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).g ≫ cochainsMap₂ f φ) :
            (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
          x g :
        (↑B : Type (max u u_1)))
⊢ Eq (α := (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
    ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH1.{u, u_1} B).g) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} B).X₃ : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).g ≫ cochainsMap₂ f φ) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : (↑(shortComplexH1.{u, u_1} A).X₂ : Type (max u u_1))
g : G × G
⊢ Eq (α := (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH1.{u, u_1} B).g) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x g :
      (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).g ≫ cochainsMap₂ f φ) :
          (a : (↑(shortComplexH1 A).X₂ : Type (max u u_1))) → (↑(shortComplexH1 B).X₃ : Type (max u u_1)))
        x g :
      (↑B : Type (max u u_1)))

Tactic:
simpa [shortComplexH1, d₁₂, cochainsMap₁, cochainsMap₂] using (hom_comm_apply φ _ _).symm

Premises used: groupCohomology.cochainsMap₁, groupCohomology.d₁₂, groupCohomology.cochainsMap₂, Rep.hom_comm_apply, Eq.symm, groupCohomology.shortComplexH1
-- 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 k H
B : Rep k G
f : G →* H
⊢ Eq (α := shortComplexH1.{u, u_1} A ⟶ shortComplexH1.{u, u_1} B) (mapShortComplexH1 f 0) 0

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k H : Type u
inst : CommRing k
inst_1 : Group H
A : Rep k H
⊢ mapShortComplexH1 (MonoidHom.id H) (𝟙 A) = 𝟙 (shortComplexH1.{u, u_1} 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 k K
B : Rep k H
C : Rep k G
f : H →* K
g : G →* H
φ : res f A ⟶ B
ψ : res g B ⟶ C
⊢ mapShortComplexH1 (f.comp g) (CategoryTheory.Functor.map (resFunctor g) φ ≫ ψ) =
    mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ

Tactic:
rfl

Premises used: groupCohomology.mapShortComplexH1, Prod.map, 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 k G
φ : A ⟶ B
ψ : B ⟶ C
⊢ mapShortComplexH1 (MonoidHom.id G) (φ ≫ ψ) =
    CategoryStruct.comp (Y := shortComplexH1.{u, u_1} B) (mapShortComplexH1 (MonoidHom.id G) φ)
      (mapShortComplexH1 (MonoidHom.id G) ψ)

Tactic:
rfl

Premises used: groupCohomology.mapShortComplexH1, Prod.map, 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ mapCocycles₁.{u, u_1} f φ ≫ (shortComplexH1.{u, u_1} B).moduleCatLeftHomologyData.i =
    (shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.i ≫ cochainsMap₁ f φ

Tactic:
simp
-- 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : (↑(ModuleCat.of k ↥(cocycles₁ A)) : Type (max u u_1))
⊢ Eq (α := (a : G) → (↑B : Type (max u u_1)))
    (⇑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
                (CC := ModuleCat.carrier) (mapCocycles₁.{u, u_1} f φ) :
              (a : (↑(ModuleCat.of k ↥(cocycles₁ A)) : Type (max u u_1))) →
                (↑(ModuleCat.of k ↥(cocycles₁ B)) : Type (max u u_1)))
            x :
          (↑(ModuleCat.of k ↥(cocycles₁ B)) : Type (max u u_1))) :
      (a : G) → (↑B : Type (max u u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (cochainsMap₁ f φ) :
        (a : (↑(ModuleCat.of k (H → (↑A : Type (max u u_1)))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G → (↑B : Type (max u u_1)))) : Type (max u u_1)))
      (⇑x : (a : H) → (↑A : Type (max u u_1))))

Tactic:
rfl

Premises used: 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ cocyclesMap f φ 1 ≫ (isoCocycles₁ B).hom = (isoCocycles₁ A).hom ≫ mapCocycles₁ f φ

Tactic:
simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, groupCohomology.shortComplexH1, CategoryTheory.ShortComplex.LeftHomologyData.i
-- 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 k H
B : Rep k G
φ : res 1 A ⟶ B
rw :
  (shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂ =
    0 ≫ (shortComplexH1.{u, u_1} B).moduleCatLeftHomologyData.i
⊢ mapCocycles₁.{u, u_1} 1 φ = 0

Tactic:
rw [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, cyclesMap'_i]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, CategoryTheory.ShortComplex.cyclesMap'_i, groupCohomology.shortComplexH1, CategoryTheory.ShortComplex.LeftHomologyData.i
-- 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 k H
B : Rep k G
φ : res 1 A ⟶ B
⊢ (shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂ =
    0 ≫ (shortComplexH1.{u, u_1} B).moduleCatLeftHomologyData.i

Tactic:
ModuleCat.hom_ext (LinearMap.ext fun _ ↦ funext fun y => ?_)

Premises used: LinearMap.ext, Set.Mem, funext, ModuleCat.hom_ext, groupCohomology.cocycles₁
-- 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 k H
B : Rep k G
φ : res 1 A ⟶ B
refine :
  ∀ (x : (↑(shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.K : Type (max u u_1))) (y : G),
    Eq (α := (↑B : Type (max u u_1)))
      ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂) :
            (a : (↑(shortComplexH1 A).moduleCatLeftHomologyData.K : Type (max u u_1))) →
              (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
          x y :
        (↑B : Type (max u u_1)))
      ((ModuleCat.Hom.hom (0 ≫ (shortComplexH1.{u, u_1} B).moduleCatLeftHomologyData.i) :
            (a : (↑(shortComplexH1 A).moduleCatLeftHomologyData.K : Type (max u u_1))) →
              (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
          x y :
        (↑B : Type (max u u_1)))
⊢ (shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂ =
    0 ≫ (shortComplexH1.{u, u_1} B).moduleCatLeftHomologyData.i

Tactic:
refine ModuleCat.hom_ext (LinearMap.ext fun _ ↦ funext fun y => ?_)

Premises used: LinearMap.ext, ModuleCat.hom_ext
-- 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 k H
B : Rep k G
φ : res 1 A ⟶ B
x : (↑(shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.K : Type (max u u_1))
y : G
⊢ Eq (α := (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom ((shortComplexH1.{u, u_1} A).moduleCatLeftHomologyData.i ≫ (mapShortComplexH1 1 φ).τ₂) :
          (a : (↑(shortComplexH1 A).moduleCatLeftHomologyData.K : Type (max u u_1))) →
            (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x y :
      (↑B : Type (max u u_1)))
    ((ModuleCat.Hom.hom (0 ≫ (shortComplexH1.{u, u_1} B).moduleCatLeftHomologyData.i) :
          (a : (↑(shortComplexH1 A).moduleCatLeftHomologyData.K : Type (max u u_1))) →
            (↑(shortComplexH1 B).X₂ : Type (max u u_1)))
        x y :
      (↑B : Type (max u u_1)))

Tactic:
simp [mapShortComplexH1, shortComplexH1, Pi.zero_apply y]

Premises used: groupCohomology.mapShortComplexH1, Pi.zero_apply, groupCohomology.shortComplexH1
-- 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 k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ H1π A ≫ map f φ 1 = mapCocycles₁ f φ ≫ H1π B

Tactic:
simp [H1π, Iso.inv_comp_eq, ← cocyclesMap_comp_isoCocycles₁_hom_assoc]

Premises used: CategoryTheory.Iso.inv_comp_eq, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, groupCohomology.H1π
-- 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 k H
B : Rep k G
φ : res 1 A ⟶ B
⊢ Eq (α := groupCohomology A 1 ⟶ groupCohomology B 1) (map 1 φ 1) 0

Tactic:
simp [← cancel_epi (H1π _)]

Premises used: groupCohomology.H1π, CategoryTheory.cancel_epi
-- 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.259726, max (?u.259726 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
rw :
  Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
      (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S)) ≫
        𝟙 (res S.subtype A))
      1)
    0
rw₁ :
  Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (MonoidHom.comp (QuotientGroup.mk' S) S.subtype)
      (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S))) 1)
    0
rw₂ :
  Eq.{u + 1} (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map 1
      (Eq.rec (motive := fun (x : ↥S →* G ⧸ S) (h : MonoidHom.comp (QuotientGroup.mk' S) S.subtype = x) ↦
        res x (A.quotientToInvariants S) ⟶ res S.subtype A)
        (CategoryTheory.Functor.map (resFunctor S.subtype) (ofHom (A.ρ.quotientToInvariants_lift S))) ⋯)
      1)
    0
rw₃ rw₄ : Eq.{u + 1} (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1) 0 0
⊢ Eq (α := groupCohomology (A.quotientToInvariants S) 1 ⟶ groupCohomology (res S.subtype A) 1)
    (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1 ≫ map S.subtype (𝟙 (res S.subtype A)) 1) 0

Tactic:
rw [← map_comp, Category.comp_id, congr (QuotientGroup.mk'_comp_subtype S)
    (fun f φ => map f φ 1), map₁_one]

Premises used: groupCohomology.map, groupCohomology.congr, groupCohomology.map_comp, groupCohomology.map₁_one, QuotientGroup.mk'_comp_subtype, CategoryTheory.Category.comp_id, OfNat.ofNat
-- 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
rw :
  ∀ (a : (↑(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) (H1InfRes A S).f :
              (a : (↑(H1InfRes A S).X₁ : Type u)) → (↑(H1InfRes A S).X₂ : Type u))
            a :
          (↑(H1InfRes A S).X₂ : Type u))
        (0 : (↑(H1InfRes A S).X₂ : Type u)) →
      a = 0
⊢ Mono (H1InfRes A S).f

Tactic:
rw [ModuleCat.mono_iff_injective, injective_iff_map_eq_zero]

Premises used: ModuleCat.mono_iff_injective, injective_iff_map_eq_zero