awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
refine :
  ∀ {X Y : SimplexCategoryᵒᵖ} (x : X ⟶ Y),
    Eq (α :=
      Functor.obj (cechNerveTerminalFrom G) X ⟶
        (classifyingSpaceUniversalCover G ⋙
              forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
                fun (X : Action (Type u) G) ↦ X.V)).obj
          Y)
      (CategoryTheory.Functor.map (cechNerveTerminalFrom G) x ≫
        Iso.hom
          ((fun (x : SimplexCategoryᵒᵖ) ↦
              (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                  ((j : Fin ((Opposite.unop x).len + 1)) → G)))
            Y))
      (Iso.hom
          ((fun (x : SimplexCategoryᵒᵖ) ↦
              (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                  ((j : Fin ((Opposite.unop x).len + 1)) → G)))
            X) ≫
        (classifyingSpaceUniversalCover G ⋙
              forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
                fun (X : Action (Type u) G) ↦ X.V)).map
          x)
⊢ cechNerveTerminalFrom G ≅
    classifyingSpaceUniversalCover G ⋙
      forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
        fun (X : Action (Type u) G) ↦ X.V)

Tactic:
refine NatIso.ofComponents (fun _ => Types.productIso _) fun _ => ?_

Premises used: CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
X Y : SimplexCategoryᵒᵖ
x : X ⟶ Y
h :
  Eq (α :=
    Functor.obj (cechNerveTerminalFrom G) X →
      (classifyingSpaceUniversalCover G ⋙
            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
              fun (X : Action (Type u) G) ↦ X.V)).obj
        Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryTheory.Functor.map (cechNerveTerminalFrom G) x ≫
          Iso.hom
            ((fun (x : SimplexCategoryᵒᵖ) ↦
                (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                  Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                    ((j : Fin ((Opposite.unop x).len + 1)) → G)))
              Y))))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : SimplexCategoryᵒᵖ) ↦
                (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                  Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                    ((j : Fin ((Opposite.unop x).len + 1)) → G)))
              X) ≫
          (classifyingSpaceUniversalCover G ⋙
                forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
                  fun (X : Action (Type u) G) ↦ X.V)).map
            x)))
⊢ Eq (α :=
    Functor.obj (cechNerveTerminalFrom G) X ⟶
      (classifyingSpaceUniversalCover G ⋙
            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
              fun (X : Action (Type u) G) ↦ X.V)).obj
        Y)
    (CategoryTheory.Functor.map (cechNerveTerminalFrom G) x ≫
      Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
              Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                ((j : Fin ((Opposite.unop x).len + 1)) → G)))
          Y))
    (Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
              Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                ((j : Fin ((Opposite.unop x).len + 1)) → G)))
          X) ≫
      (classifyingSpaceUniversalCover G ⋙
            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
              fun (X : Action (Type u) G) ↦ X.V)).map
        x)

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
X Y : SimplexCategoryᵒᵖ
x : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (cechNerveTerminalFrom G) X →
      (classifyingSpaceUniversalCover G ⋙
            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
              fun (X : Action (Type u) G) ↦ X.V)).obj
        Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryTheory.Functor.map (cechNerveTerminalFrom G) x ≫
          Iso.hom
            ((fun (x : SimplexCategoryᵒᵖ) ↦
                (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                  Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                    ((j : Fin ((Opposite.unop x).len + 1)) → G)))
              Y))))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : SimplexCategoryᵒᵖ) ↦
                (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                  Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                    ((j : Fin ((Opposite.unop x).len + 1)) → G)))
              X) ≫
          (classifyingSpaceUniversalCover G ⋙
                forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
                  fun (X : Action (Type u) G) ↦ X.V)).map
            x)))

Tactic:
Matrix.ext fun _ _ => Pi.lift_π_apply (f := fun _ ↦ G) _ _ _

Premises used: Matrix, Quiver.Hom.unop, CategoryTheory.Limits.Pi.π, SimplexCategory.Hom.toOrderHom, DFunLike.coe, Matrix.ext, CategoryTheory.Limits.Pi.lift_π_apply
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
X Y : SimplexCategoryᵒᵖ
x : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (cechNerveTerminalFrom G) X →
      (classifyingSpaceUniversalCover G ⋙
            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
              fun (X : Action (Type u) G) ↦ X.V)).obj
        Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryTheory.Functor.map (cechNerveTerminalFrom G) x ≫
          Iso.hom
            ((fun (x : SimplexCategoryᵒᵖ) ↦
                (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                  Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                    ((j : Fin ((Opposite.unop x).len + 1)) → G)))
              Y))))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : SimplexCategoryᵒᵖ) ↦
                (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                  Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                    ((j : Fin ((Opposite.unop x).len + 1)) → G)))
              X) ≫
          (classifyingSpaceUniversalCover G ⋙
                forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
                  fun (X : Action (Type u) G) ↦ X.V)).map
            x)))

Tactic:
exact Matrix.ext fun _ _ => Pi.lift_π_apply (f := fun _ ↦ G) _ _ _

Premises used: Matrix.ext, CategoryTheory.Limits.Pi.lift_π_apply
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
this : (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve ≅ compForgetAugmented G
⊢ (compForgetAugmented G).ExtraDegeneracy

Tactic:
refine
    ExtraDegeneracy.ofIso (?_ : (Arrow.mk <| terminal.from G).augmentedCechNerve ≅ _)
      (extraDegeneracyAugmentedCechNerve G)

Premises used: classifyingSpaceUniversalCover.extraDegeneracyAugmentedCechNerve, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ofIso
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
w :
  ∀ (n : SimplexCategoryᵒᵖ),
    NatTrans.app
        (CategoryTheory.Functor.map (𝟭 (SimplicialObject (Type u)))
            (Iso.hom (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)) ≫
          (compForgetAugmented G).hom)
        n =
      ((Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.hom ≫
            CategoryTheory.Functor.map (SimplicialObject.const (Type u))
              (Iso.hom (Iso.refl (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.right))).app
        n
⊢ CategoryTheory.Functor.map (𝟭 (SimplicialObject (Type u)))
        (Iso.hom (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)) ≫
      (compForgetAugmented G).hom =
    (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.hom ≫
      CategoryTheory.Functor.map (SimplicialObject.const (Type u))
        (Iso.hom (Iso.refl (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.right))

Tactic:
ext : 1
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
n_1 : SimplexCategoryᵒᵖ
⊢ NatTrans.app
      (CategoryTheory.Functor.map (𝟭 (SimplicialObject (Type u)))
          (Iso.hom (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)) ≫
        (compForgetAugmented G).hom)
      n_1 =
    ((Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.hom ≫
          CategoryTheory.Functor.map (SimplicialObject.const (Type u))
            (Iso.hom (Iso.refl (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.right))).app
      n_1

Tactic:
IsTerminal.hom_ext terminalIsTerminal _ _

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
n_1 : SimplexCategoryᵒᵖ
⊢ NatTrans.app
      (CategoryTheory.Functor.map (𝟭 (SimplicialObject (Type u)))
          (Iso.hom (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)) ≫
        (compForgetAugmented G).hom)
      n_1 =
    ((Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.hom ≫
          CategoryTheory.Functor.map (SimplicialObject.const (Type u))
            (Iso.hom (Iso.refl (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.right))).app
      n_1

Tactic:
exact IsTerminal.hom_ext terminalIsTerminal _ _

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
⊢ (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve ≅ compForgetAugmented G

Tactic:
exact
    Comma.isoMk (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)
      (Iso.refl _) (by ext : 1; exact IsTerminal.hom_ext terminalIsTerminal _ _)

Premises used: CategoryTheory.Comma.isoMk, CategoryTheory.Iso.refl, CategoryTheory.Iso.trans
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
c : Fin (n + 1) → G
⊢ Eq (α := (Fin n → G) →₀ k)
    ((d k G n : (a : (Fin (n + 1) → G) →₀ k) → (Fin n → G) →₀ k) (single c 1) : (Fin n → G) →₀ k)
    (∑ p : Fin (n + 1), single (c ∘ p.succAbove) (HPow.hPow (α := k) (-1) (↑p : ℕ)) : (Fin n → G) →₀ k)

Tactic:
simp [d]

Premises used: Rep.standardComplex.d
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
rw :
  HSMul.hSMul (β := (Fin n → G) →₀ k) r
      (∑ p : Fin (n + 1), single (c ∘ p.succAbove) (HPow.hPow (α := k) (-1) (↑p : ℕ))) =
    ∑ p : Fin (n + 1), single (c ∘ p.succAbove) (HSMul.hSMul (β := k) r 1 * HPow.hPow (α := k) (-1) (↑p : ℕ))
⊢ Eq (α := (Fin n → G) →₀ k)
    ((d k G n : (a : (Fin (n + 1) → G) →₀ k) → (Fin n → G) →₀ k) (single c r) : (Fin n → G) →₀ k)
    (∑ p : Fin (n + 1), single (c ∘ p.succAbove) (r * HPow.hPow (α := k) (-1) (↑p : ℕ)) : (Fin n → G) →₀ k)

Tactic:
rw [← mul_one r, ← smul_eq_mul, ← smul_single, map_smul, d_of]

Premises used: Rep.standardComplex.d_of, smul_eq_mul, mul_one, Finsupp.smul_single, map_smul
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ HSMul.hSMul (β := (Fin n → G) →₀ k) r
      (∑ p : Fin (n + 1), single (c ∘ p.succAbove) (HPow.hPow (α := k) (-1) (↑p : ℕ))) =
    ∑ p : Fin (n + 1), single (c ∘ p.succAbove) (HSMul.hSMul (β := k) r 1 * HPow.hPow (α := k) (-1) (↑p : ℕ))

Tactic:
simp [Finset.smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G_1 : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
n : ℕ
⊢ Projective (C := Rep k G) (HomologicalComplex.X (standardComplex k G) n)

Tactic:
inferInstanceAs <| Projective (Rep.diagonal k G (n + 1))

Premises used: _private.0.Rep.standardComplex.x_projective._proof_1
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G_1 : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
n : ℕ
⊢ Projective (C := Rep k G) (HomologicalComplex.X (standardComplex k G) n)

Tactic:
exact inferInstanceAs <| Projective (Rep.diagonal k G (n + 1))
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G_1 : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
n : ℕ
⊢ Projective (C := Rep k G) (HomologicalComplex.X (standardComplex k G) n)

Tactic:
classical exact inferInstanceAs <| Projective (Rep.diagonal k G (n + 1))
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
n : ℕ
⊢ Eq (α :=
    (↑(HomologicalComplex.X (standardComplex k G) (n + 1)) : Type u) →ₗ[k]
      (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    (Representation.IntertwiningMap.toLinearMap (Hom.hom (HomologicalComplex.d (standardComplex k G) (n + 1) n)))
    (d k G (n + 1))

Tactic:
Finsupp.lhom_ext' fun (x : Fin (n + 2) → G) => LinearMap.ext_ring ?_

Premises used: Finsupp.lhom_ext', LinearMap.ext_ring
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
n : ℕ
refine :
  ∀ (x : Fin (n + 2) → G),
    Eq (α := (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
      ((Representation.IntertwiningMap.toLinearMap (Hom.hom (HomologicalComplex.d (standardComplex k G) (n + 1) n)) ∘ₗ
            lsingle x :
          (a : k) → (↑((standardComplex k G).X n) : Type u))
        1)
      ((d k G (n + 1) ∘ₗ lsingle x : (a : k) → (↑((standardComplex k G).X n) : Type u)) 1)
⊢ Eq (α :=
    (↑(HomologicalComplex.X (standardComplex k G) (n + 1)) : Type u) →ₗ[k]
      (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    (Representation.IntertwiningMap.toLinearMap (Hom.hom (HomologicalComplex.d (standardComplex k G) (n + 1) n)))
    (d k G (n + 1))

Tactic:
refine Finsupp.lhom_ext' fun (x : Fin (n + 2) → G) => LinearMap.ext_ring ?_

Premises used: Finsupp.lhom_ext', LinearMap.ext_ring
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
n : ℕ
x : Fin (n + 2) → G
⊢ Eq (α := (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom (HomologicalComplex.d (standardComplex k G) (n + 1) n)) ∘ₗ
          lsingle x :
        (a : k) → (↑((standardComplex k G).X n) : Type u))
      1)
    ((d k G (n + 1) ∘ₗ lsingle x : (a : k) → (↑((standardComplex k G).X n) : Type u)) 1)

Tactic:
simp [standardComplex, Action.ofMulAction_V, SimplicialObject.δ, SimplexCategory.δ,
    Fin.succAboveOrderEmb, ← Int.cast_smul_eq_zsmul k ((-1) ^ _ : ℤ), ← ofHom_smul, ← ofHom_sum,
    Representation.IntertwiningMap.coe_toLinearMap, Representation.IntertwiningMap.sum_apply,
    Representation.IntertwiningMap.smul_apply, (Representation.linearizeMap_single), smul_single,
    smul_eq_mul, mul_one]

Premises used: Representation.IntertwiningMap.coe_toLinearMap, SimplexCategory.δ, Representation.IntertwiningMap.smul_apply, Representation.IntertwiningMap.sum_apply, Fin.succAboveOrderEmb, HPow.hPow, Representation.linearizeMap_single, Rep.standardComplex, Rep.ofHom_sum, smul_eq_mul, mul_one, CategoryTheory.SimplicialObject.δ, OfNat.ofNat, Finsupp.smul_single, Int.cast_smul_eq_zsmul, Action.ofMulAction_V, Neg.neg, Rep.ofHom_smul
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
n : ℕ
f : (Fin (n + 1 + 1) → G) →₀ k
rw :
  Eq (α := (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((d k G (n + 1) : (a : (↑((standardComplex k G).X (n + 1)) : Type u)) → (↑((standardComplex k G).X n) : Type u)) f :
      (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((d k G (n + 1) : (a : (Fin (n + 1 + 1) → G) →₀ k) → (Fin (n + 1) → G) →₀ k) f : (Fin (n + 1) → G) →₀ k)
⊢ Eq (α := (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((Hom.hom (HomologicalComplex.d (standardComplex k G) (n + 1) n) :
          (a : (↑((standardComplex k G).X (n + 1)) : Type u)) → (↑((standardComplex k G).X n) : Type u))
        f :
      (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((d k G (n + 1) : (a : (Fin (n + 1 + 1) → G) →₀ k) → (Fin (n + 1) → G) →₀ k) f : (Fin (n + 1) → G) →₀ k)

Tactic:
rw [← Representation.IntertwiningMap.toLinearMap_apply, d_eq]

Premises used: Rep.standardComplex.d_eq, Representation.IntertwiningMap.toLinearMap_apply
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
n : ℕ
f : (Fin (n + 1 + 1) → G) →₀ k
⊢ Eq (α := (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((d k G (n + 1) : (a : (↑((standardComplex k G).X (n + 1)) : Type u)) → (↑((standardComplex k G).X n) : Type u)) f :
      (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((d k G (n + 1) : (a : (Fin (n + 1 + 1) → G) →₀ k) → (Fin (n + 1) → G) →₀ k) f : (Fin (n + 1) → G) →₀ k)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
x : G
x_1 : Fin 1 → G
⊢ Eq (α := k)
    ((((linearCombination k fun (x : Fin 1 → G) ↦ 1) ∘ₗ
              (Representation.ofMulAction k G (Fin 1 → G) : (a : G) → ((Fin 1 → G) →₀ k) →ₗ[k] (Fin 1 → G) →₀ k) x) ∘ₗ
            lsingle x_1 :
          (a : k) → k)
        1 :
      k)
    ((((Representation.trivial k G k : (a : G) → k →ₗ[k] k) x ∘ₗ linearCombination k fun (x : Fin 1 → G) ↦ 1) ∘ₗ
            lsingle x_1 :
          (a : k) → k)
        1 :
      k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
⊢ Eq (α :=
    HomologicalComplex.X (forget₂ToModuleCat k G) 0 ⟶
      HomologicalComplex.X
        (Functor.obj (ChainComplex.single₀ (ModuleCat k))
          (Functor.obj
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
            (trivial k G k)))
        0)
    (HomologicalComplex.Hom.f (HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G)) 0)
    (CategoryTheory.Functor.map
      (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
        fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
      (ε k G))

Tactic:
ModuleCat.hom_ext <| Finsupp.lhom_ext fun (x : Fin 1 → G) r => ?_

Premises used: Finsupp.lhom_ext, ModuleCat.hom_ext
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
hf :
  ∀ (x : (↑(HomologicalComplex.X (standardComplex k G) 1) : Type u)),
    Eq (α := (↑(trivial k G k) : Type u))
      ((Representation.IntertwiningMap.toLinearMap (Hom.hom (HomologicalComplex.d (standardComplex k G) 1 0 ≫ ε k G)) :
            (a : (↑((standardComplex k G).X 1) : Type u)) → (↑(trivial k G k) : Type u))
          x :
        (↑(trivial k G k) : Type u))
      ((Representation.IntertwiningMap.toLinearMap (Hom.hom 0) :
            (a : (↑((standardComplex k G).X 1) : Type u)) → (↑(trivial k G k) : Type u))
          x :
        (↑(trivial k G k) : Type u))
⊢ Eq (α := Quiver.Hom (V := Rep k G) (HomologicalComplex.X (standardComplex k G) 1) (trivial k G k))
    (HomologicalComplex.d (standardComplex k G) 1 0 ≫ ε k G) 0

Tactic:
ext : 3
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
x : (↑(HomologicalComplex.X (standardComplex k G) 1) : Type u)
rw :
  Eq (α :=
    HomologicalComplex.X (forget₂ToModuleCat k G) 1 ⟶
      Functor.obj
        (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
          fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (trivial k G k))
    (HomologicalComplex.Hom.f (HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G)) 1 ≫
        HomologicalComplex.d
          (Functor.obj (ChainComplex.single₀ (ModuleCat k))
            (Functor.obj
              (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              (trivial k G k)))
          1 0 :
      HomologicalComplex.X (forget₂ToModuleCat k G) 1 ⟶
        HomologicalComplex.X
          (Functor.obj (ChainComplex.single₀ (ModuleCat k))
            (Functor.obj
              (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              (trivial k G k)))
          0)
    0
⊢ Eq (α :=
    HomologicalComplex.X (forget₂ToModuleCat k G) 1 ⟶
      Functor.obj
        (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
          fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (trivial k G k))
    (CategoryStruct.comp (Y := HomologicalComplex.X (forget₂ToModuleCat k G) 0)
      (HomologicalComplex.d (forget₂ToModuleCat k G) 1 0)
      (CategoryTheory.Functor.map
        (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
          fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (ε k G)))
    0

Tactic:
rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq,
      ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]

Premises used: HomotopyEquiv.hom, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, HomologicalComplex.Hom.comm', OfNat.ofNat, rfl