-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
inst_3 : DecidableEq G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
inst_4 : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
rw :
  HSub.hSub (α := (↑(groupHomology A i) : Type u)) (β := (↑(groupHomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
            x :
          (↑(groupHomology A i) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X := ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
            y :
          (↑(groupHomology A i) : Type u)) =
      0 ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈
      (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range
rw₁ :
  Eq (α := (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          (x - y) :
        (↑(groupHomology A i) : Type u))
      (0 : (↑(groupHomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈
      (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range
⊢ Eq (α := (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          x :
        (↑(groupHomology A i) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) (groupHomologyπEven A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(LinearMap.ker A.ρ.norm)) : Type u)) → (↑(groupHomology A i) : Type u))
          y :
        (↑(groupHomology A i) : Type u)) ↔
    (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈
      (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range
have rw₂ : (↑(x - y) : (↑A : Type u)) ∈
    (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range ↔
  (↑x : (↑A : Type u)) - (↑y : (↑A : Type u)) ∈
    (Hom.hom (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (A.applyAsHom (k := k) g : A ⟶ A) (𝟙 A))).range
Tactic: rw [← sub_eq_zero, ← map_sub, groupHomologyπEven_eq_zero_iff, AddSubgroupClass.coe_sub]