awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
π₁_1 : ContRepresentation R G V
π₂_1 : ContRepresentation R G W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
h : G
rw :
  f.toContinuousLinearMap ∘SL g.comp (σ₁₂ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) h) =
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap)
rw₁ :
  f.toContinuousLinearMap ∘SL
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₂ : (a : G) → W →L[R] W) h) g.toContinuousLinearMap =
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap)
rw₂ :
  f.comp (σ₁₂ := RingHom.id R) ((π₂ : (a : G) → W →L[R] W) h) ∘SL g.toContinuousLinearMap =
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap)
rw₃ :
  Eq (α := V →L[R] U)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h) f.toContinuousLinearMap ∘SL
      g.toContinuousLinearMap)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap))
rw₄ rw₅ :
  Eq (α := V →L[R] U)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap))
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap))
⊢ (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap).comp (σ₁₂ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) h) =
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap)

Tactic:
rw [comp_assoc, g.2, ← comp_assoc, f.2, comp_assoc]

Premises used: ContinuousLinearMap.comp_assoc, ContIntertwiningMap.isIntertwining'
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
g : G
⊢ (↑φ.toContinuousLinearEquiv : 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)
      (↑φ.toContinuousLinearEquiv : V →L[R] W)

Tactic:
φ.isIntertwining' g

Premises used: ContRepresentation.Equiv.isIntertwining', ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
e : V ≃L[R] W
he :
  ∀ (g : G),
    (↑e : 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) (↑e : V →L[R] W)
⊢ (mk e he).toContinuousLinearEquiv = e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
e : V ≃L[R] W
he :
  ∀ (g : G),
    (↑e : 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) (↑e : V →L[R] W)
⊢ (↑(mk e he) : ρ →ⁱL σ) = { toContinuousLinearMap := (↑e : V →L[R] W), isIntertwining' := he }

Tactic:
rfl

Premises used: rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
e : V ≃L[R] W
he :
  ∀ (g : G),
    (↑e : 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) (↑e : V →L[R] W)
⊢ (↑(mk e he).toContinuousLinearEquiv : V →L[R] W) = (↑e : V →L[R] W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ ψ : σ.Equiv ρ
h : φ.toContinuousLinearEquiv = ψ.toContinuousLinearEquiv
mk'' :
  ∀ (toContinuousLinearEquiv : W ≃L[R] V)
    (cont : Continuous (↑(↑toContinuousLinearEquiv : W ≃ₗ[R] V) : W →ₗ[R] V).toFun)
    (isIntertwining' :
      ∀ (g : G),
        { toLinearMap := (↑(↑toContinuousLinearEquiv : W ≃ₗ[R] V) : W →ₗ[R] V), cont := cont : W →L[R] V }.comp (σ₁₂ :=
            RingHom.id R) ((σ : (a : G) → W →L[R] W) g) =
          ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g)
            { toLinearMap := (↑(↑toContinuousLinearEquiv : W ≃ₗ[R] V) : W →ₗ[R] V), cont := cont : W →L[R] V })
    (h :
      { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
            σ.Equiv ρ }.toContinuousLinearEquiv =
        ψ.toContinuousLinearEquiv),
    { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
        σ.Equiv ρ } =
      ψ
⊢ φ = ψ

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

Tactic:
simpa [ContIntertwiningMap.ext_iff] using h

Premises used: ContIntertwiningMap.ext_iff
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ ψ : σ.Equiv ρ
⊢ φ.toContinuousLinearEquiv = ψ.toContinuousLinearEquiv ↔ φ = ψ

Tactic:
toContinuousLinearEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, ContRepresentation.Equiv.toContinuousLinearEquiv_injective
-- 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
φ_1 φ ψ : ρ.Equiv σ
h1 : Eq (α := V → W) (⇑φ.toContinuousLinearEquiv : (a : V) → W) (⇑ψ.toContinuousLinearEquiv : (a : V) → W)
h2 : (↑φ.toContinuousLinearEquiv : V ≃ₗ[R] W).invFun = (↑ψ.toContinuousLinearEquiv : V ≃ₗ[R] W).invFun
mk'' :
  ∀ (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),
    { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
        ρ.Equiv σ } =
      ψ
⊢ φ = ψ

Tactic:
cases φ
-- 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 }
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 }

Tactic:
simp_all
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
e : V ≃L[R] W
he :
  ∀ (g : G),
    (↑e : 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) (↑e : V →L[R] W)
v : V
⊢ Eq.{u_4 + 1} (α := W) ((mk e he : (a : V) → W) v : W) ((e : (a : V) → W) v : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ ψ : ρ.Equiv σ
h : Eq (α := (a : V) → W) (⇑φ : (a : V) → W) (⇑ψ : (a : V) → W)
mk'' :
  ∀ (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 })
    (h :
      Eq (α := (a : V) → W)
        (⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
              ρ.Equiv σ } :
          (a : V) → W)
        (⇑ψ : (a : V) → W)),
    { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
        ρ.Equiv σ } =
      ψ
⊢ φ = ψ

Tactic:
cases φ
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
ψ : ρ.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 }
h :
  Eq (α := (a : V) → W)
    (⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
          ρ.Equiv σ } :
      (a : V) → W)
    (⇑ψ : (a : V) → W)
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 })
    (h :
      Eq (α := (a : V) → W)
        (⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
              ρ.Equiv σ } :
          (a : V) → W)
        (⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv_1, cont := cont_1, isIntertwining' := isIntertwining'_1 :
              ρ.Equiv σ } :
          (a : V) → W)),
    { 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 ψ
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
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 }
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 }
h :
  Eq (α := (a : V) → W)
    (⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' :
          ρ.Equiv σ } :
      (a : V) → W)
    (⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv_1, cont := cont_1, isIntertwining' := isIntertwining'_1 :
          ρ.Equiv σ } :
      (a : V) → W)
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' : ρ.Equiv σ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv_1, cont := cont_1, isIntertwining' := isIntertwining'_1 }

Tactic:
simpa using h
-- 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 σ
⊢ ∀ (g : G),
    Eq (α := V →L[R] V)
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id R) (↑(ContinuousLinearEquiv.refl R V) : V →L[R] V)
        ((ρ : (a : G) → V →L[R] V) g))
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g)
        (↑(ContinuousLinearEquiv.refl R V) : V →L[R] V))

Tactic:
simp