-- 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 :
  ∀ (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)
⊢ Eq (α :=
    TensorProduct k (H →₀ k) (↑A : Type u) →ₗ[k]
      (↑B : Type u) →ₗ[k]
        (Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ.Coinvariants)
    (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)
    (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:
ext