awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 1) (iCycles A 1) :
          (a : (↑(cycles A 1) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        (cyclesMk 1 0 cyclesMk₁_eq._proof_1
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (chainsIso₁ A).inv :
              (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
            (↑x : G →₀ (↑A : Type u)))
          ⋯) :
      (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 1) (iCycles A 1) :
          (a : (↑(cycles A 1) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₁ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(cycles A 1) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 1) : Type u))
have rw : Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (chainsIso₁ A).inv :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
      (↑x : G →₀ (↑A : Type u)) :
    (↑((inhomogeneousChains A).X 1) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := cycles A 1) (iCycles A 1) :
        (a : (↑(cycles A 1) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (isoCycles₁ A).inv :
          (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(cycles A 1) : Type u))
        x) :
    (↑((inhomogeneousChains A).X 1) : Type u))
Tactic: rw [iCycles_mk]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₁ A).inv :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        (↑x : G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 1) (iCycles A 1) :
          (a : (↑(cycles A 1) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₁ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(cycles A 1) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 1) : Type u))
have simp : Eq (α := (Fin 1 → G) →₀ (↑A : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (chainsIso₁ A).inv :
        (a : G →₀ (↑A : Type u)) → (Fin 1 → G) →₀ (↑A : Type u))
      (↑x : G →₀ (↑A : Type u)) :
    (Fin 1 → G) →₀ (↑A : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (chainsIso₁ A).inv) :
        (a : ↥(cycles₁ A)) → (Fin 1 → G) →₀ (↑A : Type u))
      x :
    (Fin 1 → G) →₀ (↑A : Type u))
Tactic: simp only [ChainComplex.of_X, isoCycles₁_inv_comp_iCycles_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousChains A).X 2) (Y := (inhomogeneousChains A).X 1)
            ((inhomogeneousChains A).d 2 1) :
          (a : (↑((inhomogeneousChains A).X 2) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (chainsIso₂ A).inv :
            (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
          (↑x : G × G →₀ (↑A : Type u))) :
      (↑((inhomogeneousChains A).X 1) : Type u))
    (0 : (↑((inhomogeneousChains A).X 1) : Type u))
have rw : Eq (α := (↑((inhomogeneousChains A).X 1) : Type u))
  ((ModuleCat.Hom.hom (d₂₁ A ≫ (chainsIso₁ A).inv) :
        (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 1) : Type u))
      (↑x : G × G →₀ (↑A : Type u)) :
    (↑((inhomogeneousChains A).X 1) : Type u))
  (0 : (↑((inhomogeneousChains A).X 1) : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ Eq (α := (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 2) (iCycles A 2) :
          (a : (↑(cycles A 2) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        (cyclesMk 2 1 cyclesMk₂_eq._proof_1
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (chainsIso₂ A).inv :
              (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
            (↑x : G × G →₀ (↑A : Type u)))
          ⋯) :
      (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 2) (iCycles A 2) :
          (a : (↑(cycles A 2) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₂ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(cycles A 2) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 2) : Type u))
have rw : Eq (α := (↑((inhomogeneousChains A).X 2) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (chainsIso₂ A).inv :
        (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
      (↑x : G × G →₀ (↑A : Type u)) :
    (↑((inhomogeneousChains A).X 2) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := cycles A 2) (iCycles A 2) :
        (a : (↑(cycles A 2) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (isoCycles₂ A).inv :
          (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(cycles A 2) : Type u))
        x) :
    (↑((inhomogeneousChains A).X 2) : Type u))
Tactic: rw [iCycles_mk]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ Eq (α := (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chainsIso₂ A).inv :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        (↑x : G × G →₀ (↑A : Type u)) :
      (↑((inhomogeneousChains A).X 2) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := cycles A 2) (iCycles A 2) :
          (a : (↑(cycles A 2) : Type u)) → (↑((inhomogeneousChains A).X 2) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (isoCycles₂ A).inv :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(cycles A 2) : Type u))
          x) :
      (↑((inhomogeneousChains A).X 2) : Type u))
have simp : Eq (α := (Fin 2 → G) →₀ (↑A : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (chainsIso₂ A).inv :
        (a : G × G →₀ (↑A : Type u)) → (Fin 2 → G) →₀ (↑A : Type u))
      (↑x : G × G →₀ (↑A : Type u)) :
    (Fin 2 → G) →₀ (↑A : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) ((shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (chainsIso₂ A).inv) :
        (a : ↥(cycles₂ A)) → (Fin 2 → G) →₀ (↑A : Type u))
      x :
    (Fin 2 → G) →₀ (↑A : Type u))
Tactic: simp only [ChainComplex.of_X, isoCycles₂_inv_comp_iCycles_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ Eq (α := (inhomogeneousChains A).X 1 ⟶ (inhomogeneousChains A).X 0) ((inhomogeneousChains A).d 1 0) 0
have h : ∀ (g : Fin 1 → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
  Eq (α := (↑A : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (inhomogeneousChains A).d 1 0) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
              x :
            (↑((inhomogeneousChains A).X 0) : Type u)) :
          (a : Fin 0 → G) → (↑A : Type u))
        default :
      (↑A : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ 0) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((inhomogeneousChains A).X 0) : Type u))
              x :
            (↑((inhomogeneousChains A).X 0) : Type u)) :
          (a : Fin 0 → G) → (↑A : Type u))
        default :
      (↑A : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ 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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          x :
        (↑(H1 A) : Type u))
      (0 : (↑(H1 A) : Type u)) ↔
    (↑x : G →₀ (↑A : Type u)) ∈ boundaries₁ A
have h : Eq (α := (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 1).homology)
  ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
    leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
      Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso)
  (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
      (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
    (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData.π ≫
      Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso)
Tactic: have h := leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv
    (shortComplexH1 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousChains A).sc 1).leftHomologyIso.hom
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₁ A)
h :
  Eq (α := (shortComplexH1 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 1).homology)
    ((shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso)
    (cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains 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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          x :
        (↑(H1 A) : Type u))
      (0 : (↑(H1 A) : Type u)) ↔
    (↑x : G →₀ (↑A : Type u)) ∈ boundaries₁ A
have simp : Eq (α := (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
    ((ModuleCat.Hom.hom (shortComplexH1 A).moduleCatLeftHomologyData.π :
          (a : ↥(cycles₁ A)) → (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
        x :
      (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
    (0 : (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u)) ↔
  (↑x : G →₀ (↑A : Type u)) ∈ boundaries₁ A
Tactic: simp only [H1π, isoCycles₁, π, 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.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cycles₁ 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 ↥(cycles₁ 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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          y :
        (↑(H1 A) : Type u)) ↔
    (↑x : G →₀ (↑A : Type u)) - (↑y : G →₀ (↑A : Type u)) ∈ boundaries₁ A
have rw : (↑(x - y) : G →₀ (↑A : Type u)) ∈ boundaries₁ A ↔ (↑x : G →₀ (↑A : Type u)) - (↑y : G →₀ (↑A : Type u)) ∈ boundaries₁ A
Tactic: rw [← sub_eq_zero, ← map_sub, H1π_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u))
        (H1ToTensorOfIsTrivial A ∘ₗ TensorProduct.lift (mkH1OfIsTrivial A))).toAddMonoidHom =
    LinearMap.toAddMonoidHom
      (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u)) LinearMap.id)
have h : ∀ (g : G) (a : (↑A : Type u)),
  Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((((Multiplicative.toAdd :
                (a : Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))) →
                  (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
              ((MonoidHom.comp
                    ((AddMonoidHom.toMultiplicativeRight :
                        (a :
                            Additive (Abelianization G) →+
                              (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) →
                          Abelianization G →*
                            Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                      (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u))
                          (H1ToTensorOfIsTrivial A ∘ₗ TensorProduct.lift (mkH1OfIsTrivial A))).toAddMonoidHom)
                    Abelianization.of :
                  (a : G) → Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                g) :
            (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
          (a : (↑A : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((((Multiplicative.toAdd :
                (a : Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))) →
                  (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
              ((MonoidHom.comp
                    ((AddMonoidHom.toMultiplicativeRight :
                        (a :
                            Additive (Abelianization G) →+
                              (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) →
                          Abelianization G →*
                            Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                      (LinearMap.toAddMonoidHom
                        (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u))
                          LinearMap.id)))
                    Abelianization.of :
                  (a : G) → Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                g) :
            (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
          (a : (↑A : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
Tactic: ext g a
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g : G
a : (↑A : Type u)
⊢ Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((H1AddEquivOfIsTrivial A : (a : (↑(H1 A) : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
                (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))
              (single g a) :
            (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))) :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
          ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
have rw : Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
  ((H1ToTensorOfIsTrivial A : (a : (↑(H1 A) : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
              (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))
            (single g a) :
          (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))) :
    Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
  ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
        ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
      a :
    Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
Tactic: rw [H1AddEquivOfIsTrivial_apply, H1ToTensorOfIsTrivial_H1π_single g a]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
g : G
a : (↑A : Type u)
rw :
  Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((H1ToTensorOfIsTrivial A : (a : (↑(H1 A) : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
                (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))
              (single g a) :
            (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))) :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
          ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
⊢ Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((H1AddEquivOfIsTrivial A : (a : (↑(H1 A) : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑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 ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
                (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))
              (single g a) :
            (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))) :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
          ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
have rw₁ : Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
  ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
        ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
      a :
    Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
  ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
        ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
      a :
    Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
Tactic: rw [H1AddEquivOfIsTrivial_apply, H1ToTensorOfIsTrivial_H1π_single g a]