-- 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
g : G
a : H
x : (↑A : Type u)
x_1 : (↑B : Type u)
⊢ Eq (α := (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ.Coinvariants)
    ((((((TensorProduct.AlgebraTensorModule.curry
                          (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)) ∘ₗ
                            (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ :
                                (a : G) →
                                  TensorProduct k (H →₀ k) (↑A : Type u) →ₗ[k] TensorProduct k (H →₀ k) (↑A : Type u))
                              g) ∘ₗ
                        lsingle a :
                      k →ₗ[k]
                        (↑A : Type u) →ₗ[k]
                          (↑B : Type u) →ₗ[k]
                            (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A)
                                  (res φ B)).ρ.Coinvariants) :
                    (a : k) →
                      (↑A : Type u) →ₗ[k]
                        (↑B : Type u) →ₗ[k]
                          (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                  1 :
                (a : (↑A : Type u)) →
                  (↑B : Type u) →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
              x :
            (↑B : Type u) →ₗ[k]
              (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ.Coinvariants) :
          (a : (↑B : Type u)) → (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
        x_1 :
      (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ.Coinvariants)
    ((((((TensorProduct.AlgebraTensorModule.curry
                          (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))) ∘ₗ
                        lsingle a :
                      k →ₗ[k]
                        (↑A : Type u) →ₗ[k]
                          (↑B : Type u) →ₗ[k]
                            (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A)
                                  (res φ B)).ρ.Coinvariants) :
                    (a : k) →
                      (↑A : Type u) →ₗ[k]
                        (↑B : Type u) →ₗ[k]
                          (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                  1 :
                (a : (↑A : Type u)) →
                  (↑B : Type u) →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
              x :
            (↑B : Type u) →ₗ[k]
              (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ.Coinvariants) :
          (a : (↑B : Type u)) → (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
        x_1 :
      (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ.Coinvariants)

Tactic:
simpa [coinvariantsTensorMk, Coinvariants.mk_eq_iff]
        using Coinvariants.sub_mem_ker _ _

Premises used: Representation.Coinvariants.sub_mem_ker, Representation.Coinvariants.mk_eq_iff, Rep.coinvariantsTensorMk