-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
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
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
h₃ :
  ∀ (a : G) (b : (↑A : Type u)) (f : G →₀ (↑A : Type u)),
    a ∉ f.support →
      b ≠ 0 →
        ∀
          (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))
                    f =
                  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)
          ⦃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))
                (single a b + f) =
              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
⊢ 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)

Premises used: Finsupp.single_add, add_sub_add_comm, Finsupp.sum_add_index, groupHomology.d₁₀_single