Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
x✝ : H
⊢ TensorProduct.lift
        (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
          (TensorProduct.lift
            (((lift (↑A →ₗ[k] ↑B →ₗ[k] (A.ρ.tprod (MonoidHom.comp B.ρ φ)).Coinvariants) k H) fun g ↦
                (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
              ↑(MonoidAlgebra.coeffLinearEquiv k)))
          ⋯) ∘ₗ
      TensorProduct.map
        (Coinvariants.map (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
          (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
          { toLinearMap := LinearMap.rTensor (↑A) (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝⁻¹),
            isIntertwining' := ⋯ })
        (B.ρ x✝) =
    TensorProduct.lift
      (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (TensorProduct.lift
          (((lift (↑A →ₗ[k] ↑B →ₗ[k] (A.ρ.tprod (MonoidHom.comp B.ρ φ)).Coinvariants) k H) fun g ↦
              (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
            ↑(MonoidAlgebra.coeffLinearEquiv k)))
        ⋯)

Tactic:
ext

Goal state after:
k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
x✝³ x✝² : H
x✝¹ : ↑A
x✝ : ↑B
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.AlgebraTensorModule.curry
                  (TensorProduct.lift
                      (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                        (TensorProduct.lift
                          (((lift (↑A →ₗ[k] ↑B →ₗ[k] (A.ρ.tprod (MonoidHom.comp B.ρ φ)).Coinvariants) k H) fun g ↦
                              (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                            ↑(MonoidAlgebra.coeffLinearEquiv k)))
                        ⋯) ∘ₗ
                    TensorProduct.map
                      (Coinvariants.map (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                        (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                        {
                          toLinearMap :=
                            LinearMap.rTensor (↑A) (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝³⁻¹),
                          isIntertwining' := ⋯ })
                      (B.ρ x✝³)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.AlgebraTensorModule.curry
                  (TensorProduct.lift
                    (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                      (TensorProduct.lift
                        (((lift (↑A →ₗ[k] ↑B →ₗ[k] (A.ρ.tprod (MonoidHom.comp B.ρ φ)).Coinvariants) k H) fun g ↦
                            (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                          ↑(MonoidAlgebra.coeffLinearEquiv k)))
                      ⋯)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝