-- 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
x : A ⟶ res φ B
hf :
  ∀ (x_1 : (↑(of A.ρ) : Type (max (max u v') w))),
    Eq (α := (↑(of (MonoidHom.comp B.ρ φ)) : Type (max (max u v') w)))
      ((IntertwiningMap.toLinearMap
              (Hom.hom
                ((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.ρ φ)))
                  ((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.ρ))
                    x))) :
            (a : (↑(of A.ρ) : Type (max (max u v') w))) → (↑(of (MonoidHom.comp B.ρ φ)) : Type (max (max u v') w)))
          x_1 :
        (↑(of (MonoidHom.comp B.ρ φ)) : Type (max (max u v') w)))
      (((Hom.hom x).toLinearMap :
            (a : (↑(of A.ρ) : Type (max (max u v') w))) → (↑(of (MonoidHom.comp B.ρ φ)) : Type (max (max u v') w)))
          x_1 :
        (↑(of (MonoidHom.comp B.ρ φ)) : Type (max (max u v') w)))
⊢ (fun (f : ind φ A ⟶ B) ↦
        (ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ } :
          of A.ρ ⟶ of (MonoidHom.comp B.ρ φ)))
      ((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.ρ))
        x) =
    x

Tactic:
ext