-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
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
⊢ (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
have 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))
Tactic: ext