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
ρ : 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))
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))
⊢ (↑(φ.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₄ : Eq (α := V →L[R] U)
  (comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g) (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘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]
-- 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))
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))
rw₄ :
  Eq (α := V →L[R] U)
    (comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g) (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘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)))
⊢ (↑(φ.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₅ : Eq (α := V →L[R] U)
  (comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
    ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘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]
-- 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 σ
⊢ φ.trans φ.symm = refl ρ
have h : ∀ (x : V), Eq (α := V) ((φ.trans φ.symm : (a : V) → V) x : V) ((refl ρ : (a : V) → V) x : V)
Tactic: ext
-- 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 σ
⊢ φ.symm.trans φ = refl σ
have h : ∀ (x : W), Eq (α := W) ((φ.symm.trans φ : (a : W) → W) x : W) ((refl σ : (a : W) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
⊢ 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
have 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)) sorry,
                    map_add' := sorry, map_smul' := sorry, cont := sorry } :
                  (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: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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)
⊢ 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⁻¹)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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)
⊢ 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⁻¹)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
⊢ 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
have 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' := sorry, map_smul' := sorry, cont := sorry } :
                (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: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
⊢ {
      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) }
have 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' := sorry, map_smul' := sorry, cont := sorry } :
                (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' := sorry, map_smul' := sorry, cont := sorry : 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' := sorry, map_smul' := sorry, cont := sorry : 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
π : ContRepresentation R G V
inst_21 : IsTopologicalRing R
inst_22 : IsTopologicalGroup G
inst_23 : IsTopologicalGroup H
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f : π₁ →ⁱL π₂
x x_1 : C(G, V)
⊢ comp (↑f : C(V, W)) (x + x_1) = HAdd.hAdd (α := C(G, W)) (comp (↑f : C(V, W)) x) (comp (↑f : C(V, W)) x_1)
have h : ∀ (a : G),
  Eq.{u_4 + 1} (α := W) ((comp (↑f : C(V, W)) (x + x_1) : (a : G) → W) a : W)
    ((HAdd.hAdd (α := C(G, W)) (comp (↑f : C(V, W)) x) (comp (↑f : C(V, W)) x_1) : (a : G) → W) a : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
π : ContRepresentation R G V
inst_21 : IsTopologicalRing R
inst_22 : IsTopologicalGroup G
inst_23 : IsTopologicalGroup H
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f : π₁ →ⁱL π₂
x : R
x_1 : C(G, V)
⊢ comp (↑f : C(V, W)) (x • x_1) =
    HSMul.hSMul (α := R) (β := C(G, W)) ((RingHom.id R : (a : R) → R) x : R) (comp (↑f : C(V, W)) x_1)
have h : ∀ (a : G),
  Eq.{u_4 + 1} (α := W) ((comp (↑f : C(V, W)) (x • x_1) : (a : G) → W) a : W)
    ((HSMul.hSMul (α := R) (β := C(G, W)) ((RingHom.id R : (a : R) → R) x : R) (comp (↑f : C(V, W)) x_1) : (a : G) → W)
        a :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
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
π : ContRepresentation R G V
inst_21 : IsTopologicalRing R
inst_22 : IsTopologicalGroup G
inst_23 : IsTopologicalGroup H
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f : π₁ →ⁱL π₂
g : G
⊢ Eq (α := C(G, V) →L[R] C(G, W))
    (ContinuousLinearMap.comp (R₂ := R) (σ₁₂ := RingHom.id R) (σ₂₃ := RingHom.id R) (M₂ := C(G, V))
      { toFun := comp (↑f : C(V, W)), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
      (((π₁.coind₁ : ContRepresentation R G C(G, V)) : (a : G) → C(G, V) →L[R] C(G, V)) g))
    (ContinuousLinearMap.comp (R₂ := R) (σ₁₂ := RingHom.id R) (σ₂₃ := RingHom.id R) (M₂ := C(G, W))
      (((π₂.coind₁ : ContRepresentation R G C(G, W)) : (a : G) → C(G, W) →L[R] C(G, W)) g)
      { toFun := comp (↑f : C(V, W)), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ })
have h : ∀ (x : C(G, V)) (a : G),
  Eq.{u_4 + 1} (α := W)
    ((((ContinuousLinearMap.comp (R₂ := R) (σ₁₂ := RingHom.id R) (σ₂₃ := RingHom.id R) (M₂ := C(G, V))
                  { toFun := comp (↑f : C(V, W)), map_add' := sorry, map_smul' := sorry, cont := sorry }
                  (((π₁.coind₁ : ContRepresentation R G C(G, V)) : (a : G) → C(G, V) →L[R] C(G, V)) g) :
                (a : C(G, V)) → C(G, W))
              x :
            C(G, W)) :
          (a : G) → W)
        a :
      W)
    ((((ContinuousLinearMap.comp (R₂ := R) (σ₁₂ := RingHom.id R) (σ₂₃ := RingHom.id R) (M₂ := C(G, W))
                  (((π₂.coind₁ : ContRepresentation R G C(G, W)) : (a : G) → C(G, W) →L[R] C(G, W)) g)
                  { toFun := comp (↑f : C(V, W)), map_add' := sorry, map_smul' := sorry, cont := sorry } :
                (a : C(G, V)) → C(G, W))
              x :
            C(G, W)) :
          (a : G) → W)
        a :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Equiv (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
g : G
⊢ Eq (α := (H →₀ k) →ₗ[k] k)
    ((↑(Finsupp.uniqueLinearEquiv k k 1) : (H →₀ k) →ₗ[k] k) ∘ₗ (ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g)
    (((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g ∘ₗ
      (↑(Finsupp.uniqueLinearEquiv k k 1) : (H →₀ k) →ₗ[k] k))
have h : ∀ (a : H),
  Eq (α := k)
    ((((↑(Finsupp.uniqueLinearEquiv k k 1) : (H →₀ k) →ₗ[k] k) ∘ₗ
              (ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → k)
        1 :
      k)
    (((((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g ∘ₗ
              (↑(Finsupp.uniqueLinearEquiv k k 1) : (H →₀ k) →ₗ[k] k)) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → k)
        1 :
      k)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RepresentationTheory.Equiv (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
g : G
⊢ Eq (α := Finsupp.{v, u} (Fin 1 → G) k →ₗ[k] G →₀ k)
    ((↑(Finsupp.domLCongr (Equiv.funUnique (Fin 1) G)) : ((Fin 1 → G) →₀ k) →ₗ[k] G →₀ k) ∘ₗ
      (diagonal k G 1 : (a : G) → ((Fin 1 → G) →₀ k) →ₗ[k] (Fin 1 → G) →₀ k) g)
    ((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g ∘ₗ
      (↑(Finsupp.domLCongr (Equiv.funUnique (Fin 1) G)) : ((Fin 1 → G) →₀ k) →ₗ[k] G →₀ k))
have h : ∀ (a : Fin 1 → G) (a_1 : G),
  Eq.{u + 1} (α := k)
    (((((↑(Finsupp.domLCongr (Equiv.funUnique (Fin 1) G)) : ((Fin 1 → G) →₀ k) →ₗ[k] G →₀ k) ∘ₗ
                  (diagonal k G 1 : (a : G) → ((Fin 1 → G) →₀ k) →ₗ[k] (Fin 1 → G) →₀ k) g) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → G →₀ k)
            1 :
          (a : G) → k)
        a_1 :
      k)
    (((((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g ∘ₗ
                  (↑(Finsupp.domLCongr (Equiv.funUnique (Fin 1) G)) : ((Fin 1 → G) →₀ k) →ₗ[k] G →₀ k)) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → G →₀ k)
            1 :
          (a : G) → k)
        a_1 :
      k)
Tactic: ext