-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G : Type v
H : Type v'
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A_1 : Rep.{w, u, v} k G
B_1 : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
h : H
a : (↑A : Type (max (max u v') w))
⊢ Eq (α := (↑(of B.ρ) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((IntertwiningMap.toLinearMap
                          (Hom.hom
                            ((fun (f : A ⟶ res φ B) ↦
                                (ofHom
                                    {
                                      toLinearMap :=
                                        Coinvariants.lift
                                          (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                                          (TensorProduct.lift
                                            ((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
                                                  k H :
                                                (a :
                                                    H →
                                                      (↑A : Type (max (max u v') w)) →ₗ[k]
                                                        (↑B : Type (max (max u v') w))) →
                                                  (H →₀ k) →ₗ[k]
                                                    (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
                                              fun (h : H) ↦
                                              (B.ρ :
                                                    (a : H) →
                                                      (↑B : Type (max (max u v') w)) →ₗ[k]
                                                        (↑B : Type (max (max u v') w)))
                                                  h⁻¹ ∘ₗ
                                                (Hom.hom f).toLinearMap))
                                          ⋯,
                                      isIntertwining' := ⋯ : (Representation.ind φ A.ρ).IntertwiningMap B.ρ } :
                                  of (Representation.ind φ A.ρ) ⟶ of B.ρ))
                              ((fun (f : ind φ A ⟶ B) ↦
                                  (ofHom
                                      { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1,
                                        isIntertwining' := ⋯ : A.ρ.IntertwiningMap (MonoidHom.comp B.ρ φ) } :
                                    of A.ρ ⟶ of (MonoidHom.comp B.ρ φ)))
                                f))) :
                        (↑(of (Representation.ind φ A.ρ)) : Type (max (max u v') w)) →ₗ[k]
                          (↑(of B.ρ) : Type (max (max u v') w))) ∘ₗ
                      Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                  lsingle h :
                k →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑(of B.ρ) : Type (max (max u v') w))) :
              (a : k) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑(of B.ρ) : Type (max (max u v') w)))
            1 :
          (a : (↑A : Type (max (max u v') w))) → (↑(of B.ρ) : Type (max (max u v') w)))
        a :
      (↑(of B.ρ) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((Hom.hom f).toLinearMap ∘ₗ
                      Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                  lsingle h :
                k →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑(of B.ρ) : Type (max (max u v') w))) :
              (a : k) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑(of B.ρ) : Type (max (max u v') w)))
            1 :
          (a : (↑A : Type (max (max u v') w))) → (↑(of B.ρ) : Type (max (max u v') w)))
        a :
      (↑(of B.ρ) : Type (max (max u v') w)))

Tactic:
simpa using (hom_comm_apply f h⁻¹ (IndV.mk φ A.ρ 1 a)).symm

Premises used: Representation.IndV.mk, Inv.inv, Rep.ρ, Rep.hom_comm_apply, OfNat.ofNat, Eq.symm, DFunLike.coe