awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: rw [comp_assoc, g.2, ← comp_assoc, f.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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)
⊢ (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)
have 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))
Tactic: rw [comp_assoc, g.2, ← comp_assoc, f.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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))
⊢ (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)
have 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))
Tactic: rw [comp_assoc, g.2, ← comp_assoc, f.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
⊢ φ = ψ
have 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 φ
Cleared hypotheses: φ, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' : σ.Equiv ρ } =
    ψ
have 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 }
Tactic: cases ψ
Cleared hypotheses: ψ, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
⊢ φ = ψ
have 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 φ
Cleared hypotheses: φ, h1, h2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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)
⊢ φ = ψ
have 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 φ
Cleared hypotheses: φ, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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)
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' : ρ.Equiv σ } =
    ψ
have 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 }
Tactic: cases ψ
Cleared hypotheses: ψ, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
⊢ (↑φ.symm : W →L[R] V).comp (σ₁₂ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) =
    comp (σ₂₃ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) (↑φ.symm : W →L[R] V)
have rw : ((↑φ.toContinuousLinearEquiv : V →L[R] W) ∘SL (↑φ.symm : W →L[R] V)).comp (σ₁₂ := RingHom.id R)
    ((σ : (a : G) → W →L[R] W) g) =
  (↑φ.toContinuousLinearEquiv : V →L[R] W).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) ∘SL
    (↑φ.symm : W →L[R] V)
Tactic: rw [← cancel_left' (g := φ.toContinuousLinearEquiv.toContinuousLinearMap)
    φ.toContinuousLinearEquiv.injective, ← comp_assoc, ← comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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 σ
ψ : σ.Equiv τ
g : G
⊢ (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g) (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U)
have rw : ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W)).comp (σ₁₂ := RingHom.id R)
    ((ρ : (a : G) → V →L[R] V) g) =
  comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
    ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
Tactic: rw [← ContinuousLinearEquiv.comp_coe, comp_assoc,
    φ.isIntertwining, ← comp_assoc, ψ.isIntertwining, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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 σ
ψ : σ.Equiv τ
g : G
rw :
  ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W)).comp (σ₁₂ := RingHom.id R)
      ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
⊢ (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g) (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U)
have rw₁ : (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL
    (↑φ.toContinuousLinearEquiv : V →L[R] W).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
  comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
    ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
Tactic: rw [← ContinuousLinearEquiv.comp_coe, comp_assoc,
    φ.isIntertwining, ← comp_assoc, ψ.isIntertwining, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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 σ
ψ : σ.Equiv τ
g : G
rw :
  ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W)).comp (σ₁₂ := RingHom.id R)
      ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
rw₁ :
  (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL
      (↑φ.toContinuousLinearEquiv : V →L[R] W).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
⊢ (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g) (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U)
have rw₂ : (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL
    comp (σ₂₃ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) (↑φ.toContinuousLinearEquiv : V →L[R] W) =
  comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
    ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
Tactic: rw [← ContinuousLinearEquiv.comp_coe, comp_assoc,
    φ.isIntertwining, ← comp_assoc, ψ.isIntertwining, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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 σ
ψ : σ.Equiv τ
g : G
rw :
  ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W)).comp (σ₁₂ := RingHom.id R)
      ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
rw₁ :
  (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL
      (↑φ.toContinuousLinearEquiv : V →L[R] W).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
rw₂ :
  (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL
      comp (σ₂₃ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) (↑φ.toContinuousLinearEquiv : V →L[R] W) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
⊢ (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g) (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U)
have rw₃ : (↑ψ.toContinuousLinearEquiv : W →L[R] U).comp (σ₁₂ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) ∘SL
    (↑φ.toContinuousLinearEquiv : V →L[R] W) =
  comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
    ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
Tactic: rw [← ContinuousLinearEquiv.comp_coe, comp_assoc,
    φ.isIntertwining, ← comp_assoc, ψ.isIntertwining, comp_assoc]