awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep.{u_1, u, u} k G)
hX : X.ShortExact
y : G → (↑X.X₂ : Type u_1)
x : G × G → (↑X.X₁ : Type u_1)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u_1)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u_1))) : Type (max u u_1)))
      y)
⊢ Eq (α := (↑(shortComplexH2 X.X₂).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) (X := X₂ (shortComplexH2.{u, u_1} (G := G) X.1)) (Y := (shortComplexH2 X.X₂).X₃)
            (g (shortComplexH2.{u, u_1} (G := G) X.1) ≫ Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) X.f)) :
          (a : (↑(shortComplexH2 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH2 X.X₂).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) (X := X₂ (shortComplexH2.{u, u_1} (G := G) X.1))
            (Hom.τ₂ (mapShortComplexH2 (MonoidHom.id G) X.f) ≫ (shortComplexH2 X.X₂).g) :
          (a : (↑(shortComplexH2 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))

Tactic:
have := congr($((mapShortComplexH2 (MonoidHom.id G) X.f).comm₂₃.symm) x)
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep.{u_1, u, u} k G)
hX : X.ShortExact
y : G → (↑X.X₂ : Type u_1)
x : G × G → (↑X.X₁ : Type u_1)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u_1)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u_1))) : Type (max u u_1)))
      y)
this :
  Eq (α := (↑(shortComplexH2 X.X₂).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) (X := X₂ (shortComplexH2.{u, u_1} (G := G) X.1)) (Y := (shortComplexH2 X.X₂).X₃)
            (g (shortComplexH2.{u, u_1} (G := G) X.1) ≫ Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) X.f)) :
          (a : (↑(shortComplexH2 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH2 X.X₂).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) (X := X₂ (shortComplexH2.{u, u_1} (G := G) X.1))
            (Hom.τ₂ (mapShortComplexH2 (MonoidHom.id G) X.f) ≫ (shortComplexH2 X.X₂).g) :
          (a : (↑(shortComplexH2 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH2 X.X₂).X₃ : Type (max u u_1)))
⊢ Eq (α := G × G × G → (↑X.X₂ : Type u_1))
    ((fun (x : G × G × G → (↑X.X₁ : Type u_1)) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x : G × G × G → (↑X.X₂ : Type u_1)))
      ((ModuleCat.Hom.hom (d₂₃ X.X₁) :
          (a : G × G → (↑X.X₁ : Type u_1)) → (↑(ModuleCat.of k (G × G × G → (↑X.X₁ : Type u_1))) : Type (max u u_1)))
        x))
    ((fun (x : G × G × G → (↑X.X₁ : Type u_1)) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u_1)) → (↑X.X₂ : Type u_1)) ∘ x : G × G × G → (↑X.X₂ : Type u_1)))
      0)

Tactic:
simp_all [shortComplexH2, LinearMap.compLeft]

Premises used: groupCohomology.shortComplexH2, LinearMap.compLeft
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → (↑X.X₂ : Type u)
hy :
  Eq (α := G → (↑X.X₃ : Type u)) ((⇑(Rep.Hom.hom X.g) : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) ∘ y)
    (⇑z : (a : G) → (↑X.X₃ : Type u))
x : G × G → (↑X.X₁ : Type u)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u))) : Type u))
      y)
rw :
  Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
    ((ModuleCat.Hom.hom (d₁₂ X.X₃ ≫ (cochainsIso₂ X.X₃).inv) :
          (a : (↑(ModuleCat.of k (G → (↑X.X₃ : Type u))) : Type u)) →
            (↑((inhomogeneousCochains X.X₃).X (1 + 1)) : Type u))
        (⇑z : (a : G) → (↑X.X₃ : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
⊢ Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousCochains X.X₃).X 1) (Y :=
            (inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1))
            ((inhomogeneousCochains X.X₃).d 1 (HAdd.hAdd (α := ℕ) 1 1)) :
          (a : (↑((inhomogeneousCochains X.X₃).X 1) : Type u)) → (↑((inhomogeneousCochains X.X₃).X (1 + 1)) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₁ X.X₃).inv :
              (a : (↑(ModuleCat.of k (G → (↑X.X₃ : Type u))) : Type u)) →
                (↑((inhomogeneousCochains X.X₃).X 1) : Type u))
            (⇑z : (a : G) → (↑X.X₃ : Type u)) :
          (↑((inhomogeneousCochains X.X₃).X 1) : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]

Premises used: groupCohomology.eq_d₁₂_comp_inv, LinearMap.comp_apply, ModuleCat.hom_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → (↑X.X₂ : Type u)
hy :
  Eq (α := G → (↑X.X₃ : Type u)) ((⇑(Rep.Hom.hom X.g) : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) ∘ y)
    (⇑z : (a : G) → (↑X.X₃ : Type u))
x : G × G → (↑X.X₁ : Type u)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u))) : Type u))
      y)
⊢ Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
    ((ModuleCat.Hom.hom (d₁₂ X.X₃ ≫ (cochainsIso₂ X.X₃).inv) :
          (a : (↑(ModuleCat.of k (G → (↑X.X₃ : Type u))) : Type u)) →
            (↑((inhomogeneousCochains X.X₃).X (1 + 1)) : Type u))
        (⇑z : (a : G) → (↑X.X₃ : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 1 1)) : Type u))

Tactic:
simp [cocycles₁.d₁₂_apply z]

Premises used: groupCohomology.cocycles₁.d₁₂_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → (↑X.X₂ : Type u)
hy :
  Eq (α := G → (↑X.X₃ : Type u)) ((⇑(Rep.Hom.hom X.g) : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) ∘ y)
    (⇑z : (a : G) → (↑X.X₃ : Type u))
x : G × G → (↑X.X₁ : Type u)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u))) : Type u))
      y)
g : Fin 1 → G
⊢ Eq (α := (↑X.X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := HomologicalComplex.X (inhomogeneousCochains (G := G) X.2) 1) (Y :=
            (inhomogeneousCochains X.X₃).X 1) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) 1) :
          (a : (↑((inhomogeneousCochains X.2).X 1) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₁ X.X₂).inv :
              (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
                (↑((inhomogeneousCochains X.X₂).X 1) : Type u))
            y :
          (↑((inhomogeneousCochains X.X₂).X 1) : Type u))
        g :
      (↑X.X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₁ X.X₃).inv :
          (a : (↑(ModuleCat.of k (G → (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 1) : Type u))
        (⇑z : (a : G) → (↑X.X₃ : Type u)) g :
      (↑X.X₃ : Type u))

Tactic:
simp [cochainsIso₁, ← hy]

Premises used: groupCohomology.cochainsIso₁
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → (↑X.X₂ : Type u)
hy :
  Eq (α := G → (↑X.X₃ : Type u)) ((⇑(Rep.Hom.hom X.g) : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) ∘ y)
    (⇑z : (a : G) → (↑X.X₃ : Type u))
x : G × G → (↑X.X₁ : Type u)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u))) : Type u))
      y)
g : Fin (HAdd.hAdd (α := ℕ) 1 1) → G
h :
  Eq (α := (↑X.X₂ : Type u))
    (Function.comp (β := (↑X.X₁ : Type u)) (⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cochainsIso₂ X.X₁).inv :
            (a : (↑(ModuleCat.of k (G × G → (↑X.X₁ : Type u))) : Type u)) →
              (↑((inhomogeneousCochains X.X₁).X 2) : Type u))
          x)
        g :
      (↑X.X₂ : Type u))
    ((ModuleCat.Hom.hom (d₁₂ X.X₂ ≫ (cochainsIso₂ X.X₂).inv) :
          (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
            (↑((inhomogeneousCochains X.X₂).X (1 + 1)) : Type u))
        y g :
      (↑X.X₂ : Type u))
⊢ Eq (α := (↑X.X₂ : Type u))
    (Function.comp (β := (↑X.X₁ : Type u)) (⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cochainsIso₂ X.X₁).inv :
            (a : (↑(ModuleCat.of k (G × G → (↑X.X₁ : Type u))) : Type u)) →
              (↑((inhomogeneousCochains X.X₁).X 2) : Type u))
          x)
        g :
      (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousCochains X.X₂).X 1) (Y :=
            (inhomogeneousCochains X.X₂).X (HAdd.hAdd (α := ℕ) 1 1))
            ((inhomogeneousCochains X.X₂).d 1 (HAdd.hAdd (α := ℕ) 1 1)) :
          (a : (↑((inhomogeneousCochains X.X₂).X 1) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (1 + 1)) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₁ X.X₂).inv :
              (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
                (↑((inhomogeneousCochains X.X₂).X 1) : Type u))
            y :
          (↑((inhomogeneousCochains X.X₂).X 1) : Type u))
        g :
      (↑X.X₂ : Type u))

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]

Premises used: groupCohomology.eq_d₁₂_comp_inv, LinearMap.comp_apply, ModuleCat.hom_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → (↑X.X₂ : Type u)
hy :
  Eq (α := G → (↑X.X₃ : Type u)) ((⇑(Rep.Hom.hom X.g) : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) ∘ y)
    (⇑z : (a : G) → (↑X.X₃ : Type u))
x : G × G → (↑X.X₁ : Type u)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u))) : Type u))
      y)
g : Fin (HAdd.hAdd (α := ℕ) 1 1) → G
⊢ Eq (α := (↑X.X₂ : Type u))
    (Function.comp (β := (↑X.X₁ : Type u)) (⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cochainsIso₂ X.X₁).inv :
            (a : (↑(ModuleCat.of k (G × G → (↑X.X₁ : Type u))) : Type u)) →
              (↑((inhomogeneousCochains X.X₁).X 2) : Type u))
          x)
        g :
      (↑X.X₂ : Type u))
    ((ModuleCat.Hom.hom (d₁₂ X.X₂ ≫ (cochainsIso₂ X.X₂).inv) :
          (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
            (↑((inhomogeneousCochains X.X₂).X (1 + 1)) : Type u))
        y g :
      (↑X.X₂ : Type u))

Tactic:
simpa [← hx] using congr_fun (congr($((CommSq.vert_inv
        ⟨cochainsMap_f_2_comp_cochainsIso₂ (MonoidHom.id G) X.f⟩).w) x)) g

Premises used: groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, congrArg, CategoryTheory.ConcreteCategory.hom, CategoryTheory.CommSq.vert_inv, id, CategoryTheory.CommSq.mk, MonoidHom.id, CategoryTheory.ShortComplex.f, CategoryTheory.CommSq.w, congr_fun, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → (↑X.X₂ : Type u)
hy :
  Eq (α := G → (↑X.X₃ : Type u)) ((⇑(Rep.Hom.hom X.g) : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) ∘ y)
    (⇑z : (a : G) → (↑X.X₃ : Type u))
x : G × G → (↑X.X₁ : Type u)
hx :
  Eq (α := G × G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₁₂ X.X₂) :
        (a : (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u))) : Type u))
      y)
⊢ Eq (α := (↑(groupCohomology X.X₁ 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := groupCohomology X.X₃ 1) (δ hX 1 2 ⋯) :
          (a : (↑(groupCohomology X.X₃ 1) : Type u)) → (↑(groupCohomology X.X₁ 2) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (H1π X.X₃) :
              (a : (↑(ModuleCat.of k ↥(cocycles₁ X.X₃)) : Type u)) → (↑(H1 X.X₃) : Type u))
            z :
          (↑(H1 X.X₃) : Type u)) :
      (↑(groupCohomology X.X₁ 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H2π X.X₁) :
          (a : (↑(ModuleCat.of k ↥(cocycles₂ X.X₁)) : Type u)) → (↑(H2 X.X₁) : Type u))
        (Subtype.mk (p := fun (x : G × G → (↑X.X₁ : Type u)) ↦ x ∈ cocycles₂ X.X₁) x ⋯) :
      (↑(H2 X.X₁) : Type u))

Tactic:
simpa [H1π, H2π, ← cocyclesMk₂_eq X.X₁, ← cocyclesMk₁_eq X.X₃] using
    δ_apply hX rfl ((cochainsIso₁ X.X₃).inv z) (by
      rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]
      simp [cocycles₁.d₁₂_apply z]) ((cochainsIso₁ X.X₂).inv y) (by ext; simp [cochainsIso₁, ← hy])
    ((cochainsIso₂ X.X₁).inv x) <| by
      ext g
      rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]
      simpa [← hx] using congr_fun (congr($((CommSq.vert_inv
        ⟨cochainsMap_f_2_comp_cochainsIso₂ (MonoidHom.id G) X.f⟩).w) x)) g

Premises used: groupCohomology.δ_apply, CategoryTheory.ConcreteCategory.hom, CategoryTheory.ShortComplex.X₁, groupCohomology.cochainsIso₁, groupCohomology.cocyclesMk₁_eq, groupCohomology.H1π, groupCohomology.cocyclesMk₂_eq, DFunLike.coe, groupCohomology.H2π, CategoryTheory.ShortComplex.X₃, CategoryTheory.Iso.inv, rfl, CategoryTheory.ShortComplex.X₂, groupCohomology.cochainsIso₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : (↑A : Type (max u u_1))
g : G
simp :
  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 +
      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)))
            y :
          (↑A : Type (max u u_1)))
        y =
    HAdd.hAdd (α := G → (↑A : Type (max u u_1))) (β := G → (↑A : Type (max u u_1)))
      (fun (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)
      (fun (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)))
              y :
            (↑A : Type (max u u_1)))
          y)
      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 + y) :
        (↑A : Type (max u u_1)))
      (x + y) =
    HAdd.hAdd (α := G → (↑A : Type (max u u_1))) (β := G → (↑A : Type (max u u_1)))
      (fun (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)
      (fun (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)))
              y :
            (↑A : Type (max u u_1)))
          y)
      g

Tactic:
simp only [map_add, add_sub_add_comm]

Premises used: map_add, add_sub_add_comm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : (↑A : Type (max u u_1))
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 +
      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)))
            y :
          (↑A : Type (max u u_1)))
        y =
    HAdd.hAdd (α := G → (↑A : Type (max u u_1))) (β := G → (↑A : Type (max u u_1)))
      (fun (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)
      (fun (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)))
              y :
            (↑A : Type (max u u_1)))
          y)
      g

Tactic:
rfl