-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G_1 : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G_1
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
G : Type u_6
H : Type u_7
inst_14 : Group G
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace R
inst_17 : ContinuousSMul R V
inst_18 : ContinuousSMul R W
inst_19 : Group H
inst_20 : TopologicalSpace H
φ : G →ₜ* H
π_1 : ContRepresentation R G V
inst_21 : IsTopologicalRing R
inst_22 : IsTopologicalGroup G
inst_23 : IsTopologicalGroup H
π : ContRepresentation R G V
h1 h2 : H
h :
  ∀ (x : ↥(coindV φ π : Submodule R C(H, V))) (a : H),
    Eq.{u_3 + 1} (α := V)
      (((↑(({
                      toFun := fun (x : ↥(coindV φ π : Submodule R C(H, V))) ↦
                        match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V)))
                          x with
                        | ⟨f, hf⟩ =>
                          Subtype.mk (p := fun (x : C(H, V)) ↦
                            Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) x)
                            (f.comp (ContinuousMap.mulRight (h1 * h2))) ⋯,
                      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                    (a : ↥(coindV φ π)) → ↥(coindV φ π))
                  x) :
              C(H, V)) :
            (a : H) → V)
          a :
        V)
      (((↑((HMul.hMul (α := ↥(coindV φ π : Submodule R C(H, V)) →L[R] ↥(coindV φ π : Submodule R C(H, V)))
                      {
                        toFun := fun (x : ↥(coindV φ π : Submodule R C(H, V))) ↦
                          match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V)))
                            x with
                          | ⟨f, hf⟩ =>
                            Subtype.mk (p := fun (x : C(H, V)) ↦
                              Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) x)
                              (f.comp (ContinuousMap.mulRight h1)) ⋯,
                        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
                        ↥(coindV φ π : Submodule R C(H, V)) →L[R] ↥(coindV φ π : Submodule R C(H, V)) }
                      {
                        toFun := fun (x : ↥(coindV φ π : Submodule R C(H, V))) ↦
                          match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V)))
                            x with
                          | ⟨f, hf⟩ =>
                            Subtype.mk (p := fun (x : C(H, V)) ↦
                              Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) x)
                              (f.comp (ContinuousMap.mulRight h2)) ⋯,
                        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
                        ↥(coindV φ π : Submodule R C(H, V)) →L[R] ↥(coindV φ π : Submodule R C(H, V)) } :
                    (a : ↥(coindV φ π)) → ↥(coindV φ π))
                  x) :
              C(H, V)) :
            (a : H) → V)
          a :
        V)
⊢ {
      toFun := fun (x : ↥(coindV φ π : Submodule R C(H, V))) ↦
        match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V))) x with
        | ⟨f, hf⟩ =>
          Subtype.mk (p := fun (x : C(H, V)) ↦
            Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) x)
            (f.comp (ContinuousMap.mulRight (h1 * h2))) ⋯,
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    HMul.hMul (α := ↥(coindV φ π : Submodule R C(H, V)) →L[R] ↥(coindV φ π : Submodule R C(H, V)))
      {
        toFun := fun (x : ↥(coindV φ π : Submodule R C(H, V))) ↦
          match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V))) x with
          | ⟨f, hf⟩ =>
            Subtype.mk (p := fun (x : C(H, V)) ↦
              Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) x)
              (f.comp (ContinuousMap.mulRight h1)) ⋯,
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
        ↥(coindV φ π : Submodule R C(H, V)) →L[R] ↥(coindV φ π : Submodule R C(H, V)) }
      {
        toFun := fun (x : ↥(coindV φ π : Submodule R C(H, V))) ↦
          match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V))) x with
          | ⟨f, hf⟩ =>
            Subtype.mk (p := fun (x : C(H, V)) ↦
              Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) x)
              (f.comp (ContinuousMap.mulRight h2)) ⋯,
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
        ↥(coindV φ π : Submodule R C(H, V)) →L[R] ↥(coindV φ π : Submodule R C(H, V)) }

Tactic:
ext