-- 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 : A ⟶ res φ B
g : G
a : H
x : (↑A : Type (max (max u v') w))
e_f' :
  Eq (α := (↑B : Type (max (max u v') w)))
    ((((B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) a⁻¹ :
            (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) :
          (a : (↑B : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        ((((B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
                ((φ : (a : G) → H) g)⁻¹ :
              (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) :
            (a : (↑B : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
          (((((res φ B).ρ :
                    (a : G) → (↑(res φ B) : Type (max (max u v') w)) →ₗ[k] (↑(res φ B) : Type (max (max u v') w)))
                  g :
                (↑(res φ B) : Type (max (max u v') w)) →ₗ[k] (↑(res φ B) : Type (max (max u v') w))) :
              (a : (↑(res φ B) : Type (max (max u v') w))) → (↑(res φ B) : Type (max (max u v') w)))
            ((Hom.hom f : (a : (↑A : Type (max (max u v') w))) → (↑(res φ B) : Type (max (max u v') w))) x))) :
      (↑B : Type (max (max u v') w)))
    ((((B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) a⁻¹ :
            (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) :
          (a : (↑B : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        ((Hom.hom f : (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w))) x) :
      (↑B : Type (max (max u v') w)))
⊢ Eq (α := (↑B : Type (max (max u v') w)))
    ((((B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) a⁻¹ :
            (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) :
          (a : (↑B : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        ((((B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
                ((φ : (a : G) → H) g)⁻¹ :
              (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) :
            (a : (↑B : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
          ((Hom.hom f : (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
            ((((A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g :
                  (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) :
                (a : (↑A : Type (max (max u v') w))) → (↑A : Type (max (max u v') w)))
              x))) :
      (↑B : Type (max (max u v') w)))
    ((((B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) a⁻¹ :
            (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) :
          (a : (↑B : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        ((Hom.hom f : (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w))) x) :
      (↑B : Type (max (max u v') w)))

Tactic:
rw [hom_comm_apply f g _]

Premises used: Rep.hom_comm_apply