awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
hij : j + 1 = i
z : (Fin i → G) →₀ (↑X.X₃ : Type u)
hz :
  Eq (α := (↑((inhomogeneousChains X.X₃).X j) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((inhomogeneousChains X.X₃).d i j) :
          (a : (↑((inhomogeneousChains X.X₃).X i) : Type u)) → (↑((inhomogeneousChains X.X₃).X j) : Type u))
        z :
      (↑((inhomogeneousChains X.X₃).X j) : Type u))
    (0 : (↑((inhomogeneousChains 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 := (inhomogeneousChains X.X₂).X i) (Y :=
          HomologicalComplex.X (inhomogeneousChains (G := G) X.3) i)
          (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) X.g) i) :
        (a : (↑((inhomogeneousChains X.X₂).X i) : Type u)) → (↑((inhomogeneousChains X.3).X i) : Type u))
      y =
    z
x : (Fin j → G) →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := (Fin j → G) →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap :
          (a : (Fin j → G) →₀ (↑X.X₁ : Type u)) → (Fin j → G) →₀ (↑X.X₂ : Type u))
        x :
      (Fin j → G) →₀ (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((inhomogeneousChains X.X₂).d i j) :
          (a : (↑((inhomogeneousChains X.X₂).X i) : Type u)) → (↑((inhomogeneousChains X.X₂).X j) : Type u))
        y :
      (↑((inhomogeneousChains X.X₂).X j) : Type u))
⊢ Eq (α := (↑(groupHomology 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 : (↑(groupHomology X.X₃ i) : Type u)) → (↑(groupHomology 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 : (↑(cycles X.X₃ i) : Type u)) → (↑(groupHomology X.X₃ i) : Type u))
            (cyclesMk i j ⋯ z ⋯) :
          (↑(groupHomology X.X₃ i) : Type u)) :
      (↑(groupHomology 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 : (↑(cycles X.X₁ j) : Type u)) → (↑(groupHomology X.X₁ j) : Type u))
        (cyclesMkOfCompEqD hX hx) :
      (↑(groupHomology X.X₁ j) : Type u))

Tactic:
exact (map_chainsFunctor_shortExact hX).δ_apply i j hij z hz y hy x (by simpa using hx) _ rfl

Premises used: groupHomology.map_chainsFunctor_shortExact, CategoryTheory.ShortComplex.ShortExact.δ_apply, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G →₀ (↑X.X₂ : Type u)) → G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G →₀ (↑X.X₃ : Type u))
x : (↑X.X₁ : Type u)
hx :
  Eq (α := (↑X.X₂ : Type u)) ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) x : (↑X.X₂ : Type u))
    ((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 (↑X.X₂ : Type u)) : Type u))
        y :
      (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
rw :
  Eq (α := (↑((inhomogeneousChains X.X₃).X 0) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ X.X₃ ≫ (chainsIso₀ X.X₃).inv) :
          (a : (↑(ModuleCat.of k (G →₀ (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₃).X 0) : Type u))
        (↑z : G →₀ (↑X.X₃ : Type u)) :
      (↑((inhomogeneousChains X.X₃).X 0) : Type u))
    (0 : (↑((inhomogeneousChains X.X₃).X 0) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains X.X₃).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousChains X.X₃).X 1) (Y := (inhomogeneousChains X.X₃).X 0)
            ((inhomogeneousChains X.X₃).d 1 0) :
          (a : (↑((inhomogeneousChains X.X₃).X 1) : Type u)) → (↑((inhomogeneousChains X.X₃).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (chainsIso₁ X.X₃).inv :
            (a : (↑(ModuleCat.of k (G →₀ (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₃).X 1) : Type u))
          (↑z : G →₀ (↑X.X₃ : Type u))) :
      (↑((inhomogeneousChains X.X₃).X 0) : Type u))
    (0 : (↑((inhomogeneousChains X.X₃).X 0) : Type u))

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

Premises used: LinearMap.comp_apply, groupHomology.eq_d₁₀_comp_inv, ModuleCat.hom_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G →₀ (↑X.X₂ : Type u)) → G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G →₀ (↑X.X₃ : Type u))
x : (↑X.X₁ : Type u)
hx :
  Eq (α := (↑X.X₂ : Type u)) ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) x : (↑X.X₂ : Type u))
    ((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 (↑X.X₂ : Type u)) : Type u))
        y :
      (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains X.X₃).X 0) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ X.X₃ ≫ (chainsIso₀ X.X₃).inv) :
          (a : (↑(ModuleCat.of k (G →₀ (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₃).X 0) : Type u))
        (↑z : G →₀ (↑X.X₃ : Type u)) :
      (↑((inhomogeneousChains X.X₃).X 0) : Type u))
    (0 : (↑((inhomogeneousChains X.X₃).X 0) : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G →₀ (↑X.X₂ : Type u)) → G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G →₀ (↑X.X₃ : Type u))
x : (↑X.X₁ : Type u)
hx :
  Eq (α := (↑X.X₂ : Type u)) ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) x : (↑X.X₂ : Type u))
    ((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 (↑X.X₂ : Type u)) : Type u))
        y :
      (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
x_1 : Fin 1 → G
⊢ Eq (α := (↑X.3 : Type u))
    ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X := (inhomogeneousChains X.X₂).X 1) (Y :=
                  HomologicalComplex.X (inhomogeneousChains (G := G) X.3) 1)
                  (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) X.g) 1) :
                (a : (↑((inhomogeneousChains X.X₂).X 1) : Type u)) → (↑((inhomogeneousChains X.3).X 1) : Type u))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (chainsIso₁ X.X₂).inv :
                  (a : (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u)) →
                    (↑((inhomogeneousChains X.X₂).X 1) : Type u))
                y) :
            (↑(HomologicalComplex.X (inhomogeneousChains (G := G) X.3) 1) : Type u)) :
          (a : Fin 1 → G) → (↑X.3 : Type u))
        x_1 :
      (↑X.3 : Type u))
    ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (chainsIso₁ X.X₃).inv :
                (a : (↑(ModuleCat.of k (G →₀ (↑X.X₃ : Type u))) : Type u)) →
                  (↑((inhomogeneousChains X.X₃).X 1) : Type u))
              (↑z : G →₀ (↑X.X₃ : Type u)) :
            (↑((inhomogeneousChains X.X₃).X 1) : Type u)) :
          (a : Fin 1 → G) → (↑X.3 : Type u))
        x_1 :
      (↑X.3 : Type u))

Tactic:
simp [chainsIso₁, ← hy]

Premises used: groupHomology.chainsIso₁
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G →₀ (↑X.X₂ : Type u)) → G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G →₀ (↑X.X₃ : Type u))
x : (↑X.X₁ : Type u)
hx :
  Eq (α := (↑X.X₂ : Type u)) ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) x : (↑X.X₂ : Type u))
    ((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 (↑X.X₂ : Type u)) : Type u))
        y :
      (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
x_1 : Fin 0 → G
rw :
  ((((ModuleCat.Hom.hom (d₁₀ X.X₂ ≫ (chainsIso₀ X.X₂).inv) :
              (a : (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₂).X 0) : Type u))
            y :
          (↑((inhomogeneousChains X.X₂).X 0) : Type u)) :
        (a : Fin 0 → G) → (↑X.X₂ : Type u))
      x_1 :
    (↑X.X₂ : Type u))
| ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := (inhomogeneousChains X.X₂).X 1) (Y := (inhomogeneousChains X.X₂).X 0)
                ((inhomogeneousChains X.X₂).d 1 0) :
              (a : (↑((inhomogeneousChains X.X₂).X 1) : Type u)) → (↑((inhomogeneousChains X.X₂).X 0) : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (chainsIso₁ X.X₂).inv :
                (a : (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u)) →
                  (↑((inhomogeneousChains X.X₂).X 1) : Type u))
              y) :
          (↑((inhomogeneousChains X.X₂).X 0) : Type u)) :
        (a : Fin 0 → G) → (↑X.X₂ : Type u))
      x_1 :
    (↑X.X₂ : Type u))

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

Premises used: LinearMap.comp_apply, groupHomology.eq_d₁₀_comp_inv, ModuleCat.hom_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G →₀ (↑X.X₂ : Type u)) → G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G →₀ (↑X.X₃ : Type u))
x : (↑X.X₁ : Type u)
hx :
  Eq (α := (↑X.X₂ : Type u)) ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) x : (↑X.X₂ : Type u))
    ((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 (↑X.X₂ : Type u)) : Type u))
        y :
      (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
x_1 : Fin 0 → G
⊢ Eq (α := (↑X.X₂ : Type u))
    ((((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap :
                (a : (Fin 0 → G) →₀ (↑X.X₁ : Type u)) → (Fin 0 → G) →₀ (↑X.X₂ : Type u))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (chainsIso₀ X.X₁).inv :
                  (a : (↑(ModuleCat.of k (↑X.X₁ : Type u)) : Type u)) → (↑((inhomogeneousChains X.X₁).X 0) : Type u))
                x) :
            (Fin 0 → G) →₀ (↑X.X₂ : Type u)) :
          (a : Fin 0 → G) → (↑X.X₂ : Type u))
        x_1 :
      (↑X.X₂ : Type u))
    ((((ModuleCat.Hom.hom (d₁₀ X.X₂ ≫ (chainsIso₀ X.X₂).inv) :
                (a : (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u)) →
                  (↑((inhomogeneousChains X.X₂).X 0) : Type u))
              y :
            (↑((inhomogeneousChains X.X₂).X 0) : Type u)) :
          (a : Fin 0 → G) → (↑X.X₂ : Type u))
        x_1 :
      (↑X.X₂ : Type u))

Tactic:
simp [chainsIso₀, ← hx]

Premises used: groupHomology.chainsIso₀
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G →₀ (↑X.X₂ : Type u)) → G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G →₀ (↑X.X₃ : Type u))
x : (↑X.X₁ : Type u)
hx :
  Eq (α := (↑X.X₂ : Type u)) ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) x : (↑X.X₂ : Type u))
    ((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 (↑X.X₂ : Type u)) : Type u))
        y :
      (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
⊢ Eq (α := (↑(groupHomology X.X₁ 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := groupHomology X.X₃ 1) (δ hX 1 0 ⋯) :
          (a : (↑(groupHomology X.X₃ 1) : Type u)) → (↑(groupHomology X.X₁ 0) : 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 ↥(cycles₁ X.X₃)) : Type u)) → (↑(H1 X.X₃) : Type u))
            z :
          (↑(H1 X.X₃) : Type u)) :
      (↑(groupHomology X.X₁ 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H0π X.X₁) :
          (a : (↑(ModuleCat.of k (↑X.X₁ : Type u)) : Type u)) → (↑(H0 X.X₁) : Type u))
        x :
      (↑(H0 X.X₁) : Type u))

Tactic:
simpa only [H1π, ModuleCat.hom_comp, LinearMap.coe_comp, Function.comp_apply, H0π,
    ← cyclesMk₀_eq X.X₁, ← cyclesMk₁_eq X.X₃]
  using δ_apply hX (i := 1) (j := 0) rfl ((chainsIso₁ X.X₃).inv z.1) (by
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]; simp)
    ((chainsIso₁ X.X₂).inv y) (Finsupp.ext fun _ => by simp [chainsIso₁, ← hy])
    ((chainsIso₀ X.X₁).inv x) (Finsupp.ext fun _ => by
      conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]
      simp [chainsIso₀, ← hx])

Premises used: Finsupp.ext, CategoryTheory.ConcreteCategory.hom, CategoryTheory.ShortComplex.X₁, groupHomology.H1π, groupHomology.chainsIso₁, groupHomology.δ_apply, LinearMap.coe_comp, groupHomology.H0π, groupHomology.cyclesMk₁_eq, Function.comp_apply, groupHomology.chainsIso₀, groupHomology.cyclesMk₀_eq, Subtype.val, ModuleCat.hom_comp, DFunLike.coe, CategoryTheory.ShortComplex.X₃, CategoryTheory.Iso.inv, rfl, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : G × G →₀ (↑X.X₂ : Type u)
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : 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) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
⊢ Eq (α := (↑(X₃ (shortComplexH1 (G := G) X.2)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (Y := X₃ (shortComplexH1 (G := G) X.2))
            ((shortComplexH1 X.X₁).g ≫ Hom.τ₃ (mapShortComplexH1 (MonoidHom.id G) X.f)) :
          (a : (↑(shortComplexH1 X.X₁).X₂ : Type u)) → (↑(shortComplexH1 X.2).X₃ : Type u))
        x :
      (↑(X₃ (shortComplexH1 (G := G) X.2)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (shortComplexH1 X.X₁).X₂) (Y := X₃ (shortComplexH1 (G := G) X.2))
            (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) X.f) ≫ g (shortComplexH1 (G := G) X.2)) :
          (a : (↑(shortComplexH1 X.X₁).X₂ : Type u)) → (↑(shortComplexH1 X.2).X₃ : Type u))
        x :
      (↑(X₃ (shortComplexH1 (G := G) X.2)) : Type u))

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

Tactic:
simp_all [shortComplexH1]

Premises used: groupHomology.shortComplexH1
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G × G →₀ (↑X.X₂ : Type u)) → G × G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G × G →₀ (↑X.X₃ : Type u))
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : 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) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
rw :
  Eq (α := (↑((inhomogeneousChains X.X₃).X 1) : Type u))
    ((ModuleCat.Hom.hom (d₂₁ X.X₃ ≫ (chainsIso₁ X.X₃).inv) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₃).X 1) : Type u))
        (↑z : G × G →₀ (↑X.X₃ : Type u)) :
      (↑((inhomogeneousChains X.X₃).X 1) : Type u))
    (0 : (↑((inhomogeneousChains X.X₃).X 1) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains X.X₃).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousChains X.X₃).X 2) (Y := (inhomogeneousChains X.X₃).X 1)
            ((inhomogeneousChains X.X₃).d 2 1) :
          (a : (↑((inhomogeneousChains X.X₃).X 2) : Type u)) → (↑((inhomogeneousChains X.X₃).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (chainsIso₂ X.X₃).inv :
            (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₃ : Type u))) : Type u)) →
              (↑((inhomogeneousChains X.X₃).X 2) : Type u))
          (↑z : G × G →₀ (↑X.X₃ : Type u))) :
      (↑((inhomogeneousChains X.X₃).X 1) : Type u))
    (0 : (↑((inhomogeneousChains X.X₃).X 1) : Type u))

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

Premises used: groupHomology.eq_d₂₁_comp_inv, LinearMap.comp_apply, ModuleCat.hom_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G × G →₀ (↑X.X₂ : Type u)) → G × G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G × G →₀ (↑X.X₃ : Type u))
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : 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) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains X.X₃).X 1) : Type u))
    ((ModuleCat.Hom.hom (d₂₁ X.X₃ ≫ (chainsIso₁ X.X₃).inv) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₃).X 1) : Type u))
        (↑z : G × G →₀ (↑X.X₃ : Type u)) :
      (↑((inhomogeneousChains X.X₃).X 1) : Type u))
    (0 : (↑((inhomogeneousChains X.X₃).X 1) : Type u))

Tactic:
simp