-- 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
g : G
⊢ 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)))
have 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)
Tactic: ext