-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
x x_1 : H
h :
  ∀ (x_2 : res φ (leftRegular k H) ⟶ A) (a : H),
    Eq (α := (↑A : Type (max u w)))
      (((Representation.IntertwiningMap.toLinearMap
                (Hom.hom
                  (({
                        toFun := fun (f : res φ (leftRegular k H) ⟶ A) ↦
                          CategoryTheory.Functor.map (resFunctor φ)
                              (((↑(LinearEquiv.symm (leftRegularHomEquiv (leftRegular k H))) :
                                    (↑(leftRegular k H) : Type (max u w)) →ₗ[k] leftRegular k H ⟶ leftRegular k H) :
                                  (a : (↑(leftRegular k H) : Type (max u w))) → leftRegular k H ⟶ leftRegular k H)
                                (single (x * x_1) 1)) ≫
                            f,
                        map_add' := ⋯, map_smul' := ⋯ :
                        (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A } :
                      (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ A)
                    x_2)) :
              (↑(res φ (leftRegular k H)) : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) ∘ₗ
            lsingle a :
          (a : k) → (↑A : Type (max u w)))
        1)
      (((Representation.IntertwiningMap.toLinearMap
                (Hom.hom
                  ((HMul.hMul (α := (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A)
                        {
                          toFun := fun (f : res φ (leftRegular k H) ⟶ A) ↦
                            CategoryTheory.Functor.map (resFunctor φ)
                                (((↑(LinearEquiv.symm (leftRegularHomEquiv (leftRegular k H))) :
                                      (↑(leftRegular k H) : Type (max u w)) →ₗ[k] leftRegular k H ⟶ leftRegular k H) :
                                    (a : (↑(leftRegular k H) : Type (max u w))) → leftRegular k H ⟶ leftRegular k H)
                                  (single x 1)) ≫
                              f,
                          map_add' := ⋯, map_smul' := ⋯ :
                          (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A }
                        {
                          toFun := fun (f : res φ (leftRegular k H) ⟶ A) ↦
                            CategoryTheory.Functor.map (resFunctor φ)
                                (((↑(LinearEquiv.symm (leftRegularHomEquiv (leftRegular k H))) :
                                      (↑(leftRegular k H) : Type (max u w)) →ₗ[k] leftRegular k H ⟶ leftRegular k H) :
                                    (a : (↑(leftRegular k H) : Type (max u w))) → leftRegular k H ⟶ leftRegular k H)
                                  (single x_1 1)) ≫
                              f,
                          map_add' := ⋯, map_smul' := ⋯ :
                          (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A } :
                      (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ A)
                    x_2)) :
              (↑(res φ (leftRegular k H)) : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) ∘ₗ
            lsingle a :
          (a : k) → (↑A : Type (max u w)))
        1)
⊢ {
      toFun := fun (f : res φ (leftRegular k H) ⟶ A) ↦
        CategoryTheory.Functor.map (resFunctor φ)
            (((↑(LinearEquiv.symm (leftRegularHomEquiv (leftRegular k H))) :
                  (↑(leftRegular k H) : Type (max u w)) →ₗ[k] leftRegular k H ⟶ leftRegular k H) :
                (a : (↑(leftRegular k H) : Type (max u w))) → leftRegular k H ⟶ leftRegular k H)
              (single (x * x_1) 1)) ≫
          f,
      map_add' := ⋯, map_smul' := ⋯ } =
    HMul.hMul (α := (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A)
      {
        toFun := fun (f : res φ (leftRegular k H) ⟶ A) ↦
          CategoryTheory.Functor.map (resFunctor φ)
              (((↑(LinearEquiv.symm (leftRegularHomEquiv (leftRegular k H))) :
                    (↑(leftRegular k H) : Type (max u w)) →ₗ[k] leftRegular k H ⟶ leftRegular k H) :
                  (a : (↑(leftRegular k H) : Type (max u w))) → leftRegular k H ⟶ leftRegular k H)
                (single x 1)) ≫
            f,
        map_add' := ⋯, map_smul' := ⋯ : (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A }
      {
        toFun := fun (f : res φ (leftRegular k H) ⟶ A) ↦
          CategoryTheory.Functor.map (resFunctor φ)
              (((↑(LinearEquiv.symm (leftRegularHomEquiv (leftRegular k H))) :
                    (↑(leftRegular k H) : Type (max u w)) →ₗ[k] leftRegular k H ⟶ leftRegular k H) :
                  (a : (↑(leftRegular k H) : Type (max u w))) → leftRegular k H ⟶ leftRegular k H)
                (single x_1 1)) ≫
            f,
        map_add' := ⋯, map_smul' := ⋯ : (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A }

Tactic:
ext