-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
rw :
  HSub.hSub (α := (↑(groupCohomology A i) : Type u)) (β := (↑(groupCohomology 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 ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
            x :
          (↑(groupCohomology 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 ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
              (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
            y :
          (↑(groupCohomology 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 (α := (↑(groupCohomology 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 ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          (x - y) :
        (↑(groupCohomology A i) : Type u))
      (0 : (↑(groupCohomology 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
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
⊢ Eq (α := (↑(groupCohomology 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 ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          x :
        (↑(groupCohomology 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 ↥(Hom.hom A.norm).ker) (groupCohomologyπOdd A g hg i hi) :
            (a : (↑(ModuleCat.of k ↥(Hom.hom A.norm).ker) : Type u)) → (↑(groupCohomology A i) : Type u))
          y :
        (↑(groupCohomology 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 : (↑A : Type u)) - (↑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, groupCohomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]