awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
h : H
f : C(H, V)
hf : Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) f
⊢ Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) (f.comp (ContinuousMap.mulRight h))

Tactic:
simp [mul_assoc, hf _]

Premises used: mul_assoc
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
h : H
x x_1 : ↥(coindV φ π : Submodule R C(H, V))
⊢ (match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V))) x + x_1 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 h)) ⋯) =
    HAdd.hAdd (α := ↥(coindV φ π : Submodule R C(H, V))) (β := ↥(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 h)) ⋯ :
        ↥(coindV φ π : Submodule R C(H, V)))
      (match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V))) x_1 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 h)) ⋯ :
        ↥(coindV φ π : Submodule R C(H, V)))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
h : H
x : R
x_1 : ↥(coindV φ π : Submodule R C(H, V))
⊢ (match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V))) x • x_1 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 h)) ⋯) =
    HSMul.hSMul (α := R) (β := ↥(coindV φ π : Submodule R C(H, V))) ((RingHom.id R : (a : R) → R) x : R)
      (match (motive := ↥(coindV φ π : Submodule R C(H, V)) → ↥(coindV φ π : Submodule R C(H, V))) x_1 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 h)) ⋯ :
        ↥(coindV φ π : Submodule R C(H, V)))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
h : H
⊢ Continuous (X := ↥(coindV φ π : Submodule R C(H, V))) (Y := C(H, V))
    (Function.comp (β := ↥(coindV φ π : Submodule R C(H, V)))
      (Subtype.val (p := fun (x : C(H, V)) ↦
        Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) x))
      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 h)) ⋯)

Tactic:
simpa using (ContinuousMap.mulRight h).continuous_precomp.comp continuous_subtype_val

Premises used: ContinuousMap.mulRight, continuous_subtype_val, Continuous.comp, ContinuousMap.continuous_precomp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
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 1)) ⋯,
                      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                    (a : ↥(coindV φ π)) → ↥(coindV φ π))
                  x) :
              C(H, V)) :
            (a : H) → V)
          a :
        V)
      (((↑((1 : (a : ↥(coindV φ π)) → ↥(coindV φ π)) x) : C(H, V)) : (a : H) → V) a : V)
⊢ Eq (α := ↥(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 1)) ⋯,
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
    1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
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 1)) ⋯,
                    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                  (a : ↥(coindV φ π)) → ↥(coindV φ π))
                x) :
            C(H, V)) :
          (a : H) → V)
        a :
      V)
    (((↑((1 : (a : ↥(coindV φ π)) → ↥(coindV φ π)) x) : C(H, V)) : (a : H) → V) a : V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
g : G
x x_1 : C(G, V)
h :
  ∀ (a : G),
    Eq.{u_3 + 1} (α := V)
      ((comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) ((x + x_1).comp (ContinuousMap.mulLeft g⁻¹)) :
            (a : G) → V)
          a :
        V)
      ((HAdd.hAdd (α := C(G, V))
              (comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) (x.comp (ContinuousMap.mulLeft g⁻¹)))
              (comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) (x_1.comp (ContinuousMap.mulLeft g⁻¹))) :
            (a : G) → V)
          a :
        V)
⊢ comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) ((x + x_1).comp (ContinuousMap.mulLeft g⁻¹)) =
    HAdd.hAdd (α := C(G, V))
      (comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) (x.comp (ContinuousMap.mulLeft g⁻¹)))
      (comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) (x_1.comp (ContinuousMap.mulLeft g⁻¹)))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
g : G
x x_1 : C(G, V)
a : G
⊢ Eq.{u_3 + 1} (α := V)
    ((comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) ((x + x_1).comp (ContinuousMap.mulLeft g⁻¹)) :
          (a : G) → V)
        a :
      V)
    ((HAdd.hAdd (α := C(G, V))
            (comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) (x.comp (ContinuousMap.mulLeft g⁻¹)))
            (comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) (x_1.comp (ContinuousMap.mulLeft g⁻¹))) :
          (a : G) → V)
        a :
      V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
g : G
x : R
x_1 : C(G, V)
h :
  ∀ (a : G),
    Eq.{u_3 + 1} (α := V)
      ((comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) ((x • x_1).comp (ContinuousMap.mulLeft g⁻¹)) :
            (a : G) → V)
          a :
        V)
      ((HSMul.hSMul (α := R) (β := C(G, V)) ((RingHom.id R : (a : R) → R) x : R)
              (comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) (x_1.comp (ContinuousMap.mulLeft g⁻¹))) :
            (a : G) → V)
          a :
        V)
⊢ comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) ((x • x_1).comp (ContinuousMap.mulLeft g⁻¹)) =
    HSMul.hSMul (α := R) (β := C(G, V)) ((RingHom.id R : (a : R) → R) x : R)
      (comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) (x_1.comp (ContinuousMap.mulLeft g⁻¹)))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
g : G
x : R
x_1 : C(G, V)
a : G
⊢ Eq.{u_3 + 1} (α := V)
    ((comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) ((x • x_1).comp (ContinuousMap.mulLeft g⁻¹)) :
          (a : G) → V)
        a :
      V)
    ((HSMul.hSMul (α := R) (β := C(G, V)) ((RingHom.id R : (a : R) → R) x : R)
            (comp (↑((π : (a : G) → V →L[R] V) g : V →L[R] V) : C(V, V)) (x_1.comp (ContinuousMap.mulLeft g⁻¹))) :
          (a : G) → V)
        a :
      V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
h :
  ∀ (x : C(G, V)) (a : G),
    Eq.{u_3 + 1} (α := V)
      (((({
                    toFun := fun (f : C(G, V)) ↦
                      comp (↑((π : (a : G) → V →L[R] V) 1) : C(V, V)) (f.comp (ContinuousMap.mulLeft 1⁻¹)),
                    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                  (a : C(G, V)) → C(G, V))
                x :
              C(G, V)) :
            (a : G) → V)
          a :
        V)
      ((((1 : (a : C(G, V)) → C(G, V)) x : C(G, V)) : (a : G) → V) a : V)
⊢ Eq (α := C(G, V) →L[R] C(G, V))
    { toFun := fun (f : C(G, V)) ↦ comp (↑((π : (a : G) → V →L[R] V) 1) : C(V, V)) (f.comp (ContinuousMap.mulLeft 1⁻¹)),
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
    1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
x : C(G, V)
a : G
⊢ Eq.{u_3 + 1} (α := V)
    (((({
                  toFun := fun (f : C(G, V)) ↦
                    comp (↑((π : (a : G) → V →L[R] V) 1) : C(V, V)) (f.comp (ContinuousMap.mulLeft 1⁻¹)),
                  map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                (a : C(G, V)) → C(G, V))
              x :
            C(G, V)) :
          (a : G) → V)
        a :
      V)
    ((((1 : (a : C(G, V)) → C(G, V)) x : C(G, V)) : (a : G) → V) a : V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
x x_1 : G
h :
  ∀ (x_2 : C(G, V)) (a : G),
    Eq.{u_3 + 1} (α := V)
      (((({
                    toFun := fun (f : C(G, V)) ↦
                      comp (↑((π : (a : G) → V →L[R] V) (x * x_1) : V →L[R] V) : C(V, V))
                        (f.comp (ContinuousMap.mulLeft (x * x_1)⁻¹)),
                    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                  (a : C(G, V)) → C(G, V))
                x_2 :
              C(G, V)) :
            (a : G) → V)
          a :
        V)
      ((((HMul.hMul (α := C(G, V) →L[R] C(G, V))
                    {
                      toFun := fun (f : C(G, V)) ↦
                        comp (↑((π : (a : G) → V →L[R] V) x : V →L[R] V) : C(V, V))
                          (f.comp (ContinuousMap.mulLeft x⁻¹)),
                      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C(G, V) →L[R] C(G, V) }
                    {
                      toFun := fun (f : C(G, V)) ↦
                        comp (↑((π : (a : G) → V →L[R] V) x_1 : V →L[R] V) : C(V, V))
                          (f.comp (ContinuousMap.mulLeft x_1⁻¹)),
                      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C(G, V) →L[R] C(G, V) } :
                  (a : C(G, V)) → C(G, V))
                x_2 :
              C(G, V)) :
            (a : G) → V)
          a :
        V)
⊢ {
      toFun := fun (f : C(G, V)) ↦
        comp (↑((π : (a : G) → V →L[R] V) (x * x_1) : V →L[R] V) : C(V, V))
          (f.comp (ContinuousMap.mulLeft (x * x_1)⁻¹)),
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    HMul.hMul (α := C(G, V) →L[R] C(G, V))
      {
        toFun := fun (f : C(G, V)) ↦
          comp (↑((π : (a : G) → V →L[R] V) x : V →L[R] V) : C(V, V)) (f.comp (ContinuousMap.mulLeft x⁻¹)),
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C(G, V) →L[R] C(G, V) }
      {
        toFun := fun (f : C(G, V)) ↦
          comp (↑((π : (a : G) → V →L[R] V) x_1 : V →L[R] V) : C(V, V)) (f.comp (ContinuousMap.mulLeft x_1⁻¹)),
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C(G, V) →L[R] C(G, V) }

Tactic:
ext