-- 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 : H
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α :=
    (↑(Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k H)) (ind φ A)) B) : Type u) →ₗ[k]
      (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ.Coinvariants)
    (TensorProduct.lift
        (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
          (TensorProduct.lift
            ((lift
                  ((↑A : Type u) →ₗ[k]
                    (↑B : Type u) →ₗ[k]
                      (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ.Coinvariants)
                  k H :
                (a :
                    H →
                      (↑A : Type u) →ₗ[k]
                        (↑B : Type u) →ₗ[k]
                          (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants) →
                  (H →₀ k) →ₗ[k]
                    (↑A : Type u) →ₗ[k]
                      (↑B : Type u) →ₗ[k]
                        (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
              fun (g : H) ↦
              LinearMap.compl₂ (σ₄₂ := RingHom.id k) (A.coinvariantsTensorMk (res φ B))
                ((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g)))
          ⋯) ∘ₗ
      ((Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k H)) (ind φ A)) B).ρ :
          (a : H) →
            (↑(((MonoidalCategory.curriedTensor (Rep k H)).obj (ind φ A)).obj B) : Type u) →ₗ[k]
              (↑(((MonoidalCategory.curriedTensor (Rep k H)).obj (ind φ A)).obj B) : Type u))
        x)
    (TensorProduct.lift
      (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (TensorProduct.lift
          ((lift
                ((↑A : Type u) →ₗ[k]
                  (↑B : Type u) →ₗ[k]
                    (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ.Coinvariants)
                k H :
              (a :
                  H →
                    (↑A : Type u) →ₗ[k]
                      (↑B : Type u) →ₗ[k]
                        (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants) →
                (H →₀ k) →ₗ[k]
                  (↑A : Type u) →ₗ[k]
                    (↑B : Type u) →ₗ[k]
                      (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
            fun (g : H) ↦
            LinearMap.compl₂ (σ₄₂ := RingHom.id k) (A.coinvariantsTensorMk (res φ B))
              ((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g)))
        ⋯))

Tactic:
simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V, tensor_ρ, res_obj_ρ,
      Functor.postcompose₂_obj_obj_obj_obj, coinvariantsFunctor_obj_carrier,
      tprod_apply, ind_apply]

Premises used: Representation.tprod_apply, Rep.coinvariantsFunctor_obj_carrier, Rep.tensor_ρ, CategoryTheory.MonoidalCategory.curriedTensor_obj_obj, CategoryTheory.Functor.postcompose₂_obj_obj_obj_obj, Rep.res_obj_ρ, Rep.tensor_V, Representation.ind_apply