Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
x✝³ x✝² x✝¹ : H
x✝ : A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * (x✝³ * x✝²)⁻¹),
                  isIntertwining' := ⋯ } ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝³⁻¹),
                    isIntertwining' := ⋯ } *
                Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝²⁻¹),
                    isIntertwining' := ⋯ }) ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
x✝³ x✝² x✝¹ : H
x✝ : A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * (x✝³ * x✝²)⁻¹),
                  isIntertwining' := ⋯ } ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝³⁻¹),
                    isIntertwining' := ⋯ } *
                Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝²⁻¹),
                    isIntertwining' := ⋯ }) ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝