-- 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
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)

Tactic:
simp [homEquiv, mul_assoc]

Premises used: Rep.homEquiv, mul_assoc