-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
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)
⊢ 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)

Tactic:
ext g1 x g2