-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ ψ : ρ.Equiv σ
toContinuousLinearEquiv : V ≃L[R] W
cont : Continuous (↑(↑toContinuousLinearEquiv : V ≃ₗ[R] W) : V →ₗ[R] W).toFun
isIntertwining' :
  ∀ (g : G),
    { toLinearMap := (↑(↑toContinuousLinearEquiv : V ≃ₗ[R] W) : V →ₗ[R] W), cont := cont : V →L[R] W }.comp (σ₁₂ :=
        RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g)
        { toLinearMap := (↑(↑toContinuousLinearEquiv : V ≃ₗ[R] W) : V →ₗ[R] W), cont := cont : V →L[R] W }
h1 :
  Eq (α := V → W)
    (⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
            ρ.Equiv σ }.toContinuousLinearEquiv :
      (a : V) → W)
    (⇑ψ.toContinuousLinearEquiv : (a : V) → W)
h2 :
  (↑{ toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
              ρ.Equiv σ }.toContinuousLinearEquiv :
        V ≃ₗ[R] W).invFun =
    (↑ψ.toContinuousLinearEquiv : V ≃ₗ[R] W).invFun
mk'' :
  ∀ (toContinuousLinearEquiv_1 : V ≃L[R] W)
    (cont_1 : Continuous (↑(↑toContinuousLinearEquiv_1 : V ≃ₗ[R] W) : V →ₗ[R] W).toFun)
    (isIntertwining'_1 :
      ∀ (g : G),
        { toLinearMap := (↑(↑toContinuousLinearEquiv_1 : V ≃ₗ[R] W) : V →ₗ[R] W), cont := cont_1 : V →L[R] W }.comp
            (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
          ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g)
            { toLinearMap := (↑(↑toContinuousLinearEquiv_1 : V ≃ₗ[R] W) : V →ₗ[R] W), cont := cont_1 : V →L[R] W })
    (h1 :
      Eq (α := V → W)
        (⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
                ρ.Equiv σ }.toContinuousLinearEquiv :
          (a : V) → W)
        (⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv_1, cont := cont_1, isIntertwining' := isIntertwining'_1 :
                ρ.Equiv σ }.toContinuousLinearEquiv :
          (a : V) → W))
    (h2 :
      (↑{ toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
                  ρ.Equiv σ }.toContinuousLinearEquiv :
            V ≃ₗ[R] W).invFun =
        (↑{ toContinuousLinearEquiv := toContinuousLinearEquiv_1, cont := cont_1, isIntertwining' := isIntertwining'_1 :
                  ρ.Equiv σ }.toContinuousLinearEquiv :
            V ≃ₗ[R] W).invFun),
    { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
        ρ.Equiv σ } =
      { toContinuousLinearEquiv := toContinuousLinearEquiv_1, cont := cont_1, isIntertwining' := isIntertwining'_1 }
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' : ρ.Equiv σ } =
    ψ

Tactic:
cases ψ