awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
x : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)
h : x ∈ cycles₂ A
⊢ Eq (α := (↑(shortComplexH2 B).X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((mapShortComplexH2 f φ).τ₂ ≫ (shortComplexH2 B).g) :
          (a : (↑(shortComplexH2 A).X₂ : Type u)) → (↑(shortComplexH2 B).X₃ : Type u))
        x :
      (↑(shortComplexH2 B).X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH2 A).g ≫ (mapShortComplexH2 f φ).τ₃) :
          (a : (↑(shortComplexH2 A).X₂ : Type u)) → (↑(shortComplexH2 B).X₃ : Type u))
        x :
      (↑(shortComplexH2 B).X₃ : Type u))

Tactic:
have := congr($((mapShortComplexH2 f φ).comm₂₃) x)
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
x : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)
h : x ∈ cycles₂ A
this :
  Eq (α := (↑(shortComplexH2 B).X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((mapShortComplexH2 f φ).τ₂ ≫ (shortComplexH2 B).g) :
          (a : (↑(shortComplexH2 A).X₂ : Type u)) → (↑(shortComplexH2 B).X₃ : Type u))
        x :
      (↑(shortComplexH2 B).X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((shortComplexH2 A).g ≫ (mapShortComplexH2 f φ).τ₃) :
          (a : (↑(shortComplexH2 A).X₂ : Type u)) → (↑(shortComplexH2 B).X₃ : Type u))
        x :
      (↑(shortComplexH2 B).X₃ : Type u))
⊢ Membership.mem (α := (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u)) (cycles₂ B)
    ((ModuleCat.Hom.hom (chainsMap₂ f φ) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))

Tactic:
simp_all [cycles₂, shortComplexH2]

Premises used: groupHomology.cycles₂, groupHomology.shortComplexH2
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
⊢ ModuleCat.Hom.hom (mapCycles₂ f φ) = (ModuleCat.Hom.hom (chainsMap₂ f φ)).restrict ⋯

Tactic:
rfl

Premises used: Set.Mem, LinearMap.restrict, groupHomology.cycles₂, LinearMap.codRestrict, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
rw :
  mapCycles₂ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    cyclesMap' (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ) (shortComplexH2 A).moduleCatLeftHomologyData
      (shortComplexH2 C).moduleCatLeftHomologyData
rw₁ rw₂ :
  mapCycles₂ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    cyclesMap' (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ))
      (shortComplexH2 A).moduleCatLeftHomologyData (shortComplexH2 C).moduleCatLeftHomologyData
⊢ mapCycles₂ (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) = mapCycles₂ f φ ≫ mapCycles₂ g ψ

Tactic:
rw [← cyclesMap'_comp, ← mapShortComplexH2_comp]

Premises used: CategoryTheory.ShortComplex.cyclesMap'_comp, groupHomology.mapShortComplexH2_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
⊢ mapCycles₂ (MonoidHom.id G) (φ ≫ ψ) =
    CategoryStruct.comp (Y := ModuleCat.of k ↥(cycles₂ B)) (mapCycles₂ (MonoidHom.id G) φ)
      (mapCycles₂ (MonoidHom.id G) ψ)

Tactic:
mapCycles₂_comp (MonoidHom.id G) (MonoidHom.id G) _ _

Premises used: groupHomology.mapCycles₂_comp, SemilinearMapClass.semilinearMap, MonoidHom.id
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
⊢ mapCycles₂ f φ ≫ (shortComplexH2 B).moduleCatLeftHomologyData.i =
    (shortComplexH2 A).moduleCatLeftHomologyData.i ≫ chainsMap₂ f φ

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
x : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)
⊢ Eq (α := H × H →₀ (↑B : Type u))
    ((↑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (mapCycles₂ f φ) :
              (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(ModuleCat.of k ↥(cycles₂ B)) : Type u))
            x) :
        H × H →₀ (↑B : Type u)) :
      H × H →₀ (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsMap₂ f φ) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
        (↑x : G × G →₀ (↑A : Type u)) :
      (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))

Tactic:
rfl

Premises used: Finsupp.onFinset, Finsupp.mapRange, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
⊢ cyclesMap f φ 2 ≫ (isoCycles₂ B).hom = (isoCycles₂ A).hom ≫ mapCycles₂ f φ

Tactic:
simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH2 B)).i, mapShortComplexH2,
    chainsMap_f_2_comp_chainsIso₂ f]

Premises used: groupHomology.mapShortComplexH2, CategoryTheory.cancel_mono, groupHomology.chainsMap_f_2_comp_chainsIso₂, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, groupHomology.shortComplexH2, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
⊢ H2π A ≫ map f φ 2 = mapCycles₂ f φ ≫ H2π B

Tactic:
simp [H2π, Iso.inv_comp_eq, ← cyclesMap_comp_isoCycles₂_hom_assoc]

Premises used: groupHomology.H2π, CategoryTheory.Iso.inv_comp_eq, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k G
B : Rep k H
f : G →* H
φ : Quiver.Hom.{?u.1130867, max u (?u.1130867 + 1)} A_1 (res f B)
n_1 n : ℕ
A : Rep k G
⊢ map (MonoidHom.id G) (𝟙 A) n = 𝟙 (groupHomology A n)

Tactic:
simp [map, groupHomology]

Premises used: groupHomology, groupHomology.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f_1 : G →* H
φ : Quiver.Hom.{?u.1130867, max u (?u.1130867 + 1)} A (res f_1 B)
n_1 n : ℕ
X Y Z : Rep k G
f : X ⟶ Y
g : Y ⟶ Z
simp :
  Eq (α := groupHomology X n ⟶ groupHomology Z n) (map (MonoidHom.id G) (f ≫ g) n)
    (HomologicalComplex.homologyMap
      (chainsMap (MonoidHom.comp (MonoidHom.id G) (MonoidHom.id G))
        (f ≫
          ofHom
            {
              toLinearMap :=
                (↑(Hom.hom g) :
                  [inst_3 :
                      FunLike (Y.ρ.IntertwiningMap (MonoidHom.comp Z.ρ (MonoidHom.id G))) (↑Y : Type u) (↑Z : Type u)] →
                    [SemilinearMapClass (Y.ρ.IntertwiningMap (MonoidHom.comp Z.ρ (MonoidHom.id G))) (RingHom.id k)
                          (↑Y : Type u) (↑Z : Type u)] →
                      (↑Y : Type u) →ₗ[k] (↑Z : Type u)),
              isIntertwining' := ⋯ }))
      n)
⊢ Eq (α := groupHomology X n ⟶ groupHomology Z n) (map (MonoidHom.id G) (f ≫ g) n)
    (CategoryStruct.comp (Y := groupHomology Y n) (map (MonoidHom.id G) f n) (map (MonoidHom.id G) g n))

Tactic:
simp only [← HomologicalComplex.homologyMap_comp, ← chainsMap_comp]

Premises used: HomologicalComplex.homologyMap_comp, groupHomology.chainsMap_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f_1 : G →* H
φ : Quiver.Hom.{?u.1130867, max u (?u.1130867 + 1)} A (res f_1 B)
n_1 n : ℕ
X Y Z : Rep k G
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := groupHomology X n ⟶ groupHomology Z n) (map (MonoidHom.id G) (f ≫ g) n)
    (HomologicalComplex.homologyMap
      (chainsMap (MonoidHom.comp (MonoidHom.id G) (MonoidHom.id G))
        (f ≫
          ofHom
            {
              toLinearMap :=
                (↑(Hom.hom g) :
                  [inst_3 :
                      FunLike (Y.ρ.IntertwiningMap (MonoidHom.comp Z.ρ (MonoidHom.id G))) (↑Y : Type u) (↑Z : Type u)] →
                    [SemilinearMapClass (Y.ρ.IntertwiningMap (MonoidHom.comp Z.ρ (MonoidHom.id G))) (RingHom.id k)
                          (↑Y : Type u) (↑Z : Type u)] →
                      (↑Y : Type u) →ₗ[k] (↑Z : Type u)),
              isIntertwining' := ⋯ }))
      n)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : Quiver.Hom.{?u.1133369, max u (?u.1133369 + 1)} A (res f B)
n_1 n : ℕ
x x_1 : Rep k G
⊢ Eq (α := Functor.obj (functor k G n) x ⟶ Functor.obj (functor k G n) x_1)
    (CategoryTheory.Functor.map (functor k G n) 0) 0

Tactic:
simp [map]

Premises used: groupHomology.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ_1 : Quiver.Hom.{?u.1135932, max u (?u.1135932 + 1)} A (res f B)
n_1 n : ℕ
X Y : Rep k H
φ : X ⟶ Y
⊢ Eq (α := cycles (of (MonoidHom.comp X.ρ f)) n ⟶ groupHomology Y n)
    (HomologicalComplex.cyclesMap
        (chainsMap (f.comp (MonoidHom.id G))
          (CategoryStruct.comp (Y := res (MonoidHom.id G) (of (MonoidHom.comp Y.ρ f)))
            (ofHom
              {
                toLinearMap :=
                  (↑(Hom.hom φ) :
                    [inst_3 : FunLike (X.ρ.IntertwiningMap Y.ρ) (↑X : Type u) (↑Y : Type u)] →
                      [SemilinearMapClass (X.ρ.IntertwiningMap Y.ρ) (RingHom.id k) (↑X : Type u) (↑Y : Type u)] →
                        (↑X : Type u) →ₗ[k] (↑Y : Type u)),
                isIntertwining' := ⋯ })
            (ofHom
              {
                toLinearMap :=
                  (↑(IntertwiningMap.id (MonoidHom.comp Y.ρ f)) :
                    [inst_3 :
                        FunLike (IntertwiningMap (MonoidHom.comp Y.ρ f) (MonoidHom.comp Y.ρ f)) (↑Y : Type u)
                          (↑Y : Type u)] →
                      [SemilinearMapClass (IntertwiningMap (MonoidHom.comp Y.ρ f) (MonoidHom.comp Y.ρ f)) (RingHom.id k)
                            (↑Y : Type u) (↑Y : Type u)] →
                        (↑Y : Type u) →ₗ[k] (↑Y : Type u)),
                isIntertwining' := ⋯ })))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousChains Y) n)
    (HomologicalComplex.cyclesMap
        (chainsMap (MonoidHom.comp (MonoidHom.id H) f)
          (ofHom
            {
              toLinearMap :=
                (↑(Hom.hom φ) :
                  [inst_3 :
                      FunLike (X.ρ.IntertwiningMap (MonoidHom.comp Y.ρ (MonoidHom.id H))) (↑X : Type u) (↑Y : Type u)] →
                    [SemilinearMapClass (X.ρ.IntertwiningMap (MonoidHom.comp Y.ρ (MonoidHom.id H))) (RingHom.id k)
                          (↑X : Type u) (↑Y : Type u)] →
                      (↑X : Type u) →ₗ[k] (↑Y : Type u)),
              isIntertwining' := ⋯ }))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousChains Y) n)

Tactic:
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
this : Mono X.f := ⋯
i : ℕ
⊢ (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker

Tactic:
have : LinearMap.range X.f.hom.toLinearMap = LinearMap.ker X.g.hom.toLinearMap :=
        (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker
-- 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
this_1 : Mono X.f := ⋯
i : ℕ
this : (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker
⊢ Exact (ShortComplex.map (X.map (chainsFunctor k G)) (HomologicalComplex.eval (ModuleCat k) (ComplexShape.down ℕ) i))

Tactic:
simp [moduleCat_exact_iff_range_eq_ker, ker_mapRange,
        range_mapRange_linearMap X.f.hom.toLinearMap (LinearMap.ker_eq_bot.2 <|
        (Rep.mono_iff_injective X.f).1 hX.mono_f), this]

Premises used: Iff.mpr, Finsupp.range_mapRange_linearMap, LinearMap.ker_eq_bot, Finsupp.ker_mapRange, CategoryTheory.ShortComplex.ShortExact.mono_f, Rep.Hom.hom, Iff.mp, CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker, CategoryTheory.ShortComplex.f, Rep.mono_iff_injective, Representation.IntertwiningMap.toLinearMap
-- 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
⊢ (mapShortComplex₁ hX hij).Exact

Tactic:
(map_chainsFunctor_shortExact hX).homology_exact₁ i j hij

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.SnakeInput.L₂', groupHomology.map_chainsFunctor_shortExact, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.ShortComplex.ShortExact.homology_exact₁, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ, CategoryTheory.ShortComplex.homologyMap
-- 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 : ℕ
⊢ (mapShortComplex₂ X i).Exact

Tactic:
(map_chainsFunctor_shortExact hX).homology_exact₂ i

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', groupHomology.map_chainsFunctor_shortExact, groupHomology, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.map, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap, CategoryTheory.ShortComplex.ShortExact.homology_exact₂
-- 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
⊢ (mapShortComplex₃ hX hij).Exact

Tactic:
(map_chainsFunctor_shortExact hX).homology_exact₃ i j hij

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', groupHomology.map_chainsFunctor_shortExact, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.ShortExact.homology_exact₃, CategoryTheory.ShortComplex.SnakeInput.L₁', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ, CategoryTheory.ShortComplex.homologyMap
-- 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
n : ℕ
h : IsZero (groupHomology X.X₂ n)
⊢ Epi (δ hX (n + 1) n ⋯)

Tactic:
SnakeInput.epi_δ _ h

Premises used: groupHomology, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.SnakeInput.epi_δ, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ
-- 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
n : ℕ
h : IsZero (groupHomology X.X₂ (n + 1))
⊢ Mono (δ hX (n + 1) n ⋯)

Tactic:
SnakeInput.mono_δ _ h

Premises used: CategoryTheory.ShortComplex.SnakeInput.mono_δ, groupHomology, CategoryTheory.ShortComplex.homology, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ
-- 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
n : ℕ
hs : IsZero (groupHomology X.X₂ (n + 1))
h : IsZero (groupHomology X.X₂ n)
⊢ IsIso (δ hX (n + 1) n ⋯)

Tactic:
SnakeInput.isIso_δ _ hs h

Premises used: CategoryTheory.ShortComplex.SnakeInput.isIso_δ, groupHomology, CategoryTheory.ShortComplex.homology, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ
-- 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 : ℕ
y : (Fin i → G) →₀ (↑X.X₂ : Type u)
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 (α := (↑((inhomogeneousChains X.X₁).X ((ComplexShape.down ℕ).next j)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (Y := (inhomogeneousChains X.X₁).X ((ComplexShape.down ℕ).next j))
            ((inhomogeneousChains X.X₁).d j ((ComplexShape.down ℕ).next j)) :
          (a : (↑((inhomogeneousChains X.X₁).X j) : Type u)) →
            (↑((inhomogeneousChains X.X₁).X ((ComplexShape.down ℕ).next j)) : Type u))
        x :
      (↑((inhomogeneousChains X.X₁).X ((ComplexShape.down ℕ).next j)) : Type u))
    (0 : (↑((inhomogeneousChains X.X₁).X ((ComplexShape.down ℕ).next j)) : Type u))

Tactic:
simpa using (map_chainsFunctor_shortExact hX).d_eq_zero_of_f_eq_d_apply i j y x
      (by simpa using hx) _

Premises used: CategoryTheory.ShortComplex.ShortExact.d_eq_zero_of_f_eq_d_apply, groupHomology.map_chainsFunctor_shortExact
-- 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))
⊢ (ComplexShape.down ℕ).next i = j

Tactic:
simp [← hij]
-- 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 (α := (↑((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))

Tactic:
simpa using hz