awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f₁ f₂ : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
⊢ (f₁ + f₂).tensor g = f₁.tensor g + f₂.tensor g
have h : ∀ (x : V) (x_1 : U),
  Eq (α := TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry ((f₁ + f₂).tensor g).toLinearMap :
                  V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (f₁.tensor g + f₂.tensor g).toLinearMap :
                  V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
⊢ f.tensor (g₁ + g₂) = f.tensor g₁ + f.tensor g₂
have h : ∀ (x : V) (x_1 : U),
  Eq (α := TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor (g₁ + g₂)).toLinearMap :
                  V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor g₁ + f.tensor g₂).toLinearMap :
                  V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
a : A
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
⊢ (a • f).tensor g = a • f.tensor g
have h : ∀ (x : V) (x_1 : U),
  Eq (α := TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry ((a • f).tensor g).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
⊢ f.tensor (a • g) = a • f.tensor g
have h : ∀ (x : V) (x_1 : U),
  Eq (α := TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor (a • g)).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
⊢ lTensor ρ (id σ) = id (ρ.tprod σ)
have h : ∀ (x : V) (x_1 : W),
  Eq (α := TensorProduct A V W)
    (((((TensorProduct.AlgebraTensorModule.curry (lTensor ρ (id σ)).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A V W) :
                (a : V) → W →ₗ[A] TensorProduct A V W)
              x :
            W →ₗ[A] TensorProduct A V W) :
          (a : W) → TensorProduct A V W)
        x_1 :
      TensorProduct A V W)
    (((((TensorProduct.AlgebraTensorModule.curry (id (ρ.tprod σ)).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A V W) :
                (a : V) → W →ₗ[A] TensorProduct A V W)
              x :
            W →ₗ[A] TensorProduct A V W) :
          (a : W) → TensorProduct A V W)
        x_1 :
      TensorProduct A V W)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
⊢ Eq (α := (ρ.tprod σ).IntertwiningMap (ρ.tprod τ)) (lTensor ρ 0) 0
have h : ∀ (x : V) (x_1 : W),
  Eq (α := TensorProduct A V U)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (ρ := ρ.tprod σ) (σ := ρ.tprod τ) (lTensor ρ 0)) :
                  V →ₗ[A] W →ₗ[A] TensorProduct A V U) :
                (a : V) → W →ₗ[A] TensorProduct A V U)
              x :
            W →ₗ[A] TensorProduct A V U) :
          (a : W) → TensorProduct A V U)
        x_1 :
      TensorProduct A V U)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (G := G) (ρ := ρ.tprod σ) (σ := ρ.tprod τ) 0) :
                  V →ₗ[A] W →ₗ[A] TensorProduct A V U) :
                (a : V) → W →ₗ[A] TensorProduct A V U)
              x :
            W →ₗ[A] TensorProduct A V U) :
          (a : W) → TensorProduct A V U)
        x_1 :
      TensorProduct A V U)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
⊢ rTensor ρ (id σ) = id (σ.tprod ρ)
have h : ∀ (x : W) (x_1 : V),
  Eq (α := TensorProduct A W V)
    (((((TensorProduct.AlgebraTensorModule.curry (rTensor ρ (id σ)).toLinearMap : W →ₗ[A] V →ₗ[A] TensorProduct A W V) :
                (a : W) → V →ₗ[A] TensorProduct A W V)
              x :
            V →ₗ[A] TensorProduct A W V) :
          (a : V) → TensorProduct A W V)
        x_1 :
      TensorProduct A W V)
    (((((TensorProduct.AlgebraTensorModule.curry (id (σ.tprod ρ)).toLinearMap : W →ₗ[A] V →ₗ[A] TensorProduct A W V) :
                (a : W) → V →ₗ[A] TensorProduct A W V)
              x :
            V →ₗ[A] TensorProduct A W V) :
          (a : V) → TensorProduct A W V)
        x_1 :
      TensorProduct A W V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
⊢ Eq (α := (σ.tprod ρ).IntertwiningMap (τ.tprod ρ)) (rTensor ρ 0) 0
have h : ∀ (x : W) (x_1 : V),
  Eq (α := TensorProduct A U V)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (ρ := σ.tprod ρ) (σ := τ.tprod ρ) (rTensor ρ 0)) :
                  W →ₗ[A] V →ₗ[A] TensorProduct A U V) :
                (a : W) → V →ₗ[A] TensorProduct A U V)
              x :
            V →ₗ[A] TensorProduct A U V) :
          (a : V) → TensorProduct A U V)
        x_1 :
      TensorProduct A U V)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (G := G) (ρ := σ.tprod ρ) (σ := τ.tprod ρ) 0) :
                  W →ₗ[A] V →ₗ[A] TensorProduct A U V) :
                (a : W) → V →ₗ[A] TensorProduct A U V)
              x :
            V →ₗ[A] TensorProduct A U V) :
          (a : V) → TensorProduct A U V)
        x_1 :
      TensorProduct A U V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst_8 : AddCommMonoid Q
inst_9 : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
⊢ (rTensor υ f).comp (lTensor ρ g) = f.tensor g
have h : ∀ (x : V) (x_1 : W),
  Eq (α := TensorProduct A U Q)
    (((((TensorProduct.AlgebraTensorModule.curry ((rTensor υ f).comp (lTensor ρ g)).toLinearMap :
                  V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                (a : V) → W →ₗ[A] TensorProduct A U Q)
              x :
            W →ₗ[A] TensorProduct A U Q) :
          (a : W) → TensorProduct A U Q)
        x_1 :
      TensorProduct A U Q)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                (a : V) → W →ₗ[A] TensorProduct A U Q)
              x :
            W →ₗ[A] TensorProduct A U Q) :
          (a : W) → TensorProduct A U Q)
        x_1 :
      TensorProduct A U Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst_8 : AddCommMonoid Q
inst_9 : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
⊢ (lTensor τ g).comp (rTensor σ f) = f.tensor g
have h : ∀ (x : V) (x_1 : W),
  Eq (α := TensorProduct A U Q)
    (((((TensorProduct.AlgebraTensorModule.curry ((lTensor τ g).comp (rTensor σ f)).toLinearMap :
                  V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                (a : V) → W →ₗ[A] TensorProduct A U Q)
              x :
            W →ₗ[A] TensorProduct A U Q) :
          (a : W) → TensorProduct A U Q)
        x_1 :
      TensorProduct A U Q)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                (a : V) → W →ₗ[A] TensorProduct A U Q)
              x :
            W →ₗ[A] TensorProduct A U Q) :
          (a : W) → TensorProduct A U Q)
        x_1 :
      TensorProduct A U Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
⊢ Eq (α := TensorProduct A V W →ₗ[A] TensorProduct A W V)
    ((↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V) ∘ₗ
      (ρ.tprod σ : (a : G) → TensorProduct A V W →ₗ[A] TensorProduct A V W) g)
    ((σ.tprod ρ : (a : G) → TensorProduct A W V →ₗ[A] TensorProduct A W V) g ∘ₗ
      (↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V))
have a : ∀ (x : V) (x_1 : W),
  Eq (α := TensorProduct A W V)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V) ∘ₗ
                      (ρ.tprod σ : (a : G) → TensorProduct A V W →ₗ[A] TensorProduct A V W) g) :
                  V →ₗ[A] W →ₗ[A] TensorProduct A W V) :
                (a : V) → W →ₗ[A] TensorProduct A W V)
              x :
            W →ₗ[A] TensorProduct A W V) :
          (a : W) → TensorProduct A W V)
        x_1 :
      TensorProduct A W V)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((σ.tprod ρ : (a : G) → TensorProduct A W V →ₗ[A] TensorProduct A W V) g ∘ₗ
                      (↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V)) :
                  V →ₗ[A] W →ₗ[A] TensorProduct A W V) :
                (a : V) → W →ₗ[A] TensorProduct A W V)
              x :
            W →ₗ[A] TensorProduct A W V) :
          (a : W) → TensorProduct A W V)
        x_1 :
      TensorProduct A W V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
⊢ (↑(comm ρ τ) : (ρ.tprod τ).IntertwiningMap (τ.tprod ρ)).comp (IntertwiningMap.lTensor ρ f) =
    (IntertwiningMap.rTensor ρ f).comp (↑(comm ρ σ) : (ρ.tprod σ).IntertwiningMap (σ.tprod ρ))
have h : ∀ (x : V) (x_1 : W),
  Eq (α := TensorProduct A U V)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((↑(comm ρ τ) : (ρ.tprod τ).IntertwiningMap (τ.tprod ρ)).comp
                        (IntertwiningMap.lTensor ρ f)).toLinearMap :
                  V →ₗ[A] W →ₗ[A] TensorProduct A U V) :
                (a : V) → W →ₗ[A] TensorProduct A U V)
              x :
            W →ₗ[A] TensorProduct A U V) :
          (a : W) → TensorProduct A U V)
        x_1 :
      TensorProduct A U V)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((IntertwiningMap.rTensor ρ f).comp
                        (↑(comm ρ σ) : (ρ.tprod σ).IntertwiningMap (σ.tprod ρ))).toLinearMap :
                  V →ₗ[A] W →ₗ[A] TensorProduct A U V) :
                (a : V) → W →ₗ[A] TensorProduct A U V)
              x :
            W →ₗ[A] TensorProduct A U V) :
          (a : W) → TensorProduct A U V)
        x_1 :
      TensorProduct A U V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
⊢ (↑(comm τ ρ) : (τ.tprod ρ).IntertwiningMap (ρ.tprod τ)).comp (IntertwiningMap.rTensor ρ f) =
    (IntertwiningMap.lTensor ρ f).comp (↑(comm σ ρ) : (σ.tprod ρ).IntertwiningMap (ρ.tprod σ))
have h : ∀ (x : W) (x_1 : V),
  Eq (α := TensorProduct A V U)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((↑(comm τ ρ) : (τ.tprod ρ).IntertwiningMap (ρ.tprod τ)).comp
                        (IntertwiningMap.rTensor ρ f)).toLinearMap :
                  W →ₗ[A] V →ₗ[A] TensorProduct A V U) :
                (a : W) → V →ₗ[A] TensorProduct A V U)
              x :
            V →ₗ[A] TensorProduct A V U) :
          (a : V) → TensorProduct A V U)
        x_1 :
      TensorProduct A V U)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((IntertwiningMap.lTensor ρ f).comp
                        (↑(comm σ ρ) : (σ.tprod ρ).IntertwiningMap (ρ.tprod σ))).toLinearMap :
                  W →ₗ[A] V →ₗ[A] TensorProduct A V U) :
                (a : W) → V →ₗ[A] TensorProduct A V U)
              x :
            V →ₗ[A] TensorProduct A V U) :
          (a : V) → TensorProduct A V U)
        x_1 :
      TensorProduct A V U)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
⊢ Eq (α := TensorProduct A W A →ₗ[A] W)
    ((↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W) ∘ₗ
      (σ.tprod (trivial A G A) : (a : G) → TensorProduct A W A →ₗ[A] TensorProduct A W A) g)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W))
have a : ∀ (x : W),
  Eq.{u_4 + 1} (α := W)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W) ∘ₗ
                      (σ.tprod (trivial A G A) : (a : G) → TensorProduct A W A →ₗ[A] TensorProduct A W A) g) :
                  W →ₗ[A] A →ₗ[A] W) :
                (a : W) → A →ₗ[A] W)
              x :
            A →ₗ[A] W) :
          (a : A) → W)
        1 :
      W)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.rid A W) : TensorProduct A W A →ₗ[A] W)) :
                  W →ₗ[A] A →ₗ[A] W) :
                (a : W) → A →ₗ[A] W)
              x :
            A →ₗ[A] W) :
          (a : A) → W)
        1 :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
⊢ Eq (α := TensorProduct A A W →ₗ[A] W)
    ((↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W) ∘ₗ
      (tprod (trivial A G A) σ : (a : G) → TensorProduct A A W →ₗ[A] TensorProduct A A W) g)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W))
have a : ∀ (x : W),
  Eq (α := W)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W) ∘ₗ
                    (tprod (trivial A G A) σ : (a : G) → TensorProduct A A W →ₗ[A] TensorProduct A A W) g) :
                LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id A) A (W →ₗ[A] W)) :
              (a : A) → W →ₗ[A] W)
            1 :
          (a : W) → W)
        x :
      W)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑(_root_.TensorProduct.lid A W) : TensorProduct A A W →ₗ[A] W)) :
                LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id A) A (W →ₗ[A] W)) :
              (a : A) → W →ₗ[A] W)
            1 :
          (a : W) → W)
        x :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G_1
inst_2 : AddCommMonoid V_1
inst_3 : AddCommMonoid W_1
inst_4 : AddCommMonoid U
inst_5 : Module A V_1
inst_6 : Module A W_1
inst_7 : Module A U
ρ_1 : Representation A G_1 V_1
σ_1 : Representation A G_1 W_1
τ : Representation A G_1 U
f : V_1 →ₗ[A] W_1
G : Type u_6
k : Type u_7
V : Type u_8
W : Type u_9
inst_8 : Group G
inst_9 : Field k
inst_10 : AddCommGroup V
inst_11 : Module k V
inst_12 : AddCommGroup W
inst_13 : Module k W
inst_14 : FiniteDimensional k V
inst_15 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
⊢ Eq (α := TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W)
    ((↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W) ∘ₗ
      (ρ.dual.tprod σ : (a : G) → TensorProduct k (Module.Dual k V) W →ₗ[k] TensorProduct k (Module.Dual k V) W) g)
    ((ρ.linHom σ : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ
      (↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W))
have a : ∀ (v' : Module.Dual k V) (w : W) (v : V),
  Eq.{u_9 + 1} (α := W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                          ((↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W) ∘ₗ
                            (ρ.dual.tprod σ :
                                (a : G) → TensorProduct k (Module.Dual k V) W →ₗ[k] TensorProduct k (Module.Dual k V) W)
                              g) :
                        Module.Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                      (a : Module.Dual k V) → W →ₗ[k] V →ₗ[k] W)
                    v' :
                  W →ₗ[k] V →ₗ[k] W) :
                (a : W) → V →ₗ[k] W)
              w :
            V →ₗ[k] W) :
          (a : V) → W)
        v :
      W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                          ((ρ.linHom σ : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ
                            (↑(dualTensorHomEquiv k V W) : TensorProduct k (Module.Dual k V) W →ₗ[k] V →ₗ[k] W)) :
                        Module.Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                      (a : Module.Dual k V) → W →ₗ[k] V →ₗ[k] W)
                    v' :
                  W →ₗ[k] V →ₗ[k] W) :
                (a : W) → V →ₗ[k] W)
              w :
            V →ₗ[k] W) :
          (a : V) → W)
        v :
      W)
Tactic: ext v' w v
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
⊢ HMul.hMul (α := k[G]) (Finsupp.single g 1) (average k G) = average k G
have simp : HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, single (g * x) 1) =
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, single x 1)
Tactic: simp only [mul_one, Finset.mul_sum, Algebra.mul_smul_comm, average, MonoidAlgebra.of_apply,
    MonoidAlgebra.single_mul_single]