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 k G)
hX : X.ShortExact
i j : ℕ
hij : i + 1 = j
z : (Fin i → G) → (↑X.X₃ : Type u)
hz :
  Eq (α := (↑((inhomogeneousCochains X.X₃).X j) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((inhomogeneousCochains X.X₃).d i j) :
          (a : (↑((inhomogeneousCochains X.X₃).X i) : Type u)) → (↑((inhomogeneousCochains X.X₃).X j) : Type u))
        z :
      (↑((inhomogeneousCochains X.X₃).X j) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X j) : Type u))
y : (Fin i → G) → (↑X.X₂ : Type u)
hy :
  (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) i) (Y :=
          (inhomogeneousCochains X.X₃).X i) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) i) :
        (a : (↑((inhomogeneousCochains X.2).X i) : Type u)) → (↑((inhomogeneousCochains X.X₃).X i) : Type u))
      y =
    z
x : (Fin j → G) → (↑X.X₁ : Type u)
hx :
  Eq (α := (Fin j → 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) ((inhomogeneousCochains X.X₂).d i j) :
        (a : (↑((inhomogeneousCochains X.X₂).X i) : Type u)) → (↑((inhomogeneousCochains X.X₂).X j) : Type u))
      y)
⊢ Eq (α := (↑(groupCohomology X.X₁ j) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (δ hX i j hij) :
          (a : (↑(groupCohomology X.X₃ i) : Type u)) → (↑(groupCohomology X.X₁ j) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (π X.X₃ i) :
              (a : (↑(cocycles X.X₃ i) : Type u)) → (↑(groupCohomology X.X₃ i) : Type u))
            (cocyclesMk z ⋯) :
          (↑(groupCohomology X.X₃ i) : Type u)) :
      (↑(groupCohomology X.X₁ j) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (π X.X₁ j) :
          (a : (↑(cocycles X.X₁ j) : Type u)) → (↑(groupCohomology X.X₁ j) : Type u))
        (cocyclesMkOfCompEqD hX hx) :
      (↑(groupCohomology X.X₁ j) : Type u))

Tactic:
exact (map_cochainsFunctor_shortExact hX).δ_apply i j hij z hz y hy x
    (by simpa using hx) (j + 1) (by simp)

Premises used: HAdd.hAdd, CategoryTheory.ShortComplex.ShortExact.δ_apply, groupCohomology.map_cochainsFunctor_shortExact, OfNat.ofNat
-- 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
y : (↑X.X₂ : Type (max u u_1))
x : G → (↑X.X₁ : Type (max u u_1))
hx :
  Eq (α := G → (↑X.X₂ : Type (max u u_1)))
    ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u 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₀₁.{u, u_1} X.X₂) :
        (a : (↑(ModuleCat.of k (↑X.X₂ : Type (max u u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G → (↑X.X₂ : Type (max u u_1)))) : Type (max u u_1)))
      y)
a :
  Eq (α := G × G → (↑X.X₂ : Type (max u u_1)))
    ((fun (x : G × G → (↑X.X₁ : Type (max u u_1))) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x :
          G × G → (↑X.X₂ : Type (max u u_1))))
      ((ModuleCat.Hom.hom (d₁₂ X.X₁) :
          (a : G → (↑X.X₁ : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G → (↑X.X₁ : Type (max u u_1)))) : Type (max u u_1)))
        x))
    ((fun (x : G × G → (↑X.X₁ : Type (max u u_1))) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x :
          G × G → (↑X.X₂ : Type (max u u_1))))
      0)
⊢ x ∈ cocycles₁ X.X₁

Tactic:
apply Function.Injective.comp_left ((Rep.mono_iff_injective X.f).1 hX.2)

Premises used: CategoryTheory.ShortComplex.ShortExact.mono_f, Iff.mp, Function.Injective.comp_left, CategoryTheory.ShortComplex.f, Rep.mono_iff_injective
-- 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
y : (↑X.X₂ : Type (max u u_1))
x : G → (↑X.X₁ : Type (max u u_1))
hx :
  Eq (α := G → (↑X.X₂ : Type (max u u_1)))
    ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u 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₀₁.{u, u_1} X.X₂) :
        (a : (↑(ModuleCat.of k (↑X.X₂ : Type (max u u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G → (↑X.X₂ : Type (max u u_1)))) : Type (max u u_1)))
      y)
⊢ Eq (α := (↑(shortComplexH1.{u, u_1} 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₂ (shortComplexH1.{u, u_1} (G := G) X.1)) (Y :=
            (shortComplexH1.{u, u_1} X.X₂).X₃)
            (g (shortComplexH1.{u, u_1} (G := G) X.1) ≫ Hom.τ₃ (mapShortComplexH1 (MonoidHom.id G) X.f)) :
          (a : (↑(shortComplexH1 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH1 X.X₂).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} 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₂ (shortComplexH1.{u, u_1} (G := G) X.1))
            (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) X.f) ≫ (shortComplexH1.{u, u_1} X.X₂).g) :
          (a : (↑(shortComplexH1 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH1 X.X₂).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} X.X₂).X₃ : Type (max u u_1)))

Tactic:
have := congr($((mapShortComplexH1 (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 k G)
hX : X.ShortExact
y : (↑X.X₂ : Type (max u u_1))
x : G → (↑X.X₁ : Type (max u u_1))
hx :
  Eq (α := G → (↑X.X₂ : Type (max u u_1)))
    ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u 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₀₁.{u, u_1} X.X₂) :
        (a : (↑(ModuleCat.of k (↑X.X₂ : Type (max u u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G → (↑X.X₂ : Type (max u u_1)))) : Type (max u u_1)))
      y)
this :
  Eq (α := (↑(shortComplexH1.{u, u_1} 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₂ (shortComplexH1.{u, u_1} (G := G) X.1)) (Y :=
            (shortComplexH1.{u, u_1} X.X₂).X₃)
            (g (shortComplexH1.{u, u_1} (G := G) X.1) ≫ Hom.τ₃ (mapShortComplexH1 (MonoidHom.id G) X.f)) :
          (a : (↑(shortComplexH1 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH1 X.X₂).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} 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₂ (shortComplexH1.{u, u_1} (G := G) X.1))
            (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) X.f) ≫ (shortComplexH1.{u, u_1} X.X₂).g) :
          (a : (↑(shortComplexH1 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH1 X.X₂).X₃ : Type (max u u_1)))
        x :
      (↑(shortComplexH1.{u, u_1} X.X₂).X₃ : Type (max u u_1)))
⊢ Eq (α := G × G → (↑X.X₂ : Type (max u u_1)))
    ((fun (x : G × G → (↑X.X₁ : Type (max u u_1))) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x :
          G × G → (↑X.X₂ : Type (max u u_1))))
      ((ModuleCat.Hom.hom (d₁₂ X.X₁) :
          (a : G → (↑X.X₁ : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G → (↑X.X₁ : Type (max u u_1)))) : Type (max u u_1)))
        x))
    ((fun (x : G × G → (↑X.X₁ : Type (max u u_1))) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x :
          G × G → (↑X.X₂ : Type (max u u_1))))
      0)

Tactic:
simp_all [shortComplexH1, LinearMap.compLeft]

Premises used: groupCohomology.shortComplexH1, 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 : ↥X.X₃.ρ.invariants
y : (↑X.X₂ : Type u)
hy : (Rep.Hom.hom X.g : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) y = (↑z : (↑X.X₃ : Type u))
x : G → (↑X.X₁ : Type u)
hx :
  Eq (α := 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 (↑X.X₂ : Type u)) : Type u)) → (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u))
      y)
rw :
  Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
    ((ModuleCat.Hom.hom (d₀₁ X.X₃ ≫ (cochainsIso₁ X.X₃).inv) :
          (a : (↑(ModuleCat.of k (↑X.X₃ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₃).X (0 + 1)) : Type u))
        (↑z : (↑X.X₃ : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
⊢ Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 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 0) (Y :=
            (inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1))
            ((inhomogeneousCochains X.X₃).d 0 (HAdd.hAdd (α := ℕ) 0 1)) :
          (a : (↑((inhomogeneousCochains X.X₃).X 0) : Type u)) → (↑((inhomogeneousCochains X.X₃).X (0 + 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 (↑X.X₃ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
            (↑z : (↑X.X₃ : Type u)) :
          (↑((inhomogeneousCochains X.X₃).X 0) : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 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 : ↥X.X₃.ρ.invariants
y : (↑X.X₂ : Type u)
hy : (Rep.Hom.hom X.g : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) y = (↑z : (↑X.X₃ : Type u))
x : G → (↑X.X₁ : Type u)
hx :
  Eq (α := 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 (↑X.X₂ : Type u)) : Type u)) → (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u))
      y)
⊢ Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
    ((ModuleCat.Hom.hom (d₀₁ X.X₃ ≫ (cochainsIso₁ X.X₃).inv) :
          (a : (↑(ModuleCat.of k (↑X.X₃ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₃).X (0 + 1)) : Type u))
        (↑z : (↑X.X₃ : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))

Tactic:
simp
-- 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 : ↥X.X₃.ρ.invariants
y : (↑X.X₂ : Type u)
hy : (Rep.Hom.hom X.g : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) y = (↑z : (↑X.X₃ : Type u))
x : G → (↑X.X₁ : Type u)
hx :
  Eq (α := 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 (↑X.X₂ : Type u)) : Type u)) → (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u))
      y)
g : Fin 0 → 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) 0) (Y :=
            (inhomogeneousCochains X.X₃).X 0) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) 0) :
          (a : (↑((inhomogeneousCochains X.2).X 0) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 0) : 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 (↑X.X₂ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₂).X 0) : Type u))
            y :
          (↑((inhomogeneousCochains X.X₂).X 0) : 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 (↑X.X₃ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
        (↑z : (↑X.X₃ : Type u)) g :
      (↑X.X₃ : Type u))

Tactic:
simp [← hy, cochainsIso₀]

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 : ↥X.X₃.ρ.invariants
y : (↑X.X₂ : Type u)
hy : (Rep.Hom.hom X.g : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) y = (↑z : (↑X.X₃ : Type u))
x : G → (↑X.X₁ : Type u)
hx :
  Eq (α := 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 (↑X.X₂ : Type u)) : Type u)) → (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u))
      y)
g : Fin (HAdd.hAdd (α := ℕ) 0 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 → (↑X.X₁ : Type u))) : Type u)) → (↑((inhomogeneousCochains X.X₁).X 1) : Type u))
          x)
        g :
      (↑X.X₂ : Type u))
    ((ModuleCat.Hom.hom (d₀₁ X.X₂ ≫ (cochainsIso₁ X.X₂).inv) :
          (a : (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (0 + 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 → (↑X.X₁ : Type u))) : Type u)) → (↑((inhomogeneousCochains X.X₁).X 1) : 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 0) (Y :=
            (inhomogeneousCochains X.X₂).X (HAdd.hAdd (α := ℕ) 0 1))
            ((inhomogeneousCochains X.X₂).d 0 (HAdd.hAdd (α := ℕ) 0 1)) :
          (a : (↑((inhomogeneousCochains X.X₂).X 0) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (0 + 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 (↑X.X₂ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₂).X 0) : Type u))
            y :
          (↑((inhomogeneousCochains X.X₂).X 0) : 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 : ↥X.X₃.ρ.invariants
y : (↑X.X₂ : Type u)
hy : (Rep.Hom.hom X.g : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) y = (↑z : (↑X.X₃ : Type u))
x : G → (↑X.X₁ : Type u)
hx :
  Eq (α := 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 (↑X.X₂ : Type u)) : Type u)) → (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u))
      y)
g : Fin (HAdd.hAdd (α := ℕ) 0 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 → (↑X.X₁ : Type u))) : Type u)) → (↑((inhomogeneousCochains X.X₁).X 1) : Type u))
          x)
        g :
      (↑X.X₂ : Type u))
    ((ModuleCat.Hom.hom (d₀₁ X.X₂ ≫ (cochainsIso₁ X.X₂).inv) :
          (a : (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (0 + 1)) : Type u))
        y g :
      (↑X.X₂ : Type u))

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

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, CategoryTheory.CommSq.vert_inv, id, CategoryTheory.CommSq.mk, MonoidHom.id, CategoryTheory.ShortComplex.f, CategoryTheory.CommSq.w, congr_fun, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, 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 : ↥X.X₃.ρ.invariants
y : (↑X.X₂ : Type u)
hy : (Rep.Hom.hom X.g : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) y = (↑z : (↑X.X₃ : Type u))
x : G → (↑X.X₁ : Type u)
hx :
  Eq (α := 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 (↑X.X₂ : Type u)) : Type u)) → (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u))
      y)
⊢ Eq (α := (↑(groupCohomology X.X₁ 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := groupCohomology X.X₃ 0) (δ hX 0 1 ⋯) :
          (a : (↑(groupCohomology X.X₃ 0) : Type u)) → (↑(groupCohomology X.X₁ 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (H0Iso X.X₃).inv :
              (a : (↑(ModuleCat.of k ↥X.X₃.ρ.invariants) : Type u)) → (↑(H0 X.X₃) : Type u))
            z :
          (↑(H0 X.X₃) : Type u)) :
      (↑(groupCohomology X.X₁ 1) : 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))
        (Subtype.mk (p := fun (x : G → (↑X.X₁ : Type u)) ↦ x ∈ cocycles₁ X.X₁) x ⋯) :
      (↑(H1 X.X₁) : Type u))

Tactic:
simpa [H0Iso, H1π, ← cocyclesMk₁_eq X.X₁, ← cocyclesMk₀_eq z] using
    δ_apply hX rfl ((cochainsIso₀ X.X₃).inv z.1) (by
      rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₀₁_comp_inv]; simp)
      ((cochainsIso₀ X.X₂).inv y)
    (by ext; simp [← hy, cochainsIso₀]) ((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_1_comp_cochainsIso₁ (MonoidHom.id G) X.f⟩).w) x)) g

Premises used: groupCohomology.δ_apply, CategoryTheory.ConcreteCategory.hom, groupCohomology.cochainsIso₀, CategoryTheory.ShortComplex.X₁, groupCohomology.cochainsIso₁, groupCohomology.cocyclesMk₁_eq, groupCohomology.H1π, groupCohomology.H0Iso, groupCohomology.cocyclesMk₀_eq, Subtype.val, DFunLike.coe, CategoryTheory.ShortComplex.X₃, CategoryTheory.Iso.inv, rfl, CategoryTheory.ShortComplex.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)
a :
  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)
⊢ x ∈ cocycles₂ X.X₁

Tactic:
apply Function.Injective.comp_left ((Rep.mono_iff_injective X.f).1 hX.2)

Premises used: CategoryTheory.ShortComplex.ShortExact.mono_f, Iff.mp, Function.Injective.comp_left, CategoryTheory.ShortComplex.f, Rep.mono_iff_injective