awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
h : QuasiIso (C := ModuleCat k) (K := forget₂ToModuleCat k G) (HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G))
⊢ QuasiIso (K :=
    Functor.obj
      (Functor.mapHomologicalComplex
        (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))
        (ComplexShape.down ℕ))
      (standardComplex k G))
    (CategoryTheory.Functor.map
      (Functor.mapHomologicalComplex
        (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))
        (ComplexShape.down ℕ))
      (εToSingle₀ k G))
have h₁ : QuasiIso (K := forget₂ToModuleCat k G) (L :=
  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)))
  (CategoryTheory.Functor.map
      (Functor.mapHomologicalComplex
        (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))
        (ComplexShape.down ℕ))
      (εToSingle₀ k G) ≫
    NatTrans.app
      (Iso.hom
        (HomologicalComplex.singleMapHomologicalComplex
          (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))
          (ComplexShape.down ℕ) 0))
      (trivial k G k))
Tactic: rw [← εToSingle₀_comp_eq k G] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
⊢ QuasiIso (C := Rep k G) (εToSingle₀ k G)
have rw : QuasiIso (K :=
  Functor.obj
    (Functor.mapHomologicalComplex
      (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))
      (ComplexShape.down ℕ))
    (standardComplex k G))
  (CategoryTheory.Functor.map
    (Functor.mapHomologicalComplex
      (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))
      (ComplexShape.down ℕ))
    (εToSingle₀ k G))
Tactic: rw [← HomologicalComplex.quasiIso_map_iff_of_preservesHomology _ (forget₂ _ (ModuleCat.{u} k))]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
i : Fin (n + 1) → G
⊢ Eq (α := ((i : Fin (n + 1)) → G) →₀ k)
    (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
    (single (Fin.partialProd i ∘ Fin.succ) 1)
have e_a : HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ) =
  Fin.partialProd i ∘ Fin.succ
Tactic: congr
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (hypothesis)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
i : Fin (n + 1) → G
⊢ Eq (α := (↑(diagonal k G (n + 1)) : Type u))
    ((Hom.hom (d k G n ≫ Iso.inv (diagonalSuccIsoFree k G n)) :
          (a : (↑(free k G (Fin (n + 1) → G)) : Type u)) → (↑(diagonal k G (n + 1)) : Type u))
        (single i (single 1 1)) :
      (↑(diagonal k G (n + 1)) : Type u))
    ((Hom.hom (Iso.inv (diagonalSuccIsoFree k G (n + 1)) ≫ HomologicalComplex.d (standardComplex k G) (n + 1) n) :
          (a : (↑(free k G (Fin (n + 1) → G)) : Type u)) → (↑(diagonal k G (n + 1)) : Type u))
        (single i (single 1 1)) :
      (↑(diagonal k G (n + 1)) : Type u))
have eq3 : Eq (α := ((i : Fin (n + 1)) → G) →₀ k)
  (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
  (single (Fin.partialProd i ∘ Fin.succ) 1)
Tactic: have eq3 : single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) (1 : k) =
      single (Fin.partialProd i ∘ Fin.succ) 1 := by
      congr; exact funext fun j ↦ Fin.partialProd_succ' i j |>.symm
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
i : Fin (n + 1) → G
eq3 :
  Eq (α := ((i : Fin (n + 1)) → G) →₀ k)
    (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
    (single (Fin.partialProd i ∘ Fin.succ) 1)
⊢ Eq (α := (↑(diagonal k G (n + 1)) : Type u))
    ((Hom.hom (d k G n ≫ Iso.inv (diagonalSuccIsoFree k G n)) :
          (a : (↑(free k G (Fin (n + 1) → G)) : Type u)) → (↑(diagonal k G (n + 1)) : Type u))
        (single i (single 1 1)) :
      (↑(diagonal k G (n + 1)) : Type u))
    ((Hom.hom (Iso.inv (diagonalSuccIsoFree k G (n + 1)) ≫ HomologicalComplex.d (standardComplex k G) (n + 1) n) :
          (a : (↑(free k G (Fin (n + 1) → G)) : Type u)) → (↑(diagonal k G (n + 1)) : Type u))
        (single i (single 1 1)) :
      (↑(diagonal k G (n + 1)) : Type u))
have simp : HAdd.hAdd (α := (Fin (n + 1) → G) →₀ k)
    (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
    (∑ x : Fin (n + 1),
      single (Fin.partialProd (x.contractNth (fun (x1 x2 : G) ↦ x1 * x2) i)) (HPow.hPow (α := k) (-1) ((↑x : ℕ) + 1))) =
  (standardComplex.d k G (n + 1) : (a : (Fin (n + 1 + 1) → G) →₀ k) → (Fin (n + 1) → G) →₀ k)
    (single (Fin.partialProd i) 1)
Tactic: simp [μ_hom, d_single (k := k),
      Representation.linearizeOfMulActionIso_symm_apply,
      Representation.linearizeTrivialIso_symm_apply _, d_apply (k := k),
      Representation.μ_apply_single_single_leftRegular _,
      Representation.linearizeMap_single_diagonal _]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
⊢ Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
have rw : Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
  (barComplex.d k G (m + 1) ≫ barComplex.d k G m ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
Tactic: rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
rw :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫ barComplex.d k G m ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
⊢ Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
have rw₁ : Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
  (barComplex.d k G (m + 1) ≫
    Iso.inv (diagonalSuccIsoFree k G (m + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1) m)
  0
Tactic: rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
rw :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫ barComplex.d k G m ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
rw₁ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫
      Iso.inv (diagonalSuccIsoFree k G (m + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
⊢ Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
have rw₂ : Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
  ((barComplex.d k G (m + 1) ≫ Iso.inv (diagonalSuccIsoFree k G (m + 1))) ≫
    HomologicalComplex.d (standardComplex k G) (m + 1) m)
  0
Tactic: rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
rw :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫ barComplex.d k G m ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
rw₁ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫
      Iso.inv (diagonalSuccIsoFree k G (m + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
rw₂ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ Iso.inv (diagonalSuccIsoFree k G (m + 1))) ≫
      HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
⊢ Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
have rw₃ : Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
  (CategoryStruct.comp (Y := diagonal k G (m + 1 + 1))
      (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1 + 1) (m + 1))
      (HomologicalComplex.d (standardComplex k G) (m + 1) m) :
    Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
  (0 : Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
Tactic: rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
rw :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫ barComplex.d k G m ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
rw₁ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫
      Iso.inv (diagonalSuccIsoFree k G (m + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
rw₂ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ Iso.inv (diagonalSuccIsoFree k G (m + 1))) ≫
      HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
rw₃ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (CategoryStruct.comp (Y := diagonal k G (m + 1 + 1))
        (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1 + 1) (m + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1) m) :
      Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (0 : Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
⊢ Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
have rw₄ : Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
  (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫
    CategoryStruct.comp (Y := diagonal k G (m + 1 + 1)) (HomologicalComplex.d (standardComplex k G) (m + 1 + 1) (m + 1))
      (HomologicalComplex.d (standardComplex k G) (m + 1) m))
  0
Tactic: rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
rw :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫ barComplex.d k G m ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
rw₁ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫
      Iso.inv (diagonalSuccIsoFree k G (m + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
rw₂ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ Iso.inv (diagonalSuccIsoFree k G (m + 1))) ≫
      HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
rw₃ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (CategoryStruct.comp (Y := diagonal k G (m + 1 + 1))
        (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1 + 1) (m + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1) m) :
      Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (0 : Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
rw₄ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫
      CategoryStruct.comp (Y := diagonal k G (m + 1 + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1 + 1) (m + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1) m))
    0
⊢ Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
have rw₅ : Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
  (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫ 0) 0
Tactic: rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
rw :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫ barComplex.d k G m ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
rw₁ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫
      Iso.inv (diagonalSuccIsoFree k G (m + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
rw₂ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ Iso.inv (diagonalSuccIsoFree k G (m + 1))) ≫
      HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
rw₃ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (CategoryStruct.comp (Y := diagonal k G (m + 1 + 1))
        (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1 + 1) (m + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1) m) :
      Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (0 : Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
rw₄ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫
      CategoryStruct.comp (Y := diagonal k G (m + 1 + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1 + 1) (m + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1) m))
    0
rw₅ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫ 0) 0
⊢ Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
have rw₆ : Eq.{u + 1} (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1))) 0 0
Tactic: rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (hypothesis)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := Rep k G) ((fun (n : ℕ) ↦ (free k G (Fin n → G) : Rep k G)) (m + 1 + 1))
      ((fun (n : ℕ) ↦ (free k G (Fin n → G) : Rep k G)) m))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (free k G (Fin n → G) : Rep k G)) (m + 1))
      ((fun (n : ℕ) ↦
          (barComplex.d k G n : Quiver.Hom (V := Rep k G) (free k G (Fin (n + 1) → G)) (free k G (Fin n → G))))
        (m + 1))
      ((fun (n : ℕ) ↦
          (barComplex.d k G n : Quiver.Hom (V := Rep k G) (free k G (Fin (n + 1) → G)) (free k G (Fin n → G))))
        m))
    0
have key : Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
  ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
Tactic: have key : (d k G (m + 1) ≫ d k G m) ≫ (diagonalSuccIsoFree k G m).inv = 0 := by
      rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
j : ℕ
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          (j + 1)))
      (HomologicalComplex.d (standardComplex k G) (j + 1) j))
    (HomologicalComplex.d (barComplex k G) (j + 1) j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
have rw : Eq (α :=
  Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
    (HomologicalComplex.X (standardComplex k G) j))
  (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
    (Iso.hom
      ((fun (i : ℕ) ↦
          (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
        (j + 1)))
    (HomologicalComplex.d (standardComplex k G) (j + 1) j))
  (d k G j ≫
    Iso.hom
      ((fun (i : ℕ) ↦
          (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
        j))
Tactic: rw [d_def, Iso.symm_hom, Iso.symm_hom, d_comp_diagonalSuccIsoFree_inv_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
j : ℕ
rw :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          (j + 1)))
      (HomologicalComplex.d (standardComplex k G) (j + 1) j))
    (d k G j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          (j + 1)))
      (HomologicalComplex.d (standardComplex k G) (j + 1) j))
    (HomologicalComplex.d (barComplex k G) (j + 1) j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
have rw₁ : Eq (α :=
  Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
    (HomologicalComplex.X (standardComplex k G) j))
  (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
  (d k G j ≫
    Iso.hom
      ((fun (i : ℕ) ↦
          (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
        j))
Tactic: rw [d_def, Iso.symm_hom, Iso.symm_hom, d_comp_diagonalSuccIsoFree_inv_eq]