-- 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
h : H
a : (↑A : Type u)
b : (↑B : Type u)
⊢ Eq (α := (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
    ((((((TensorProduct.AlgebraTensorModule.curry
                          (((ind φ A).coinvariantsTensorMk B).compr₂
                              (ModuleCat.Hom.hom (coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B)) ∘ₗ
                            Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                        lsingle h :
                      k →ₗ[k]
                        (↑A : Type u) →ₗ[k]
                          (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
                    (a : k) →
                      (↑A : Type u) →ₗ[k]
                        (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
                  1 :
                (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
              a :
            (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
          (a : (↑B : Type u)) → (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
        b :
      (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
    ((((((TensorProduct.AlgebraTensorModule.curry
                          (((ind φ A).coinvariantsTensorMk B).compr₂
                              (ModuleCat.Hom.hom (𝟙 ((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B))) ∘ₗ
                            Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                        lsingle h :
                      k →ₗ[k]
                        (↑A : Type u) →ₗ[k]
                          (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
                    (a : k) →
                      (↑A : Type u) →ₗ[k]
                        (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
                  1 :
                (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
              a :
            (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
          (a : (↑B : Type u)) → (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
        b :
      (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))

Tactic:
simpa [coinvariantsTensorIndInv, coinvariantsTensorMk,
      coinvariantsTensorIndHom, Coinvariants.mk_eq_iff] using
        Coinvariants.mem_ker_of_eq h (IndV.mk φ _ h a ⊗ₜ[k] b) _ <| by simp

Premises used: Representation.IndV.mk, Rep.coinvariantsTensorIndInv, Representation.Coinvariants.mk_eq_iff, Representation.Coinvariants.mem_ker_of_eq, TensorProduct.tmul, Rep.coinvariantsTensorMk, DFunLike.coe, Rep.coinvariantsTensorIndHom