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