awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
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
⊢ 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)))
have 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))))))
Tactic: rw [ShortComplex.moduleCat_exact_iff_range_eq_ker]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
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
⊢ 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))))))
have pos : ∀ (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: by_cases hm : Odd (m + 1)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
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 : ℕ
⊢ QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
have zero : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) 0
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
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
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
⊢ QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
have 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)
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
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
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)
⊢ (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))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ 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))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ d A n ≫ d A (n + 1) = 0
have 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
Tactic: rw [d_eq, d_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
| Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A)) ≫
    Iso.inv (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1) → G) A))
have a : 𝟙 (HomologicalComplex.X (ChainComplex.linearYonedaObj (barComplex k G) k A) (n + 1))
Tactic: rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ 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
have 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
Tactic: slice_lhs 3 4 => rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
| (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)))
have a : 0
Tactic: rw [Category.id_comp, ((barComplex k G).linearYonedaObj k A).d_comp_d]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
⊢ 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
have 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)) ≫
    0 ≫ Iso.hom (LinearEquiv.toModuleIso (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A)))
  0
Tactic: slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).linearYonedaObj k A).d_comp_d]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
simp : d A n ≫ d A (n + 1) = 0
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := ModuleCat k) ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) n)
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) (n + 1 + 1)))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) (n + 1))
      ((fun (n : ℕ) ↦ d A n) n) ((fun (n : ℕ) ↦ d A n) (n + 1)))
    0
have simp₁ : 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: classical
    simp only
    rw [d_eq, d_eq]
    slice_lhs 3 4 => rw [Iso.hom_inv_id]
    slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).linearYonedaObj k A).d_comp_d]
    simp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Group G
A : Rep k G
n : ℕ
simp : d A n ≫ d A (n + 1) = 0
simp₁ :
  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
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := ModuleCat k) ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) n)
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) (n + 1 + 1)))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) → (↑A : Type u)) : ModuleCat k)) (n + 1))
      ((fun (n : ℕ) ↦ d A n) n) ((fun (n : ℕ) ↦ d A n) (n + 1)))
    0
have simp₂ : 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
Tactic: classical
    simp only
    rw [d_eq, d_eq]
    slice_lhs 3 4 => rw [Iso.hom_inv_id]
    slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).linearYonedaObj k A).d_comp_d]
    simp