-- 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
hf :
  ∀ (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)))
⊢ (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' := ⋯ } :
          of (Representation.ind φ A.ρ) ⟶ of B.ρ))
      ((fun (f : ind φ A ⟶ B) ↦
          (ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ } :
            of A.ρ ⟶ of (MonoidHom.comp B.ρ φ)))
        f) =
    f

Tactic:
ext h a