awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
h :
  Eq (α :=
    (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 1).homology)
    ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)
    (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso)
⊢ Eq (α := (↑(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 ↥(cocycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          x :
        (↑(H1 A) : Type u))
      (0 : (↑(H1 A) : Type u)) ↔
    (⇑x : (a : G) → (↑A : Type u)) ∈ coboundaries₁ A
have simp : Eq (α := (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
    ((ModuleCat.Hom.hom (shortComplexH1 A).moduleCatLeftHomologyData.π :
          (a : ↥(cocycles₁ A)) → (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
        x :
      (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
    (0 : (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u)) ↔
  (⇑x : (a : G) → (↑A : Type u)) ∈ coboundaries₁ A
Tactic: simp only [H1π, isoCocycles₁, π, 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)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cocycles₁ A)
⊢ Eq (α := (↑(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 ↥(cocycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          x :
        (↑(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 ↥(cocycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          y :
        (↑(H1 A) : Type u)) ↔
    HSub.hSub (α := (a : G) → (↑A : Type u)) (⇑x : (a : G) → (↑A : Type u)) (⇑y : (a : G) → (↑A : Type u)) ∈
      coboundaries₁ A
have rw : (⇑(x - y) : (a : G) → (↑A : Type u)) ∈ coboundaries₁ A ↔
  HSub.hSub (α := (a : G) → (↑A : Type u)) (⇑x : (a : G) → (↑A : Type u)) (⇑y : (a : G) → (↑A : Type u)) ∈
    coboundaries₁ A
Tactic: rw [← sub_eq_zero, ← map_sub, H1π_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ Eq (α := (inhomogeneousCochains A).X 0 ⟶ (inhomogeneousCochains A).X 1) ((inhomogeneousCochains A).d 0 1) 0
have hf : ∀ (i : Fin 0 → G) (x : (↑A : Type u)) (g : Fin 1 → G),
  Eq (α := (↑A : Type u))
    ((ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) i :
          (a : (↑A : Type u)) → (↑((inhomogeneousCochains A).X 1) : Type u))
        x g :
      (↑A : Type u))
    (((ModuleCat.Hom.hom 0 :
              (↑((inhomogeneousCochains A).X 0) : Type u) →ₗ[k] (↑((inhomogeneousCochains A).X 1) : Type u)) ∘ₗ
            LinearMap.single k (fun (i : Fin 0 → G) ↦ (↑A : Type u)) i :
          (a : (↑A : Type u)) → (↑((inhomogeneousCochains A).X 1) : Type u))
        x g :
      (↑A : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₂ 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 ↥(cocycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          x :
        (↑(H2 A) : Type u))
      (0 : (↑(H2 A) : Type u)) ↔
    (⇑x : (a : G × G) → (↑A : Type u)) ∈ coboundaries₂ A
have h : Eq (α := (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 2).homology)
  ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
    leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
      Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)
  (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
      (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
    (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData.π ≫
      Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)
Tactic: have h := leftHomologyπ_naturality'_assoc (isoShortComplexH2 A).inv
    (shortComplexH2 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousCochains A).sc 2).leftHomologyIso.hom
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₂ A)
h :
  Eq (α :=
    (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousCochains A) 2).homology)
    ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)
    (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso)
⊢ 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 ↥(cocycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          x :
        (↑(H2 A) : Type u))
      (0 : (↑(H2 A) : Type u)) ↔
    (⇑x : (a : G × G) → (↑A : Type u)) ∈ coboundaries₂ A
have simp : Eq (α := (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
    ((ModuleCat.Hom.hom (shortComplexH2 A).moduleCatLeftHomologyData.π :
          (a : ↥(cocycles₂ A)) → (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
        x :
      (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
    (0 : (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u)) ↔
  (⇑x : (a : G × G) → (↑A : Type u)) ∈ coboundaries₂ A
Tactic: simp only [H2π, isoCocycles₂, π, 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)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cocycles₂ 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 ↥(cocycles₂ 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 ↥(cocycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          y :
        (↑(H2 A) : Type u)) ↔
    HSub.hSub (α := (a : G × G) → (↑A : Type u)) (⇑x : (a : G × G) → (↑A : Type u)) (⇑y : (a : G × G) → (↑A : Type u)) ∈
      coboundaries₂ A
have rw : (⇑(x - y) : (a : G × G) → (↑A : Type u)) ∈ coboundaries₂ A ↔
  HSub.hSub (α := (a : G × G) → (↑A : Type u)) (⇑x : (a : G × G) → (↑A : Type u)) (⇑y : (a : G × G) → (↑A : Type u)) ∈
    coboundaries₂ A
Tactic: rw [← sub_eq_zero, ← map_sub, H2π_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
inst_2 : DecidableEq G
⊢ d A n =
    Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
        Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))
have hf : ∀ (a : Fin (n + 1) → G) (x : (↑A : Type u)),
  Eq (α := (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom (d A n) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom
              (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
                (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
                  Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))) ∘ₗ
            lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))) : Type u))
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
⊢ inhomogeneousChains.d A (n + 1) ≫ inhomogeneousChains.d A n = 0
have rw : Eq (α :=
  Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
    (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
  (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) →₀ (↑A : Type u)))
    (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
        Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))))
    (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
        Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))))
  0
Tactic: rw [inhomogeneousChains.d_eq, inhomogeneousChains.d_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
| Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
    Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)))
have a : 𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1))
Tactic: rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
      (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
    (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) →₀ (↑A : Type u)))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))))
    0
have slice_lhs : Eq (α :=
  Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
    (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
  (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
    (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
      (𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1)) ≫
          (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n) ≫
        Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G))))
  0
Tactic: slice_lhs 3 4 => rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
| (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
    𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1)) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n
have a : 0
Tactic: rw [Category.id_comp, ((barComplex k G).coinvariantsTensorObj A).d_comp_d]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
      (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
        (𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1)) ≫
            (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n) ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G))))
    0
have slice_lhs : Eq (α :=
  Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
    (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
  (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
    0 ≫ Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G))))
  0
Tactic: slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).coinvariantsTensorObj A).d_comp_d]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
simp : inhomogeneousChains.d A (n + 1) ≫ inhomogeneousChains.d A n = 0
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := ModuleCat k)
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) (n + 1 + 1))
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) n))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) (n + 1))
      ((fun (n : ℕ) ↦ inhomogeneousChains.d A n) (n + 1)) ((fun (n : ℕ) ↦ inhomogeneousChains.d A n) n))
    0
have simp₁ : Eq (α :=
  Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
    (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
  (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) →₀ (↑A : Type u)))
    (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
        Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))))
    (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
        Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))))
  0
Tactic: classical
    simp only
    rw [inhomogeneousChains.d_eq, inhomogeneousChains.d_eq]
    slice_lhs 3 4 => rw [Iso.hom_inv_id]
    slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).coinvariantsTensorObj A).d_comp_d]
    simp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
simp : inhomogeneousChains.d A (n + 1) ≫ inhomogeneousChains.d A n = 0
simp₁ :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
      (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
    (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) →₀ (↑A : Type u)))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))))
    0
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := ModuleCat k)
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) (n + 1 + 1))
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) n))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) (n + 1))
      ((fun (n : ℕ) ↦ inhomogeneousChains.d A n) (n + 1)) ((fun (n : ℕ) ↦ inhomogeneousChains.d A n) n))
    0
have simp₂ : Eq (α :=
  Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
    (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
  (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
    (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
      (𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1)) ≫
          (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n) ≫
        Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G))))
  0
Tactic: classical
    simp only
    rw [inhomogeneousChains.d_eq, inhomogeneousChains.d_eq]
    slice_lhs 3 4 => rw [Iso.hom_inv_id]
    slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).coinvariantsTensorObj A).d_comp_d]
    simp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n_1 n : ℕ
simp : inhomogeneousChains.d A (n + 1) ≫ inhomogeneousChains.d A n = 0
simp₁ :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
      (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
    (CategoryStruct.comp (Y := ModuleCat.of k ((Fin (n + 1) → G) →₀ (↑A : Type u)))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))))
      (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G)))))
    0
simp₂ :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
      (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
    (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
        (𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1)) ≫
            (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n) ≫
          Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G))))
    0
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := ModuleCat k)
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) (n + 1 + 1))
      ((fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) n))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u)) : ModuleCat k)) (n + 1))
      ((fun (n : ℕ) ↦ inhomogeneousChains.d A n) (n + 1)) ((fun (n : ℕ) ↦ inhomogeneousChains.d A n) n))
    0
have simp₃ : Eq (α :=
  Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ((Fin (n + 1 + 1) → G) →₀ (↑A : Type u)))
    (ModuleCat.of k ((Fin n → G) →₀ (↑A : Type u))))
  (Iso.inv (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G))) ≫
    0 ≫ Iso.hom (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin n → G))))
  0
Tactic: classical
    simp only
    rw [inhomogeneousChains.d_eq, inhomogeneousChains.d_eq]
    slice_lhs 3 4 => rw [Iso.hom_inv_id]
    slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).coinvariantsTensorObj A).d_comp_d]
    simp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n : ℕ
inst_4 : DecidableEq G
⊢ inhomogeneousChains A ≅ HomologicalComplex.coinvariantsTensorObj A (barComplex k G)
have refine_1 : (i : ℕ) → (inhomogeneousChains A).X i ≅ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X i
Tactic: refine HomologicalComplex.Hom.isoOfComponents ?_ ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (goal)
Goal:
k_1 G_1 : Type u
inst : CommRing k_1
inst_1 : Group G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Group G
A : Rep k G
n : ℕ
inst_4 : DecidableEq G
refine_1 : (i : ℕ) → (inhomogeneousChains A).X i ≅ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X i
⊢ inhomogeneousChains A ≅ HomologicalComplex.coinvariantsTensorObj A (barComplex k G)
have refine_2 : ∀ (i j : ℕ),
  (ComplexShape.down ℕ).Rel i j →
    Iso.hom (Iso.symm (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin i → G)))) ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d i j =
      (inhomogeneousChains A).d i j ≫
        Iso.hom (Iso.symm (LinearEquiv.toModuleIso (A.coinvariantsTensorFreeLEquiv (Fin j → G))))
Tactic: refine HomologicalComplex.Hom.isoOfComponents ?_ ?_