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✝³ 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✝

Tactic:
;

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✝