awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ Function.Injective (α :=
    (↑(Functor.obj
          (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (HomologicalComplex.cycles (inhomogeneousCochains A) 1)) :
      Type u))
    (β :=
    (↑(Functor.obj
          (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          ((inhomogeneousCochains A).X 1)) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (X :=
          Functor.obj
            (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            (HomologicalComplex.cycles (inhomogeneousCochains A) 1))
          (CategoryTheory.Functor.map
            (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            (HomologicalComplex.iCycles (inhomogeneousCochains A) 1))) :
      (a : (↑((forget₂ (ModuleCat k) Ab).obj (HomologicalComplex.cycles (inhomogeneousCochains A) 1)) : Type u)) →
        (↑((forget₂ (ModuleCat k) Ab).obj ((inhomogeneousCochains A).X 1)) : Type u))

Tactic:
(AddCommGrpCat.mono_iff_injective _).1 <| (forget₂ _ _).map_mono _

Premises used: CategoryTheory.Functor.map_mono, AddCommGrpCat.mono_iff_injective, CategoryTheory.forget₂, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ Eq (α := (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv) :
          (a : ↥(cocycles₁ A)) → (Fin 1 → G) → (↑A : Type u))
        x :
      (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 1) (iCocycles A 1) :
          (a : (↑(cocycles A 1) : Type u)) → (Fin 1 → G) → (↑A : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (isoCocycles₁ A).inv :
              (a : ↥(cocycles₁ A)) → (↑(cocycles A 1) : Type u))
            x :
          (↑(cocycles A 1) : Type u)) :
      (Fin 1 → G) → (↑A : Type u))

Tactic:
have := (isoCocycles₁_inv_comp_iCocycles_apply _ x).symm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
this :
  Eq (α := (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv) :
          (a : ↥(cocycles₁ A)) → (Fin 1 → G) → (↑A : Type u))
        x :
      (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 1) (iCocycles A 1) :
          (a : (↑(cocycles A 1) : Type u)) → (Fin 1 → G) → (↑A : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (isoCocycles₁ A).inv :
              (a : ↥(cocycles₁ A)) → (↑(cocycles A 1) : Type u))
            x :
          (↑(cocycles A 1) : Type u)) :
      (Fin 1 → G) → (↑A : Type u))
rw :
  Eq (α := (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₁ A).inv :
          (a : G → (↑A : Type u)) → (Fin 1 → G) → (↑A : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv) :
          (a : ↥(cocycles₁ A)) → (Fin 1 → G) → (↑A : Type u))
        x :
      (Fin 1 → G) → (↑A : Type u))
⊢ Eq (α := (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₁ A).inv :
          (a : G → (↑A : Type u)) → (Fin 1 → G) → (↑A : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (Fin 1 → G) → (↑A : Type u))
    ((ModuleCat.Hom.hom (HomologicalComplex.iCycles (inhomogeneousCochains A) 1) :
          (a : (↑(HomologicalComplex.cycles (inhomogeneousCochains A) 1) : Type u)) → (Fin 1 → G) → (↑A : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (isoCocycles₁ A).inv :
              (a : ↥(cocycles₁ A)) → (↑(cocycles A 1) : Type u))
            x :
          (↑(cocycles A 1) : Type u)) :
      (Fin 1 → G) → (↑A : Type u))

Tactic:
rw [← this]
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
this :
  Eq (α := (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv) :
          (a : ↥(cocycles₁ A)) → (Fin 1 → G) → (↑A : Type u))
        x :
      (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 1) (iCocycles A 1) :
          (a : (↑(cocycles A 1) : Type u)) → (Fin 1 → G) → (↑A : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (isoCocycles₁ A).inv :
              (a : ↥(cocycles₁ A)) → (↑(cocycles A 1) : Type u))
            x :
          (↑(cocycles A 1) : Type u)) :
      (Fin 1 → G) → (↑A : Type u))
⊢ Eq (α := (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₁ A).inv :
          (a : G → (↑A : Type u)) → (Fin 1 → G) → (↑A : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (Fin 1 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv) :
          (a : ↥(cocycles₁ A)) → (Fin 1 → G) → (↑A : Type u))
        x :
      (Fin 1 → G) → (↑A : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (ComplexShape.up ℕ).prev 2 = 1

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (ComplexShape.up ℕ).next 2 = 3

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (isoCocycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.i = iCocycles A 2 ≫ (cochainsIso₂ A).hom

Tactic:
simp [isoCocycles₂, iCocycles, HomologicalComplex.iCycles, iCycles]

Premises used: HomologicalComplex.iCycles, groupCohomology.isoCocycles₂, groupCohomology.iCocycles, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (isoCocycles₂ A).inv ≫ iCocycles A 2 = (shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₂ A).inv

Tactic:
(CommSq.horiz_inv ⟨isoCocycles₂_hom_comp_i A⟩).w

Premises used: Set.Mem, CategoryTheory.CommSq.horiz_inv, groupCohomology.isoCocycles₂_hom_comp_i, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w, groupCohomology.cocycles₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ toCocycles A 1 2 ≫ (isoCocycles₂ A).hom = (cochainsIso₁ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.f'

Tactic:
simp [← cancel_mono (shortComplexH2 A).moduleCatLeftHomologyData.i, comp_d₁₂_eq,
    shortComplexH2_f]

Premises used: groupCohomology.comp_d₁₂_eq, groupCohomology.shortComplexH2, groupCohomology.shortComplexH2_f, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ Function.Injective (α :=
    (↑(Functor.obj
          (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (HomologicalComplex.cycles (inhomogeneousCochains A) 2)) :
      Type u))
    (β :=
    (↑(Functor.obj
          (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          ((inhomogeneousCochains A).X 2)) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (X :=
          Functor.obj
            (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            (HomologicalComplex.cycles (inhomogeneousCochains A) 2))
          (CategoryTheory.Functor.map
            (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            (HomologicalComplex.iCycles (inhomogeneousCochains A) 2))) :
      (a : (↑((forget₂ (ModuleCat k) Ab).obj (HomologicalComplex.cycles (inhomogeneousCochains A) 2)) : Type u)) →
        (↑((forget₂ (ModuleCat k) Ab).obj ((inhomogeneousCochains A).X 2)) : Type u))

Tactic:
(AddCommGrpCat.mono_iff_injective _).1 <| (forget₂ _ _).map_mono _

Premises used: CategoryTheory.Functor.map_mono, AddCommGrpCat.mono_iff_injective, CategoryTheory.forget₂, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ Eq (α := (Fin 2 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₂ A).inv :
          (a : G × G → (↑A : Type u)) → (Fin 2 → G) → (↑A : Type u))
        (⇑x : (a : G × G) → (↑A : Type u)) :
      (Fin 2 → G) → (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₂ A).inv) :
          (a : ↥(cocycles₂ A)) → (Fin 2 → G) → (↑A : Type u))
        x :
      (Fin 2 → G) → (↑A : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ π A 0 ≫ (H0Iso A).hom = (cocyclesIso₀ A).hom

Tactic:
simp [H0Iso]

Premises used: groupCohomology.H0Iso
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
C : (↑(H0 A) : Type u) → Prop
x : (↑(H0 A) : Type u)
h :
  ∀ (x : ↥A.ρ.invariants),
    C
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H0Iso A).inv :
          (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type u)) → (↑(H0 A) : Type u))
        x)
⊢ C x

Tactic:
simpa using h ((H0Iso A).hom x)

Premises used: CategoryTheory.ConcreteCategory.hom, groupCohomology.H0Iso, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ (H0IsoOfIsTrivial A).hom = (H0Iso A).hom ≫ (shortComplexH0 A).f

Tactic:
rfl

Premises used: Submodule.subtype, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ π A 0 ≫ (H0IsoOfIsTrivial A).hom = iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
x : (↑A : Type u)
⊢ x ∈ A.ρ.invariants

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
x : (↑A : Type u)
⊢ Eq (α := (↑(H0 A) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H0IsoOfIsTrivial A).inv :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑(H0 A) : Type u))
        x :
      (↑(H0 A) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H0Iso A).inv :
          (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type u)) → (↑(H0 A) : Type u))
        (Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ A.ρ.invariants) x ⋯) :
      (↑(H0 A) : Type u))

Tactic:
rfl

Premises used: dite, ComplexShape.next, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Epi (H1π A)

Tactic:
inferInstanceAs <| Epi (_ ≫ _)

Premises used: _private.0.groupCohomology.instEpiModuleCatH1π._proof_1
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ Eq (α :=
    (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 1).homology)
    ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)
    (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)

Tactic:
have h := leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv
    (shortComplexH1 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousCochains A).sc 1).leftHomologyIso.hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
h :
  Eq (α :=
    (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 1).homology)
    ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)
    (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)
simp :
  Eq (α := (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
      ((ModuleCat.Hom.hom (shortComplexH1 A).moduleCatLeftHomologyData.π :
            (a : ↥(cocycles₁ A)) → (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
          x :
        (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
      (0 : (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u)) ↔
    (⇑x : (a : G) → (↑A : Type u)) ∈ coboundaries₁ A
⊢ Eq (α := (↑(H1 A) : Type u))
      ((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))
      (0 : (↑(H1 A) : Type u)) ↔
    (⇑x : (a : G) → (↑A : Type u)) ∈ coboundaries₁ A

Tactic:
simp only [H1π, isoCocycles₁, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.ShortComplex.cyclesMapIso'_inv, inferInstance, ModuleCat.mono_iff_injective, groupCohomology.H1π, LinearMap.coe_comp, map_eq_zero_iff, groupCohomology.isoCocycles₁, CategoryTheory.ShortComplex.leftHomologyMapIso'_inv, Iff.mp, groupCohomology.π, Function.comp_apply, ModuleCat.hom_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
h :
  Eq (α :=
    (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 1).homology)
    ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)
    (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)
⊢ Eq (α := (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
      ((ModuleCat.Hom.hom (shortComplexH1 A).moduleCatLeftHomologyData.π :
            (a : ↥(cocycles₁ A)) → (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
          x :
        (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
      (0 : (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u)) ↔
    (⇑x : (a : G) → (↑A : Type u)) ∈ coboundaries₁ A

Tactic:
simp [LinearMap.range_codRestrict, coboundaries₁, shortComplexH1, cocycles₁]

Premises used: groupCohomology.coboundaries₁, groupCohomology.cocycles₁, LinearMap.range_codRestrict, groupCohomology.shortComplexH1
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cocycles₁ A)
rw :
  (⇑(x - y) : (a : G) → (↑A : Type u)) ∈ coboundaries₁ A ↔
    HSub.hSub (α := (a : G) → (↑A : Type u)) (⇑x : (a : G) → (↑A : Type u)) (⇑y : (a : G) → (↑A : Type u)) ∈
      coboundaries₁ A
⊢ Eq (α := (↑(H1 A) : Type u))
      ((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))
      ((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))
          y :
        (↑(H1 A) : Type u)) ↔
    HSub.hSub (α := (a : G) → (↑A : Type u)) (⇑x : (a : G) → (↑A : Type u)) (⇑y : (a : G) → (↑A : Type u)) ∈
      coboundaries₁ A

Tactic:
rw [← sub_eq_zero, ← map_sub, H1π_eq_zero_iff]

Premises used: map_sub, sub_eq_zero, groupCohomology.H1π_eq_zero_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cocycles₁ A)
⊢ (⇑(x - y) : (a : G) → (↑A : Type u)) ∈ coboundaries₁ A ↔
    HSub.hSub (α := (a : G) → (↑A : Type u)) (⇑x : (a : G) → (↑A : Type u)) (⇑y : (a : G) → (↑A : Type u)) ∈
      coboundaries₁ A

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
C : (↑(H1 A) : Type u) → Prop
x : (↑(H1 A) : Type u)
h :
  ∀ (x : ↥(cocycles₁ A)),
    C
      ((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)
y : (↑(cocycles A 1) : Type u)
⊢ C
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := cocycles A 1) (π A 1) :
        (a : (↑(cocycles A 1) : Type u)) → (↑(groupCohomology A 1) : Type u))
      y)

Tactic:
simpa [H1π] using h ((isoCocycles₁ A).hom y)

Premises used: CategoryTheory.ConcreteCategory.hom, groupCohomology.H1π, groupCohomology.isoCocycles₁, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ π A 1 ≫ (H1Iso A).hom = (isoCocycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π

Tactic:
simp [H1Iso, isoCocycles₁, π, HomologicalComplex.homologyπ, leftHomologyπ]

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.leftHomologyπ, groupCohomology.H1Iso, groupCohomology.isoCocycles₁, groupCohomology.π