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
x x_1 : G
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)

Tactic:
simp [mul_assoc]

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
π : 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)
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)
⊢ 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)

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
π : 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)
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:
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
π : 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)
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)
⊢ 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)

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
π : 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)
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:
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
π : 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
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' := ⋯, map_smul' := ⋯, cont := ⋯ }
                    (((π₁.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' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                  (a : C(G, V)) → C(G, W))
                x :
              C(G, W)) :
            (a : G) → W)
          a :
        W)
⊢ 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 := ⋯ })

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
π : 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
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' := ⋯, map_smul' := ⋯, cont := ⋯ }
                  (((π₁.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' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                (a : C(G, V)) → C(G, W))
              x :
            C(G, W)) :
          (a : G) → W)
        a :
      W)

Tactic:
simp [f.isIntertwining]

Premises used: ContIntertwiningMap.isIntertwining
-- 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),
    Eq (α := V →L[R] C(G, V))
      (ContinuousLinearMap.comp (R₂ := R) (σ₁₂ := RingHom.id R) (σ₂₃ := RingHom.id R)
        { toFun := const G, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ((π : (a : G) → V →L[R] V) g))
      (ContinuousLinearMap.comp (R₂ := R) (σ₁₂ := RingHom.id R) (σ₂₃ := RingHom.id R) (M₂ := C(G, V))
        (((π.coind₁ : ContRepresentation R G C(G, V)) : (a : G) → C(G, V) →L[R] C(G, V)) g)
        { toFun := const G, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ })

Tactic:
aesop
-- 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
π : ContRepresentation R G V
inst_21 : IsTopologicalRing R
inst_22 : IsTopologicalGroup G
inst_23 : IsTopologicalGroup H
⊢ Eq (α := Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V)) (⊤ : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V))
    (coindV 1 (trivial R G V) : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V))

Tactic:
simp [SetLike.ext_iff]

Premises used: SetLike.ext_iff
-- 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
π : ContRepresentation R G V
inst_21 : IsTopologicalRing R
inst_22 : IsTopologicalGroup G
inst_23 : IsTopologicalGroup H
g : ↥⊥
⊢ Eq (α :=
    ContinuousMap.{u_6, u_3} (↥⊥) V →L[R] ↥(coindV 1 (trivial R G V) : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V)))
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id R)
        (↑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm Submodule.topContEquiv)
              (ContinuousLinearEquiv.ofEq ⊤ (coindV 1 (trivial R G V)) ⋯)) :
          C(↥⊥, V) →L[R] ↥(coindV 1 (trivial R G V)))
        (((coind₁ (trivial R (↥⊥) V) : ContRepresentation R (↥⊥) (ContinuousMap.{u_6, u_3} (↥⊥) V)) :
            (a : ↥⊥) → C(↥⊥, V) →L[R] C(↥⊥, V))
          g) :
      ContinuousMap.{u_6, u_3} (↥⊥) V →L[R] ↥(coindV 1 (trivial R G V) : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V)))
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) (M₂ :=
        ↥(coindV 1 (trivial R G V) : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V)))
        ((coind 1 (trivial R G V) : (a : ↥⊥) → ↥(coindV 1 (trivial R G V)) →L[R] ↥(coindV 1 (trivial R G V))) g :
          ↥(coindV 1 (trivial R G V) : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V)) →L[R]
            ↥(coindV 1 (trivial R G V) : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V)))
        ((↑(ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm Submodule.topContEquiv)
                (ContinuousLinearEquiv.ofEq ⊤ (coindV 1 (trivial R G V)) ⋯)) :
            ContinuousMap.{u_6, u_3} (↥⊥) V →L[R]
              ↥(coindV 1 (trivial R G V) : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V))) :
          ContinuousMap.{u_6, u_3} (↥⊥) V →L[R]
            ↥(coindV 1 (trivial R G V) : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V))) :
      ContinuousMap.{u_6, u_3} (↥⊥) V →L[R] ↥(coindV 1 (trivial R G V) : Submodule R (ContinuousMap.{u_6, u_3} (↥⊥) V)))

Tactic:
simp [Subsingleton.elim g 1, ContinuousLinearMap.one_def]

Premises used: Subsingleton.elim, OfNat.ofNat, ContinuousLinearMap.one_def
-- Module: Mathlib.RepresentationTheory.Equiv
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
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)
⊢ 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))

Tactic:
ext a
-- Module: Mathlib.RepresentationTheory.Equiv
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
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:
simp [Subsingleton.elim (g • a) a]

Premises used: HSMul.hSMul, Subsingleton.elim
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Monoid G
H : Type w
inst_2 : Subsingleton H
inst_3 : MulOneClass H
inst_4 : MulAction G H
f : H →₀ k
⊢ Eq.{u + 1} (α := k)
    ((IntertwiningMap.toLinearMap (ρ := ofMulAction k G H)
            (↑(ofMulActionSubsingletonEquivTrivial k G H) : (ofMulAction k G H).IntertwiningMap (trivial k G k)) :
          (a : H →₀ k) → k)
        f :
      k)
    ((f : (a : H) → k) 1 : k)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Monoid G
H : Type w
inst_2 : Subsingleton H
inst_3 : MulOneClass H
inst_4 : MulAction G H
r : k
⊢ Eq (α := H →₀ k)
    ((IntertwiningMap.toLinearMap (σ := ofMulAction k G H)
            (↑(Equiv.symm (ofMulActionSubsingletonEquivTrivial k G H)) :
              (trivial k G k).IntertwiningMap (ofMulAction k G H)) :
          (a : k) → H →₀ k)
        r :
      H →₀ k)
    (Finsupp.single 1 r : H →₀ k)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Equiv
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
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)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Equiv
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
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:
simp
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Monoid G
f : Fin 1 → G
r : k
⊢ Eq (α := G →₀ k) ((diagonalOneEquivLeftRegular k G : (a : (Fin 1 → G) →₀ k) → G →₀ k) (Finsupp.single f r) : G →₀ k)
    (Finsupp.single (f 0) r : G →₀ k)

Tactic:
simp [diagonalOneEquivLeftRegular]

Premises used: Representation.diagonalOneEquivLeftRegular
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Monoid G
g : G
r : k
⊢ Eq (α := Finsupp.{v, u} (Fin 1 → G) k)
    ((Equiv.symm (diagonalOneEquivLeftRegular k G) : (a : G →₀ k) → (Fin 1 → G) →₀ k) (Finsupp.single g r) :
      Finsupp.{v, u} (Fin 1 → G) k)
    (Finsupp.single (uniqueElim (α := fun (i : Fin 1) ↦ G) g) r : Finsupp.{v, u} ((i : Fin 1) → G) k)

Tactic:
simp [diagonalOneEquivLeftRegular]

Premises used: Representation.diagonalOneEquivLeftRegular