awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
succ :
  ShortComplex.Exact (C := Rep k G)
    (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
⊢ QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) (m + 1)

Tactic:
rw [quasiIsoAt_iff_exactAt' (hL := ChainComplex.exactAt_succ_single_obj ..),
          HomologicalComplex.exactAt_iff' _ (m + 2) (m + 1) m (by simp) (by simp)]

Premises used: ChainComplex.exactAt_succ_single_obj, HAdd.hAdd, OfNat.ofNat, quasiIsoAt_iff_exactAt', HomologicalComplex.exactAt_iff'
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
succ :
  ShortComplex.Exact
    (ShortComplex.map
      (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
      (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)))
⊢ ShortComplex.Exact (C := Rep k G)
    (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)

Tactic:
apply (forget₂ _ (ModuleCat k)).reflects_exact_of_faithful

Premises used: ModuleCat, CategoryTheory.forget₂, CategoryTheory.Functor.reflects_exact_of_faithful
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
succ :
  Eq (α :=
    Submodule k
      (↑(ShortComplex.X₂
            (ShortComplex.map
              (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
              (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)))) :
        Type u))
    (LinearMap.range
      (ModuleCat.Hom.hom
        (ShortComplex.f
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (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))))))
    (LinearMap.ker
      (ModuleCat.Hom.hom
        (ShortComplex.g
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (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))))))
⊢ ShortComplex.Exact
    (ShortComplex.map
      (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
      (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)))

Tactic:
rw [ShortComplex.moduleCat_exact_iff_range_eq_ker]

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
hm : Odd (m + 1)
⊢ Eq (α :=
    Submodule k
      (↑(ShortComplex.X₂
            (ShortComplex.map
              (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
              (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)))) :
        Type u))
    (LinearMap.range
      (ModuleCat.Hom.hom
        (ShortComplex.f
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (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))))))
    (LinearMap.ker
      (ModuleCat.Hom.hom
        (ShortComplex.g
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (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))))))

Tactic:
simpa [if_pos (Nat.even_add_one.2 (Nat.not_even_iff_odd.2 hm)),
          if_neg (Nat.not_even_iff_odd.2 hm)]
          using leftRegular.range_norm_eq_ker_applyAsHom_sub k g hg

Premises used: Iff.mpr, Nat.even_add_one, Nat.not_even_iff_odd, if_pos, Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, if_neg
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
hm : ¬Odd (m + 1)
⊢ Eq (α :=
    Submodule k
      (↑(ShortComplex.X₂
            (ShortComplex.map
              (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
              (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)))) :
        Type u))
    (LinearMap.range
      (ModuleCat.Hom.hom
        (ShortComplex.f
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (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))))))
    (LinearMap.ker
      (ModuleCat.Hom.hom
        (ShortComplex.g
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (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))))))

Tactic:
simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker, if_pos (Nat.not_odd_iff_even.1 hm),
          if_neg (Nat.not_even_iff_odd.2 <| Nat.odd_add_one.2 hm)]
        using leftRegular.range_applyAsHom_sub_eq_ker_norm k g hg

Premises used: Iff.mpr, Nat.odd_add_one, Nat.not_odd_iff_even, Nat.not_even_iff_odd, if_pos, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, Iff.mp, CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker, if_neg
-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
zero : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) 0
succ :
  ∀ (m : ℕ),
    QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m →
      QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g)
        (m + 1)
⊢ QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m

Tactic:
induction m with
    | zero =>
      simp only [resolution.π]
      rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros' _ rfl rfl rfl]
      constructor
      · apply (forget₂ _ (ModuleCat k)).reflects_exact_of_faithful
        simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker,
          HomologicalComplex.alternatingConst, ChainComplex.toSingle₀Equiv] using
          leftRegular.range_applyAsHom_sub_eq_ker_linearCombination k g hg
      · rw [Rep.epi_iff_surjective]
        intro x
        use single 1 x
        simp [ChainComplex.toSingle₀Equiv]
    | succ m _ =>
      rw [quasiIsoAt_iff_exactAt' (hL := ChainComplex.exactAt_succ_single_obj ..),
          HomologicalComplex.exactAt_iff' _ (m + 2) (m + 1) m (by simp) (by simp)]
      apply (forget₂ _ (ModuleCat k)).reflects_exact_of_faithful
      rw [ShortComplex.moduleCat_exact_iff_range_eq_ker]
      by_cases hm : Odd (m + 1)
      · simpa [if_pos (Nat.even_add_one.2 (Nat.not_even_iff_odd.2 hm)),
          if_neg (Nat.not_even_iff_odd.2 hm)]
          using leftRegular.range_norm_eq_ker_applyAsHom_sub k g hg
      · simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker, if_pos (Nat.not_odd_iff_even.1 hm),
          if_neg (Nat.not_even_iff_odd.2 <| Nat.odd_add_one.2 hm)]
        using leftRegular.range_applyAsHom_sub_eq_ker_norm k g hg

Premises used: ModuleCat, HomologicalComplex.alternatingConst, ChainComplex.toSingle₀Equiv, Odd, ChainComplex.exactAt_succ_single_obj, ChainComplex.quasiIsoAt₀_iff, CategoryTheory.ShortComplex.quasiIso_iff_of_zeros', CategoryTheory.forget₂, HAdd.hAdd, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker, Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, Rep.epi_iff_surjective, OfNat.ofNat, Rep.FiniteCyclicGroup.resolution.π, quasiIsoAt_iff_exactAt', HomologicalComplex.exactAt_iff', CategoryTheory.Functor.reflects_exact_of_faithful, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Monoid G
A : Rep.{u_1, u, u} k G
n : ℕ
f g : (Fin n → G) → (↑A : Type u_1)
x : Fin (n + 1) → G
⊢ HAdd.hAdd (α := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (x 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        ((f + g) fun (i : Fin n) ↦ x i.succ))
      (∑ j : Fin (n + 1),
        HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • (f + g) (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) x)) =
    HAdd.hAdd (α := (Fin (n + 1) → G) → (↑A : Type u_1)) (β := (Fin (n + 1) → G) → (↑A : Type u_1))
      (fun (g : Fin (n + 1) → G) ↦
        HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f fun (i : Fin n) ↦ g i.succ) :
            (↑A : Type u_1))
          (∑ j : Fin (n + 1), HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • f (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) :
            (↑A : Type u_1)))
      (fun (g_1 : Fin (n + 1) → G) ↦
        HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g_1 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (g fun (i : Fin n) ↦ g_1 i.succ) :
            (↑A : Type u_1))
          (∑ j : Fin (n + 1),
              HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • g (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g_1) :
            (↑A : Type u_1)))
      x

Tactic:
simp [Finset.sum_add_distrib, add_add_add_comm]

Premises used: Finset.sum_add_distrib, add_add_add_comm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Monoid G
A : Rep.{u_1, u, u} k G
n : ℕ
r : k
f : (Fin n → G) → (↑A : Type u_1)
h :
  ∀ (x : Fin (n + 1) → G),
    HAdd.hAdd (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (x 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((r • f) fun (i : Fin n) ↦ x i.succ))
        (∑ j : Fin (n + 1),
          HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • (r • f) (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) x)) =
      HSMul.hSMul (α := k) (β := (Fin (n + 1) → G) → (↑A : Type u_1)) ((RingHom.id k : (a : k) → k) r : k)
        (fun (g : Fin (n + 1) → G) ↦
          HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (f fun (i : Fin n) ↦ g i.succ) :
              (↑A : Type u_1))
            (∑ j : Fin (n + 1),
                HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • f (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) :
              (↑A : Type u_1)))
        x
⊢ (fun (g : Fin (n + 1) → G) ↦
      HAdd.hAdd (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((r • f) fun (i : Fin n) ↦ g i.succ))
        (∑ j : Fin (n + 1),
          HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • (r • f) (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g))) =
    HSMul.hSMul (α := k) (β := (Fin (n + 1) → G) → (↑A : Type u_1)) ((RingHom.id k : (a : k) → k) r : k)
      fun (g : Fin (n + 1) → G) ↦
      HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (f fun (i : Fin n) ↦ g i.succ) :
          (↑A : Type u_1))
        (∑ j : Fin (n + 1), HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • f (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) :
          (↑A : Type u_1))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Monoid G
A : Rep.{u_1, u, u} k G
n : ℕ
r : k
f : (Fin n → G) → (↑A : Type u_1)
x : Fin (n + 1) → G
⊢ HAdd.hAdd (α := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (x 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        ((r • f) fun (i : Fin n) ↦ x i.succ))
      (∑ j : Fin (n + 1),
        HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • (r • f) (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) x)) =
    HSMul.hSMul (α := k) (β := (Fin (n + 1) → G) → (↑A : Type u_1)) ((RingHom.id k : (a : k) → k) r : k)
      (fun (g : Fin (n + 1) → G) ↦
        HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f fun (i : Fin n) ↦ g i.succ) :
            (↑A : Type u_1))
          (∑ j : Fin (n + 1), HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • f (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) :
            (↑A : Type u_1)))
      x

Tactic:
simp [Finset.smul_sum, ← smul_assoc, mul_comm r]

Premises used: smul_assoc, Finset.smul_sum, mul_comm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
hf :
  ∀ (x : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)) (x_1 : Fin (n + 1) → G),
    Eq (α := (↑A : Type u))
      ((ModuleCat.Hom.hom (d A n) :
            (a : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)) →
              (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
          x x_1 :
        (↑A : Type u))
      ((ModuleCat.Hom.hom
              (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
                HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1) ≫
                  Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A))) :
            (a : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)) →
              (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
          x x_1 :
        (↑A : Type u))
⊢ d A n =
    Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
      HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1) ≫
        Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
x : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)
x_1 : Fin (n + 1) → G
⊢ Eq (α := (↑A : Type u))
    ((ModuleCat.Hom.hom (d A n) :
          (a : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
        x x_1 :
      (↑A : Type u))
    ((ModuleCat.Hom.hom
            (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
              HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1) ≫
                Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A))) :
          (a : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
        x x_1 :
      (↑A : Type u))

Tactic:
simp [d_hom_apply, map_add, barComplex.d_single (k := k), homEquiv]

Premises used: Rep.homEquiv, map_add, inhomogeneousCochains.d_hom_apply, Rep.barComplex.d_single
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
rw :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u)))
      (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)))
      (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1) (n + 1 + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A))))
    0
⊢ d A n ≫ d A (n + 1) = 0

Tactic:
rw [d_eq, d_eq]

Premises used: inhomogeneousCochains.d_eq
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
a : 𝟙 (HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1))
| Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)) ≫
    Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A))

Tactic:
rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
slice_lhs :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
      CategoryStruct.comp (Y := HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1))
        (HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1))
        ((𝟙 (HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1)) ≫
            HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1) (n + 1 + 1)) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A))))
    0
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin n → G) → (↑A : Type u)))
      (ModuleCat.of k ((Fin (n + 1 + 1) → G) → (↑A : Type u))))
    (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u)))
      (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin n → G) A)) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)))
      (Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1) (n + 1 + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A))))
    0

Tactic:
slice_lhs 3 4 => rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
a : 0
| (CategoryStruct.comp (Y := HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1))
      (HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) n (n + 1))
      (𝟙 (HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1)) ≫
        HomologicalComplex.d (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1) (n + 1 + 1)) :
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k (free k G (Fin n → G) ⟶ A))
      (HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1 + 1)))

Tactic:
rw [Category.id_comp, ((barComplex k G).linearYonedaObj k A).d_comp_d]

Premises used: ChainComplex.linearYonedaObj, Rep.barComplex, HomologicalComplex.d_comp_d, CategoryTheory.Category.id_comp