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