-- 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
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
⊢ 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₃ : ∀ (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
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