Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk''.mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
toContinuousLinearEquiv✝¹ : V ≃L[R] W
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h1 :
  ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹,
          isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearEquiv =
    ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
          isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv
h2 :
  (↑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹,
            isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearEquiv).invFun =
    (↑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
            isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv).invFun
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }

Tactic:
;

Goal state after:
case mk''.mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
toContinuousLinearEquiv✝¹ : V ≃L[R] W
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h1 :
  ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹,
          isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearEquiv =
    ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
          isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv
h2 :
  (↑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹,
            isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearEquiv).invFun =
    (↑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
            isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv).invFun
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }