awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g : G
a : (↑A : Type u)
⊢ Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((((Multiplicative.toAdd :
                (a : Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))) →
                  (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
              ((MonoidHom.comp
                    ((AddMonoidHom.toMultiplicativeRight :
                        (a :
                            Additive (Abelianization G) →+
                              (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) →
                          Abelianization G →*
                            Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                      (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u))
                          (H1ToTensorOfIsTrivial A ∘ₗ TensorProduct.lift (mkH1OfIsTrivial A))).toAddMonoidHom)
                    Abelianization.of :
                  (a : G) → Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                g) :
            (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
          (a : (↑A : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((((Multiplicative.toAdd :
                (a : Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))) →
                  (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
              ((MonoidHom.comp
                    ((AddMonoidHom.toMultiplicativeRight :
                        (a :
                            Additive (Abelianization G) →+
                              (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) →
                          Abelianization G →*
                            Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                      (LinearMap.toAddMonoidHom
                        (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u))
                          LinearMap.id)))
                    Abelianization.of :
                  (a : G) → Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                g) :
            (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
          (a : (↑A : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))

Tactic:
simp [TensorProduct.mk_apply, TensorProduct.lift.tmul, mkH1OfIsTrivial_apply,
        H1ToTensorOfIsTrivial_H1π_single g a]

Premises used: TensorProduct.mk_apply, TensorProduct.lift.tmul, groupHomology.H1ToTensorOfIsTrivial_H1π_single, groupHomology.mkH1OfIsTrivial_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g : G
a : (↑A : Type u)
rw :
  Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((H1ToTensorOfIsTrivial A : (a : (↑(H1 A) : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
                (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))
              (single g a) :
            (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))) :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
          ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
rw₁ rw₂ :
  Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
          ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
          ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
⊢ Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((H1AddEquivOfIsTrivial A : (a : (↑(H1 A) : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
                (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))
              (single g a) :
            (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))) :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
          ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))

Tactic:
rw [H1AddEquivOfIsTrivial_apply, H1ToTensorOfIsTrivial_H1π_single g a]

Premises used: groupHomology.H1ToTensorOfIsTrivial_H1π_single, groupHomology.H1AddEquivOfIsTrivial_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g : G
a : (↑A : Type u)
⊢ Eq (α := (↑(H1 A) : Type u))
    (((H1AddEquivOfIsTrivial A).symm : (a : Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) → (↑(H1 A) : Type u))
        ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
              ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
            a :
          Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
      (↑(H1 A) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π A) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
              (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))
            (single g a) :
          (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) :
      (↑(H1 A) : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Epi (H2π A)

Tactic:
inferInstanceAs <| Epi (_ ≫ _)

Premises used: _private.0.groupHomology.instEpiModuleCatH2π._proof_1
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ Eq (α := (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 2).homology)
    ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)
    (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)

Tactic:
have h := leftHomologyπ_naturality'_assoc (isoShortComplexH2 A).inv
    (shortComplexH2 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousChains A).sc 2).leftHomologyIso.hom
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
h :
  Eq (α := (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 2).homology)
    ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)
    (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)
simp :
  Eq (α := (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
      ((ModuleCat.Hom.hom (shortComplexH2 A).moduleCatLeftHomologyData.π :
            (a : ↥(cycles₂ A)) → (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
          x :
        (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
      (0 : (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u)) ↔
    (↑x : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A
⊢ Eq (α := (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          x :
        (↑(H2 A) : Type u))
      (0 : (↑(H2 A) : Type u)) ↔
    (↑x : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A

Tactic:
simp only [H2π, isoCycles₂, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.leftHomologyπ, groupHomology.H2π, CategoryTheory.ShortComplex.cyclesMapIso'_inv, inferInstance, ModuleCat.mono_iff_injective, LinearMap.coe_comp, map_eq_zero_iff, CategoryTheory.ShortComplex.leftHomologyMapIso'_inv, Iff.mp, Function.comp_apply, groupHomology.isoCycles₂, ModuleCat.hom_comp, groupHomology.π
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
h :
  Eq (α := (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 2).homology)
    ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)
    (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)
⊢ Eq (α := (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
      ((ModuleCat.Hom.hom (shortComplexH2 A).moduleCatLeftHomologyData.π :
            (a : ↥(cycles₂ A)) → (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
          x :
        (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
      (0 : (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u)) ↔
    (↑x : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A

Tactic:
simp [LinearMap.range_codRestrict, boundaries₂, shortComplexH2, cycles₂]

Premises used: groupHomology.boundaries₂, groupHomology.cycles₂, groupHomology.shortComplexH2, LinearMap.range_codRestrict
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cycles₂ A)
rw :
  (↑(x - y) : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A ↔
    (↑x : G × G →₀ (↑A : Type u)) - (↑y : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A
⊢ Eq (α := (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          x :
        (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          y :
        (↑(H2 A) : Type u)) ↔
    (↑x : G × G →₀ (↑A : Type u)) - (↑y : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A

Tactic:
rw [← sub_eq_zero, ← map_sub, H2π_eq_zero_iff]

Premises used: map_sub, sub_eq_zero, groupHomology.H2π_eq_zero_iff
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cycles₂ A)
⊢ (↑(x - y) : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A ↔
    (↑x : G × G →₀ (↑A : Type u)) - (↑y : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
C : (↑(H2 A) : Type u) → Prop
x : (↑(H2 A) : Type u)
h :
  ∀ (x : ↥(cycles₂ A)),
    C
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H2π A) :
          (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
        x)
y : (↑(cycles A 2) : Type u)
⊢ C
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := cycles A 2) (π A 2) :
        (a : (↑(cycles A 2) : Type u)) → (↑(groupHomology A 2) : Type u))
      y)

Tactic:
simpa [H2π] using h ((isoCycles₂ A).hom y)

Premises used: CategoryTheory.ConcreteCategory.hom, groupHomology.H2π, groupHomology.isoCycles₂, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ π A 2 ≫ (H2Iso A).hom = (isoCycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.π

Tactic:
simp [H2Iso, isoCycles₂, π, HomologicalComplex.homologyπ, leftHomologyπ]

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.leftHomologyπ, groupHomology.isoCycles₂, groupHomology.H2Iso, groupHomology.π
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (shortComplexH2 A).moduleCatLeftHomologyData.π ≫ (H2Iso A).inv = H2π A

Tactic:
(CommSq.vert_inv ⟨π_comp_H2Iso_hom A⟩).w

Premises used: Set.Mem, groupHomology.H2π, CategoryTheory.CommSq.vert_inv, groupHomology.π_comp_H2Iso_hom, CategoryTheory.CommSq.mk, groupHomology.cycles₂, CategoryTheory.CommSq.w
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
X Y : SimplexCategoryᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := Action (Type u) G) (Functor.obj (cechNerveTerminalFrom (Action.ofMulAction G G)) X)
      (Functor.obj (classifyingSpaceUniversalCover G) Y))
    (CategoryTheory.Functor.map (cechNerveTerminalFrom (Action.ofMulAction G G)) f ≫
      Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G) :
              Iso (C := Action (Type u) G)
                (limit (J := Discrete (Fin ((Opposite.unop x).len + 1)))
                  (Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G))
                (Cone.pt (J := Discrete (Fin ((Opposite.unop x).len + 1))) (F :=
                  Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G)
                  (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)))))
          Y))
    (Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G) :
              Iso (C := Action (Type u) G)
                (limit (J := Discrete (Fin ((Opposite.unop x).len + 1)))
                  (Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G))
                (Cone.pt (J := Discrete (Fin ((Opposite.unop x).len + 1))) (F :=
                  Discrete.functor fun (i : Fin ((Opposite.unop x).len + 1)) ↦ Action.ofMulAction G G)
                  (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)))))
          X) ≫
      CategoryTheory.Functor.map (classifyingSpaceUniversalCover G) f)

Tactic:
IsLimit.hom_ext (Action.ofMulActionLimitCone.{u, 0} G fun _ => G).2 fun j => ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, Action.ofMulActionLimitCone, CategoryTheory.Limits.LimitCone.isLimit
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
X Y : SimplexCategoryᵒᵖ
f : X ⟶ Y
j : Discrete (Fin ((Opposite.unop Y).len + 1))
⊢ Eq (α :=
    Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
      (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
    (NatTrans.app
        (Cone.π
          (Fan.mk (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
            fun (i : Fin ((Opposite.unop Y).len + 1)) ↦
            Pi.π (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
              ((SimplexCategory.Hom.toOrderHom f.unop :
                  (a : Fin ((Opposite.unop Y).len + 1)) → Fin ((Opposite.unop X).len + 1))
                i)))
        j :
      Quiver.Hom (V := Action (Type u) G)
        (Functor.obj
          (Functor.obj (Functor.const (Discrete (Fin ((Opposite.unop Y).len + 1))))
            (Cone.pt (J := Discrete (Fin ((Opposite.unop Y).len + 1))) (F :=
              Discrete.functor fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
              (Fan.mk (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                fun (i : Fin ((Opposite.unop Y).len + 1)) ↦
                Pi.π (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                  ((SimplexCategory.Hom.toOrderHom f.unop :
                      (a : Fin ((Opposite.unop Y).len + 1)) → Fin ((Opposite.unop X).len + 1))
                    i))))
          j)
        (Functor.obj (Discrete.functor fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
    (CategoryStruct.comp (Y := Functor.obj (classifyingSpaceUniversalCover G) X)
        (Iso.hom (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop X).len + 1)) ↦ G)) :
          Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
            (Functor.obj (classifyingSpaceUniversalCover G) X))
        (CategoryTheory.Functor.map (classifyingSpaceUniversalCover G) f ≫
            NatTrans.app
              (Cone.π (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G)))
              j :
          Quiver.Hom (V := Action (Type u) G) (Functor.obj (classifyingSpaceUniversalCover G) X)
            (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j)) :
      Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
        (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))

Tactic:
(limit.isoLimitCone_hom_π _ _).symm

Premises used: CategoryTheory.Limits.limit.π, Action.Hom.comp, CategoryTheory.Limits.limit.isoLimitCone_hom_π, TypeCat.Fun.comp, Eq.symm
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
X Y : SimplexCategoryᵒᵖ
f : X ⟶ Y
j : Discrete (Fin ((Opposite.unop Y).len + 1))
⊢ Eq (α :=
    Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
      (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
    (NatTrans.app
        (Cone.π
          (Fan.mk (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
            fun (i : Fin ((Opposite.unop Y).len + 1)) ↦
            Pi.π (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
              ((SimplexCategory.Hom.toOrderHom f.unop :
                  (a : Fin ((Opposite.unop Y).len + 1)) → Fin ((Opposite.unop X).len + 1))
                i)))
        j :
      Quiver.Hom (V := Action (Type u) G)
        (Functor.obj
          (Functor.obj (Functor.const (Discrete (Fin ((Opposite.unop Y).len + 1))))
            (Cone.pt (J := Discrete (Fin ((Opposite.unop Y).len + 1))) (F :=
              Discrete.functor fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G)
              (Fan.mk (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                fun (i : Fin ((Opposite.unop Y).len + 1)) ↦
                Pi.π (fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
                  ((SimplexCategory.Hom.toOrderHom f.unop :
                      (a : Fin ((Opposite.unop Y).len + 1)) → Fin ((Opposite.unop X).len + 1))
                    i))))
          j)
        (Functor.obj (Discrete.functor fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))
    (CategoryStruct.comp (Y := Functor.obj (classifyingSpaceUniversalCover G) X)
        (Iso.hom (limit.isoLimitCone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop X).len + 1)) ↦ G)) :
          Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
            (Functor.obj (classifyingSpaceUniversalCover G) X))
        (CategoryTheory.Functor.map (classifyingSpaceUniversalCover G) f ≫
            NatTrans.app
              (Cone.π (LimitCone.cone (Action.ofMulActionLimitCone G fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ G)))
              j :
          Quiver.Hom (V := Action (Type u) G) (Functor.obj (classifyingSpaceUniversalCover G) X)
            (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j)) :
      Quiver.Hom (V := Action (Type u) G) (∏ᶜ fun (x : Fin ((Opposite.unop X).len + 1)) ↦ Action.ofMulAction G G)
        (Functor.obj (Discrete.functor fun (i : Fin ((Opposite.unop Y).len + 1)) ↦ Action.ofMulAction G G) j))

Tactic:
exact (limit.isoLimitCone_hom_π _ _).symm

Premises used: CategoryTheory.Limits.limit.isoLimitCone_hom_π, Eq.symm