Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
g x✝¹ : G
x✝ a✝¹ : α
a✝ : G
⊢ ((((TensorProduct.AlgebraTensorModule.curry
                    (↑(TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (MonoidAlgebra.coeffLinearEquiv k) ≪≫ₗ
                                finsuppTensorFinsupp' k G α ≪≫ₗ
                              Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                            curryLinearEquiv k ≪≫ₗ
                          mapRange.linearEquiv (MonoidAlgebra.coeffLinearEquiv k).symm) ∘ₗ
                      ((leftRegular k G).tprod (trivial k G k[α])) g) ∘ₗ
                  MonoidAlgebra.lsingle x✝¹)
                1 ∘ₗ
              MonoidAlgebra.lsingle x✝)
            1)
          a✝¹).coeff
      a✝ =
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((free k G α) g ∘ₗ
                      ↑(TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (MonoidAlgebra.coeffLinearEquiv k) ≪≫ₗ
                                finsuppTensorFinsupp' k G α ≪≫ₗ
                              Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                            curryLinearEquiv k ≪≫ₗ
                          mapRange.linearEquiv (MonoidAlgebra.coeffLinearEquiv k).symm)) ∘ₗ
                  MonoidAlgebra.lsingle x✝¹)
                1 ∘ₗ
              MonoidAlgebra.lsingle x✝)
            1)
          a✝¹).coeff
      a✝

Tactic:
;

Goal state after:
k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
g x✝¹ : G
x✝ a✝¹ : α
a✝ : G
⊢ ((((TensorProduct.AlgebraTensorModule.curry
                    (↑(TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (MonoidAlgebra.coeffLinearEquiv k) ≪≫ₗ
                                finsuppTensorFinsupp' k G α ≪≫ₗ
                              Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                            curryLinearEquiv k ≪≫ₗ
                          mapRange.linearEquiv (MonoidAlgebra.coeffLinearEquiv k).symm) ∘ₗ
                      ((leftRegular k G).tprod (trivial k G k[α])) g) ∘ₗ
                  MonoidAlgebra.lsingle x✝¹)
                1 ∘ₗ
              MonoidAlgebra.lsingle x✝)
            1)
          a✝¹).coeff
      a✝ =
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((free k G α) g ∘ₗ
                      ↑(TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (MonoidAlgebra.coeffLinearEquiv k) ≪≫ₗ
                                finsuppTensorFinsupp' k G α ≪≫ₗ
                              Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                            curryLinearEquiv k ≪≫ₗ
                          mapRange.linearEquiv (MonoidAlgebra.coeffLinearEquiv k).symm)) ∘ₗ
                  MonoidAlgebra.lsingle x✝¹)
                1 ∘ₗ
              MonoidAlgebra.lsingle x✝)
            1)
          a✝¹).coeff
      a✝