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
rw :
  ∀ (x₂ : (↑(shortComplexH0.{u, u_1} A).X₂ : Type (max u u_1))),
    Eq (α := (↑(shortComplexH0.{u, u_1} A).X₃ : 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)
                (shortComplexH0.{u, u_1} A).g :
              (a : (↑(shortComplexH0 A).X₂ : Type (max u u_1))) → (↑(shortComplexH0 A).X₃ : Type (max u u_1)))
            x₂ :
          (↑(shortComplexH0.{u, u_1} A).X₃ : Type (max u u_1)))
        (0 : (↑(shortComplexH0.{u, u_1} A).X₃ : Type (max u u_1))) →
      ∃ (x₁ : (↑(shortComplexH0.{u, u_1} A).X₁ : 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)
                (shortComplexH0.{u, u_1} A).f :
              (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
            x₁ =
          x₂
⊢ (shortComplexH0.{u, u_1} A).Exact

Tactic:
rw [ShortComplex.moduleCat_exact_iff]

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type (max u u_1))
d₀₁ :
  ∀
    (hx :
      Eq (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦
                (↑x1 : Type (max u_1 u)) →ₗ[k] (↑x2 : Type (max u_1 u))) (CC := ModuleCat.carrier)
                (groupCohomology.d₀₁.{u, u_1} A) :
              (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u_1 u))) →
                (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
            x :
          (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
        (0 : (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))),
    ∃ (x₁ : (↑(shortComplexH0.{u, u_1} A).X₁ : 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) (shortComplexH0.{u, u_1} A).f :
            (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
          x₁ =
        x
⊢ Eq (α := (↑(shortComplexH0.{u, u_1} A).X₃ : 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) (shortComplexH0.{u, u_1} A).g :
            (a : (↑(shortComplexH0 A).X₂ : Type (max u u_1))) → (↑(shortComplexH0 A).X₃ : Type (max u u_1)))
          x :
        (↑(shortComplexH0.{u, u_1} A).X₃ : Type (max u u_1)))
      (0 : (↑(shortComplexH0.{u, u_1} A).X₃ : Type (max u u_1))) →
    ∃ (x₁ : (↑(shortComplexH0.{u, u_1} A).X₁ : 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) (shortComplexH0.{u, u_1} A).f :
            (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
          x₁ =
        x

Tactic:
(hx : d₀₁ _ x = 0)
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type (max u u_1))
hx :
  Eq (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u_1 u)) →ₗ[k] (↑x2 : Type (max u_1 u)))
            (CC := ModuleCat.carrier) (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u_1 u))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
        x :
      (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    (0 : (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
⊢ ∃ (x₁ : (↑(shortComplexH0.{u, u_1} A).X₁ : 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) (shortComplexH0.{u, u_1} A).f :
          (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
        x₁ =
      x

Tactic:
⟨⟨x, fun g => ?_⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type (max u u_1))
hx :
  Eq (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u_1 u)) →ₗ[k] (↑x2 : Type (max u_1 u)))
            (CC := ModuleCat.carrier) (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u_1 u))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
        x :
      (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    (0 : (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
refine :
  ∀ (g : G),
    (((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
            (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
          (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
        x =
      x
⊢ ∃ (x₁ : (↑(shortComplexH0.{u, u_1} A).X₁ : 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) (shortComplexH0.{u, u_1} A).f :
          (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
        x₁ =
      x

Tactic:
refine ⟨⟨x, fun g => ?_⟩, rfl⟩
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type (max u u_1))
hx :
  Eq (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u_1 u)) →ₗ[k] (↑x2 : Type (max u_1 u)))
            (CC := ModuleCat.carrier) (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u_1 u))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
        x :
      (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    (0 : (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
g : G
rw :
  HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          x :
        (↑A : Type (max u u_1)))
      x =
    0
⊢ (((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
          (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
        (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
      x =
    x

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type (max u u_1))
hx :
  Eq (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u_1 u)) →ₗ[k] (↑x2 : Type (max u_1 u)))
            (CC := ModuleCat.carrier) (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u_1 u))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
        x :
      (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    (0 : (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
g : G
⊢ HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          x :
        (↑A : Type (max u u_1)))
      x =
    0

Tactic:
congr_fun hx g

Premises used: congr_fun
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type (max u u_1))
hx :
  Eq (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u_1 u)) →ₗ[k] (↑x2 : Type (max u_1 u)))
            (CC := ModuleCat.carrier) (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u_1 u))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
        x :
      (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
    (0 : (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u_1 u)))
g : G
⊢ HSub.hSub (α := (↑A : Type (max u u_1)))
      ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
              (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
            (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
          x :
        (↑A : Type (max u u_1)))
      x =
    0

Tactic:
exact congr_fun hx g

Premises used: congr_fun
-- 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 0 = 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
dsimp :
  (KernelFork.ofι (HomologicalComplex.iCycles (inhomogeneousCochains A) 0) ⋯).mapOfIsLimit ⋯.fIsKernel
        (dArrowIso₀₁ A).hom ≫
      (shortComplexH0 A).f =
    iCocycles A 0 ≫ (cochainsIso₀ A).hom
⊢ (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f = iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
dsimp [cocyclesIso₀]

Premises used: groupCohomology.cocyclesIso₀
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (KernelFork.ofι (HomologicalComplex.iCycles (inhomogeneousCochains A) 0) ⋯).mapOfIsLimit ⋯.fIsKernel
        (dArrowIso₀₁ A).hom ≫
      (shortComplexH0 A).f =
    iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
apply KernelFork.mapOfIsLimit_ι

Premises used: CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
rw : iCocycles A 0 = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv
rw₁ : iCocycles A 0 = ((cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f) ≫ (cochainsIso₀ A).inv
rw₂ : iCocycles A 0 ≫ (cochainsIso₀ A).hom = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f
rw₃ rw₄ : iCocycles A 0 ≫ (cochainsIso₀ A).hom = iCocycles A 0 ≫ (cochainsIso₀ A).hom
⊢ (cocyclesIso₀ A).inv ≫ iCocycles A 0 = (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, cocyclesIso₀_hom_comp_f]

Premises used: CategoryTheory.Category.assoc, groupCohomology.cocyclesIso₀_hom_comp_f, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥A.ρ.invariants
h :
  ∀ (g : Fin (HAdd.hAdd (α := ℕ) 0 1) → G),
    Eq (α := (↑A : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 0) :
            (a : (↑(ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) : Type u)) →
              (↑(ModuleCat.of k ((Fin (0 + 1) → G) → (↑A : Type u))) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (cochainsIso₀ A).inv :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
              (↑x : (↑A : Type u)) :
            (↑((inhomogeneousCochains A).X 0) : Type u))
          g :
        (↑A : Type u))
      (0 g : (↑A : Type u))
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 0 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 0) :
          (a : (↑(ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (0 + 1) → G) → (↑A : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ A).inv :
              (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
            (↑x : (↑A : Type u)) :
          (↑((inhomogeneousCochains A).X 0) : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 0 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 0 1) → G) → (↑A : Type u))) : Type u))

Tactic:
ext g

Premises used: CategoryTheory.ShortComplex.g
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥A.ρ.invariants
g : Fin (HAdd.hAdd (α := ℕ) 0 1) → G
⊢ Eq (α := (↑A : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 0) :
          (a : (↑(ModuleCat.of k ((Fin 0 → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (0 + 1) → G) → (↑A : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ A).inv :
              (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
            (↑x : (↑A : Type u)) :
          (↑((inhomogeneousCochains A).X 0) : Type u))
        g :
      (↑A : Type u))
    (0 g : (↑A : Type u))

Tactic:
simp [cochainsIso₀, x.2 (g 0),
      inhomogeneousCochains.d, Pi.zero_apply (M := fun _ => A)]

Premises used: inhomogeneousCochains.d, groupCohomology.cochainsIso₀, Pi.zero_apply, OfNat.ofNat, Subtype.property
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥A.ρ.invariants
rw :
  Eq (α := (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₀ A).inv :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        (↑x : (↑A : Type u)) :
      (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 0) (iCocycles A 0) :
          (a : (↑(cocycles A 0) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cocyclesIso₀ A).inv :
              (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type u)) → (↑(cocycles A 0) : Type u))
            x :
          (↑(cocycles A 0) : Type u)) :
      (↑((inhomogeneousCochains A).X 0) : Type u))
⊢ Eq (α := (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 0) (iCocycles A 0) :
          (a : (↑(cocycles A 0) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        (cocyclesMk
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ A).inv :
              (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
            (↑x : (↑A : Type u)))
          ⋯) :
      (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 0) (iCocycles A 0) :
          (a : (↑(cocycles A 0) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cocyclesIso₀ A).inv :
              (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type u)) → (↑(cocycles A 0) : Type u))
            x :
          (↑(cocycles A 0) : Type u)) :
      (↑((inhomogeneousCochains A).X 0) : Type u))

Tactic:
rw [iCocycles_mk]

Premises used: groupCohomology.iCocycles_mk
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥A.ρ.invariants
⊢ Eq (α := (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₀ A).inv :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        (↑x : (↑A : Type u)) :
      (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 0) (iCocycles A 0) :
          (a : (↑(cocycles A 0) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cocyclesIso₀ A).inv :
              (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type u)) → (↑(cocycles A 0) : Type u))
            x :
          (↑(cocycles A 0) : Type u)) :
      (↑((inhomogeneousCochains A).X 0) : Type u))

Tactic:
(cocyclesIso₀_inv_comp_iCocycles_apply A x).symm

Premises used: groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, Eq.symm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥A.ρ.invariants
⊢ Eq (α := (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₀ A).inv :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        (↑x : (↑A : Type u)) :
      (↑((inhomogeneousCochains A).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cocycles A 0) (iCocycles A 0) :
          (a : (↑(cocycles A 0) : Type u)) → (↑((inhomogeneousCochains A).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cocyclesIso₀ A).inv :
              (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type u)) → (↑(cocycles A 0) : Type u))
            x :
          (↑(cocycles A 0) : Type u)) :
      (↑((inhomogeneousCochains A).X 0) : Type u))

Tactic:
exact (cocyclesIso₀_inv_comp_iCocycles_apply A x).symm

Premises used: groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, Eq.symm
-- 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 1 = 0

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 1 = 2

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 ≫ (shortComplexH1 A).moduleCatLeftHomologyData.i = iCocycles A 1 ≫ (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 1 = (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv

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

Premises used: Set.Mem, CategoryTheory.CommSq.horiz_inv, CategoryTheory.CommSq.mk, groupCohomology.isoCocycles₁_hom_comp_i, 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 0 1 ≫ (isoCocycles₁ A).hom = (cochainsIso₀ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.f'

Tactic:
simp [← cancel_mono (shortComplexH1 A).moduleCatLeftHomologyData.i, comp_d₀₁_eq,
    shortComplexH1_f]

Premises used: groupCohomology.shortComplexH1_f, groupCohomology.comp_d₀₁_eq, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, groupCohomology.shortComplexH1, CategoryTheory.ShortComplex.LeftHomologyData.i