awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
this : Mono X.f := ⋯
i : ℕ
⊢ Exact (ShortComplex.map (X.map (chainsFunctor k G)) (HomologicalComplex.eval (ModuleCat k) (ComplexShape.down ℕ) i))
have this₁ : (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker
Tactic: have : LinearMap.range X.f.hom.toLinearMap = LinearMap.ker X.g.hom.toLinearMap :=
        (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G →₀ (↑X.X₂ : Type u)) → G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G →₀ (↑X.X₃ : Type u))
x : (↑X.X₁ : Type u)
hx :
  Eq (α := (↑X.X₂ : Type u)) ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) x : (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₁₀ X.X₂) :
          (a : (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u)) → (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
        y :
      (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains X.X₃).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousChains X.X₃).X 1) (Y := (inhomogeneousChains X.X₃).X 0)
            ((inhomogeneousChains X.X₃).d 1 0) :
          (a : (↑((inhomogeneousChains X.X₃).X 1) : Type u)) → (↑((inhomogeneousChains X.X₃).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (chainsIso₁ X.X₃).inv :
            (a : (↑(ModuleCat.of k (G →₀ (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₃).X 1) : Type u))
          (↑z : G →₀ (↑X.X₃ : Type u))) :
      (↑((inhomogeneousChains X.X₃).X 0) : Type u))
    (0 : (↑((inhomogeneousChains X.X₃).X 0) : Type u))
have rw : Eq (α := (↑((inhomogeneousChains X.X₃).X 0) : Type u))
  ((ModuleCat.Hom.hom (d₁₀ X.X₃ ≫ (chainsIso₀ X.X₃).inv) :
        (a : (↑(ModuleCat.of k (G →₀ (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₃).X 0) : Type u))
      (↑z : G →₀ (↑X.X₃ : Type u)) :
    (↑((inhomogeneousChains X.X₃).X 0) : Type u))
  (0 : (↑((inhomogeneousChains X.X₃).X 0) : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G →₀ (↑X.X₂ : Type u)) → G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G →₀ (↑X.X₃ : Type u))
x : (↑X.X₁ : Type u)
hx :
  Eq (α := (↑X.X₂ : Type u)) ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) x : (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₁₀ X.X₂) :
          (a : (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u)) → (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
        y :
      (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u))
x_1 : Fin 0 → G
| ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := (inhomogeneousChains X.X₂).X 1) (Y := (inhomogeneousChains X.X₂).X 0)
                ((inhomogeneousChains X.X₂).d 1 0) :
              (a : (↑((inhomogeneousChains X.X₂).X 1) : Type u)) → (↑((inhomogeneousChains X.X₂).X 0) : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (chainsIso₁ X.X₂).inv :
                (a : (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u)) →
                  (↑((inhomogeneousChains X.X₂).X 1) : Type u))
              y) :
          (↑((inhomogeneousChains X.X₂).X 0) : Type u)) :
        (a : Fin 0 → G) → (↑X.X₂ : Type u))
      x_1 :
    (↑X.X₂ : Type u))
have rw : ((((ModuleCat.Hom.hom (d₁₀ X.X₂ ≫ (chainsIso₀ X.X₂).inv) :
            (a : (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₂).X 0) : Type u))
          y :
        (↑((inhomogeneousChains X.X₂).X 0) : Type u)) :
      (a : Fin 0 → G) → (↑X.X₂ : Type u))
    x_1 :
  (↑X.X₂ : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : G × G →₀ (↑X.X₂ : Type u)
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : Type u)) x :
      G →₀ (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
⊢ Eq (α := (↑X.X₂ : Type u))
    ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u))
        ((ModuleCat.Hom.hom (d₁₀ X.X₁) : (a : G →₀ (↑X.X₁ : Type u)) → (↑(ModuleCat.of k (↑X.X₁ : Type u)) : Type u))
            x :
          (↑(ModuleCat.of k (↑X.X₁ : Type u)) : Type u)) :
      (↑X.X₂ : Type u))
    ((Rep.Hom.hom X.f : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) 0 : (↑X.X₂ : Type u))
have this : Eq (α := (↑(X₃ (shortComplexH1 (G := G) X.2)) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (Y := X₃ (shortComplexH1 (G := G) X.2))
          ((shortComplexH1 X.X₁).g ≫ Hom.τ₃ (mapShortComplexH1 (MonoidHom.id G) X.f)) :
        (a : (↑(shortComplexH1 X.X₁).X₂ : Type u)) → (↑(shortComplexH1 X.2).X₃ : Type u))
      x :
    (↑(X₃ (shortComplexH1 (G := G) X.2)) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := (shortComplexH1 X.X₁).X₂) (Y := X₃ (shortComplexH1 (G := G) X.2))
          (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) X.f) ≫ g (shortComplexH1 (G := G) X.2)) :
        (a : (↑(shortComplexH1 X.X₁).X₂ : Type u)) → (↑(shortComplexH1 X.2).X₃ : Type u))
      x :
    (↑(X₃ (shortComplexH1 (G := G) X.2)) : Type u))
Tactic: have := congr($((mapShortComplexH1 (MonoidHom.id G) X.f).comm₂₃.symm) x)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G × G →₀ (↑X.X₂ : Type u)) → G × G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G × G →₀ (↑X.X₃ : Type u))
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : Type u)) x :
      G →₀ (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
⊢ Eq (α := (↑((inhomogeneousChains X.X₃).X 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousChains X.X₃).X 2) (Y := (inhomogeneousChains X.X₃).X 1)
            ((inhomogeneousChains X.X₃).d 2 1) :
          (a : (↑((inhomogeneousChains X.X₃).X 2) : Type u)) → (↑((inhomogeneousChains X.X₃).X 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (chainsIso₂ X.X₃).inv :
            (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₃ : Type u))) : Type u)) →
              (↑((inhomogeneousChains X.X₃).X 2) : Type u))
          (↑z : G × G →₀ (↑X.X₃ : Type u))) :
      (↑((inhomogeneousChains X.X₃).X 1) : Type u))
    (0 : (↑((inhomogeneousChains X.X₃).X 1) : Type u))
have rw : Eq (α := (↑((inhomogeneousChains X.X₃).X 1) : Type u))
  ((ModuleCat.Hom.hom (d₂₁ X.X₃ ≫ (chainsIso₁ X.X₃).inv) :
        (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousChains X.X₃).X 1) : Type u))
      (↑z : G × G →₀ (↑X.X₃ : Type u)) :
    (↑((inhomogeneousChains X.X₃).X 1) : Type u))
  (0 : (↑((inhomogeneousChains X.X₃).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.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G × G →₀ (↑X.X₂ : Type u)) → G × G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G × G →₀ (↑X.X₃ : Type u))
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : Type u)) x :
      G →₀ (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
x_1 : Fin 1 → G
| ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := (inhomogeneousChains X.X₂).X 2) (Y := (inhomogeneousChains X.X₂).X 1)
                ((inhomogeneousChains X.X₂).d 2 1) :
              (a : (↑((inhomogeneousChains X.X₂).X 2) : Type u)) → (↑((inhomogeneousChains X.X₂).X 1) : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (chainsIso₂ X.X₂).inv :
                (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
                  (↑((inhomogeneousChains X.X₂).X 2) : Type u))
              y) :
          (↑((inhomogeneousChains X.X₂).X 1) : Type u)) :
        (a : Fin 1 → G) → (↑X.X₂ : Type u))
      x_1 :
    (↑X.X₂ : Type u))
have rw : ((((ModuleCat.Hom.hom (d₂₁ X.X₂ ≫ (chainsIso₁ X.X₂).inv) :
            (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
              (↑((inhomogeneousChains X.X₂).X 1) : Type u))
          y :
        (↑((inhomogeneousChains X.X₂).X 1) : Type u)) :
      (a : Fin 1 → G) → (↑X.X₂ : Type u))
    x_1 :
  (↑X.X₂ : 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
⊢ (ModuleCat.Hom.hom (d₁₀ A)).range = Coinvariants.ker A.ρ
have symm : Coinvariants.ker A.ρ = (ModuleCat.Hom.hom (d₁₀ A)).range
Tactic: symm
-- 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
⊢ Coinvariants.ker A.ρ = (ModuleCat.Hom.hom (d₁₀ A)).range
have h₁ : (Set.range fun (gv : G × (↑A : Type u)) ↦
    HSub.hSub (α := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          gv.2 :
        (↑A : Type u))
      gv.2) ⊆
  (↑(ModuleCat.Hom.hom (d₁₀ A)).range : Set (↑A : Type u))
Tactic: apply Submodule.span_eq_of_le
-- 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
h₁ :
  (Set.range fun (gv : G × (↑A : Type u)) ↦
      HSub.hSub (α := (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            gv.2 :
          (↑A : Type u))
        gv.2) ⊆
    (↑(ModuleCat.Hom.hom (d₁₀ A)).range : Set (↑A : Type u))
⊢ Coinvariants.ker A.ρ = (ModuleCat.Hom.hom (d₁₀ A)).range
have h₂ : (ModuleCat.Hom.hom (d₁₀ A)).range ≤
  Submodule.span k
    (Set.range fun (gv : G × (↑A : Type u)) ↦
      HSub.hSub (α := (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            gv.2 :
          (↑A : Type u))
        gv.2)
Tactic: apply Submodule.span_eq_of_le
-- 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 : G × (↑A : Type u)
⊢ (fun (gv : G × (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              gv.2 :
            (↑A : Type u))
          gv.2)
      x ∈
    (↑(ModuleCat.Hom.hom (d₁₀ A)).range : Set (↑A : Type u))
have h : Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
  ((ModuleCat.Hom.hom (d₁₀ A) :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      (single x.1⁻¹ x.2) :
    (↑(ModuleCat.of k (↑A : Type u)) : Type u))
  ((fun (gv : G × (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              gv.2 :
            (↑A : Type u))
          gv.2)
      x :
    (↑A : Type u))
Tactic: use single x.1⁻¹ x.2
-- 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 : (↑A : Type u)
y : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)
hy :
  (ModuleCat.Hom.hom (d₁₀ A) :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      y =
    x
⊢ Membership.mem (γ := Submodule k (↑A : Type u))
    (Submodule.span k
      (Set.range fun (gv : G × (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              gv.2 :
            (↑A : Type u))
          gv.2))
    x
have h₂ : ∀ ⦃x : (↑A : Type u)⦄
  (hy :
    (ModuleCat.Hom.hom (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        0 =
      x),
  Membership.mem (γ := Submodule k (↑A : Type u))
    (Submodule.span k
      (Set.range fun (gv : G × (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) gv.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              gv.2 :
            (↑A : Type u))
          gv.2))
    x
Tactic: induction y using Finsupp.induction generalizing x with
    | zero => simp [← hy]
    | single_add _ _ _ _ _ h =>
      simpa [← hy, add_sub_add_comm, sum_add_index, d₁₀_single (G := G)]
        using Submodule.add_mem _ (Coinvariants.mem_ker_of_eq _ _ _ rfl) (h rfl)
Cleared hypotheses: x, y, hy
-- 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
⊢ d₁₀ A ≫ NatTrans.app (coinvariantsMk k G) A = 0
have hf : ∀ (a : G) (x : (↑A : Type u)),
  Eq (α := (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A ≫ NatTrans.app (coinvariantsMk k G) A) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑((coinvariantsFunctor k G).obj A) : Type u))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u))
    (((ModuleCat.Hom.hom 0 :
              (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →ₗ[k]
                (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u)) ∘ₗ
            lsingle a :
          (a : (↑A : Type u)) → (↑((coinvariantsFunctor k G).obj A) : Type u))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) A) : Type u))
Tactic: ext
-- 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 : (↑A : Type u)
hx : x ∈ Coinvariants.ker A.ρ
⊢ ∃ (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chains₁ToCoinvariantsKer A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ↥(Coinvariants.ker A.ρ)) : Type u))
        a =
      Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ Coinvariants.ker A.ρ) x hx
have rcases : ∀ (y : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
  (hy :
    (ModuleCat.Hom.hom (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        y =
      x),
  ∃ (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chains₁ToCoinvariantsKer A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ↥(Coinvariants.ker A.ρ)) : Type u))
        a =
      Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ Coinvariants.ker A.ρ) x hx
Tactic: rcases range_d₁₀_eq_coinvariantsKer A ▸ hx with ⟨y, hy⟩
-- 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 : (↑A : Type u)
hx : x ∈ Coinvariants.ker A.ρ
y : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)
hy :
  (ModuleCat.Hom.hom (d₁₀ A) :
        (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      y =
    x
w : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)
⊢ ∃ (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chains₁ToCoinvariantsKer A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ↥(Coinvariants.ker A.ρ)) : Type u))
        a =
      Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ Coinvariants.ker A.ρ) x hx
have h : (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC := ModuleCat.carrier)
        (chains₁ToCoinvariantsKer A) :
      (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(Coinvariants.ker A.ρ)) : Type u))
    y =
  Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ Coinvariants.ker A.ρ) x hx
Tactic: use y, Subtype.ext hy
-- 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
⊢ d₁₀ A = 0
have hf : ∀ (a : G) (x : (↑A : Type u)),
  Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A) ∘ₗ lsingle a : (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u)) x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    (((ModuleCat.Hom.hom 0 :
              (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →ₗ[k] (↑(ModuleCat.of k (↑A : Type u)) : Type u)) ∘ₗ
            lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
Tactic: ext
-- 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
g : G
a : (↑A : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₂₁ A) :
        (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
      (HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
        (single (g⁻¹, g)
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G × G →₀ (↑A : Type u))
        (single (g, g⁻¹) a)) =
    HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single 1 a)
      (single 1
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))
have simp : HAdd.hAdd (β := G →₀ (↑A : Type u))
      (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single g a)
        (single 1
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u)))
      (single g⁻¹
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u)) -
    (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
        (single g⁻¹
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u))
        (single 1 a) +
      single g a) =
  HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single 1 a)
    (single 1
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          a) :
      G →₀ (↑A : Type u))
Tactic: simp only [map_sub, d₂₁_single (G := G), inv_inv, self_inv_apply, inv_mul_cancel,
    mul_inv_cancel]