-- 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
e_f' :
  ∀ (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)))
⊢ Eq (α := (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑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))
    ((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)

Tactic:
ext