-- 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 : A ⟶ res φ B
g : G
a : H
x : (↑A : Type (max (max u v') w))
⊢ Eq (α := (↑B : Type (max (max u v') w)))
    (((LinearMap.compl₂ (R₂ := k) (N := (↑A : Type (max (max u v') w))) (σ₂₃ := RingHom.id k) (σ₄₂ := RingHom.id k)
                  (((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) ∘ₗ
                    (Representation.leftRegular k H : (a : H) → (H →₀ k) →ₗ[k] H →₀ k) ((φ : (a : G) → H) g))
                  ((A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g) ∘ₗ
                lsingle a :
              (a : k) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
            1 :
          (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        x :
      (↑B : Type (max (max u v') w)))
    (((((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) ∘ₗ
                lsingle a :
              (a : k) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
            1 :
          (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        x :
      (↑B : Type (max (max u v') w)))
have 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)))
        ((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: simp only [LinearMap.coe_comp, Function.comp_apply, lsingle_apply, LinearMap.compl₂_apply,
        ofMulAction_single, smul_eq_mul, lift_apply, mul_inv_rev, map_mul, zero_smul,
        sum_single_index, one_smul, IntertwiningMap.toLinearMap_apply, Module.End.mul_apply]