-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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
⊢ {
      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 }
have 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' := sorry, map_smul' := sorry :
                      (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' := sorry, map_smul' := sorry :
                        (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' := sorry, map_smul' := sorry :
                        (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: ext