-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
inst_3 : S.FiniteIndex
X Y : Rep.{max u w, u, v} k ↥S
f : X ⟶ Y
⊢ Eq (α := ind S.subtype X ⟶ coind.{u, v, v, max u w} S.subtype Y)
    (CategoryTheory.Functor.map (indFunctor k S.subtype) f ≫ (indCoindIso.{w, u, v} Y).hom :
      ind S.subtype X ⟶ coind.{u, v, v, max u w} S.subtype Y)
    ((indCoindIso.{w, u, v} X).hom ≫ CategoryTheory.Functor.map (coindFunctor k S.subtype) f :
      ind S.subtype X ⟶ coind.{u, v, v, max u w} S.subtype Y)
have hf : ∀ (g1 : G) (x : (↑X : Type (max u w))) (g2 : G),
  Eq (α := (↑Y : Type (max u w)))
    ((↑((((AlgebraTensorModule.curry
                        ((IntertwiningMap.toLinearMap (G := G) (ρ := (ind S.subtype X).ρ) (σ :=
                              (coind.{u, v, v, max u w} S.subtype Y).ρ)
                              (Hom.hom
                                (CategoryTheory.Functor.map (indFunctor k S.subtype) f ≫
                                  (indCoindIso.{w, u, v} Y).hom)) :
                            (↑(ind S.subtype X) : Type (max (max u v) w)) →ₗ[k]
                              (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w))) ∘ₗ
                          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X.ρ) :
                            (G →₀ k) ⊗[k] (↑X : Type (max u w)) →ₗ[k]
                              (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X.ρ).Coinvariants (k :=
                                k) (G := ↥S) (V := (G →₀ k) ⊗[k] (↑X : Type (max u w))))) ∘ₗ
                      lsingle g1 :
                    k →ₗ[k]
                      (↑X : Type (max u w)) →ₗ[k] (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w))) :
                  (a : k) →
                    (↑X : Type (max u w)) →ₗ[k] (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w)))
                1 :
              (a : (↑X : Type (max u w))) → (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w)))
            x) :
        G → (↑Y : Type (max u w)))
      g2)
    ((↑((((AlgebraTensorModule.curry
                        (IntertwiningMap.toLinearMap
                            (Hom.hom
                              ((indCoindIso.{w, u, v} X).hom ≫
                                CategoryTheory.Functor.map (coindFunctor k S.subtype) f)) ∘ₗ
                          Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X.ρ)) ∘ₗ
                      lsingle g1 :
                    k →ₗ[k]
                      (↑X : Type (max u w)) →ₗ[k] (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w))) :
                  (a : k) →
                    (↑X : Type (max u w)) →ₗ[k] (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w)))
                1 :
              (a : (↑X : Type (max u w))) → (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w)))
            x) :
        G → (↑Y : Type (max u w)))
      g2)
Tactic: ext g1 x g2