-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
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
⊢ (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
have 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' := sorry :
                        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))
                              sorry,
                          isIntertwining' := sorry : (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)))
Tactic: ext