-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
X Y : Rep k H
f : X ⟶ Y
hfg :
  ∀ (a : H) (x : (↑A : Type u)) (x_1 : (↑X : Type u)),
    Eq (α := (↑((resFunctor φ ⋙ Functor.obj (coinvariantsTensor k G) A).obj Y) : Type u))
      ((((((TensorProduct.AlgebraTensorModule.curry
                            (((ind φ A).coinvariantsTensorMk X).compr₂
                                (ModuleCat.Hom.hom
                                  ((Functor.obj (coinvariantsTensor k H) (ind φ A)).map f ≫
                                    Iso.hom ((fun (B : Rep k H) ↦ coinvariantsTensorIndIso φ A B) Y))) ∘ₗ
                              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                          lsingle a :
                        k →ₗ[k]
                          (↑A : Type u) →ₗ[k]
                            (↑X : Type u) →ₗ[k]
                              (↑((resFunctor φ ⋙ Functor.obj (coinvariantsTensor k G) A).obj Y) : Type u)) :
                      (a : k) →
                        (↑A : Type u) →ₗ[k]
                          (↑X : Type u) →ₗ[k] (↑((resFunctor φ ⋙ (coinvariantsTensor k G).obj A).obj Y) : Type u))
                    1 :
                  (a : (↑A : Type u)) →
                    (↑X : Type u) →ₗ[k] (↑((resFunctor φ ⋙ (coinvariantsTensor k G).obj A).obj Y) : Type u))
                x :
              (↑X : Type u) →ₗ[k] (↑((resFunctor φ ⋙ Functor.obj (coinvariantsTensor k G) A).obj Y) : Type u)) :
            (a : (↑X : Type u)) → (↑((resFunctor φ ⋙ (coinvariantsTensor k G).obj A).obj Y) : Type u))
          x_1 :
        (↑((resFunctor φ ⋙ Functor.obj (coinvariantsTensor k G) A).obj Y) : Type u))
      ((((((TensorProduct.AlgebraTensorModule.curry
                            (((ind φ A).coinvariantsTensorMk X).compr₂
                                (ModuleCat.Hom.hom
                                  (Iso.hom ((fun (B : Rep k H) ↦ coinvariantsTensorIndIso φ A B) X) ≫
                                    (resFunctor φ ⋙ Functor.obj (coinvariantsTensor k G) A).map f)) ∘ₗ
                              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                          lsingle a :
                        k →ₗ[k]
                          (↑A : Type u) →ₗ[k]
                            (↑X : Type u) →ₗ[k]
                              (↑((resFunctor φ ⋙ Functor.obj (coinvariantsTensor k G) A).obj Y) : Type u)) :
                      (a : k) →
                        (↑A : Type u) →ₗ[k]
                          (↑X : Type u) →ₗ[k] (↑((resFunctor φ ⋙ (coinvariantsTensor k G).obj A).obj Y) : Type u))
                    1 :
                  (a : (↑A : Type u)) →
                    (↑X : Type u) →ₗ[k] (↑((resFunctor φ ⋙ (coinvariantsTensor k G).obj A).obj Y) : Type u))
                x :
              (↑X : Type u) →ₗ[k] (↑((resFunctor φ ⋙ Functor.obj (coinvariantsTensor k G) A).obj Y) : Type u)) :
            (a : (↑X : Type u)) → (↑((resFunctor φ ⋙ (coinvariantsTensor k G).obj A).obj Y) : Type u))
          x_1 :
        (↑((resFunctor φ ⋙ Functor.obj (coinvariantsTensor k G) A).obj Y) : Type u))
⊢ (Functor.obj (coinvariantsTensor k H) (ind φ A)).map f ≫
      Iso.hom ((fun (B : Rep k H) ↦ coinvariantsTensorIndIso φ A B) Y) =
    Iso.hom ((fun (B : Rep k H) ↦ coinvariantsTensorIndIso φ A B) X) ≫
      (resFunctor φ ⋙ Functor.obj (coinvariantsTensor k G) A).map f

Tactic:
ext