awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
⊢ ∀ (g : G),
    Eq (α := TensorProduct k (H →₀ k) (↑A : Type u_1) →ₗ[k] TensorProduct k (H →₀ k) (↑B : Type u_1))
      (LinearMap.lTensor (H →₀ k) (Hom.hom f).toLinearMap ∘ₗ
        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ :
            (a : G) → TensorProduct k (H →₀ k) (↑A : Type u_1) →ₗ[k] TensorProduct k (H →₀ k) (↑A : Type u_1))
          g)
      ((Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ :
            (a : G) → TensorProduct k (H →₀ k) (↑B : Type u_1) →ₗ[k] TensorProduct k (H →₀ k) (↑B : Type u_1))
          g ∘ₗ
        LinearMap.lTensor (H →₀ k) (Hom.hom f).toLinearMap)

Tactic:
simp [LinearMap.lTensor_comp_map, f.hom.2, LinearMap.map_comp_lTensor]

Premises used: LinearMap.map_comp_lTensor, Representation.IntertwiningMap.isIntertwining', Rep.Hom.hom, LinearMap.lTensor_comp_map
-- 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
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
g : H
H₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := Representation.IndV φ A.ρ →ₗ[k] Representation.IndV φ B.ρ)
    (Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
        { toLinearMap := LinearMap.lTensor (H →₀ k) (Hom.hom f).toLinearMap, isIntertwining' := ⋯ } ∘ₗ
      (Representation.ind φ A.ρ : (a : H) → Representation.IndV φ A.ρ →ₗ[k] Representation.IndV φ A.ρ) g)
    ((Representation.ind φ B.ρ : (a : H) → Representation.IndV φ B.ρ →ₗ[k] Representation.IndV φ B.ρ) g ∘ₗ
      Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
        { toLinearMap := LinearMap.lTensor (H →₀ k) (Hom.hom f).toLinearMap, isIntertwining' := ⋯ })

Tactic:
ext
-- 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
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
g a : H
x : (↑A : Type u_1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- 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 x : Rep.{w, u, v} k G
hf :
  ∀ (a : H) (x_1 : (↑x : Type w)),
    Eq (α := (↑(ind φ x) : Type (max (max u v') w)))
      ((((TensorProduct.AlgebraTensorModule.curry
                      ((Hom.hom (indMap φ (𝟙 x))).toLinearMap ∘ₗ
                        Representation.Coinvariants.mk
                          (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x.ρ)) ∘ₗ
                    lsingle a :
                  k →ₗ[k] (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w))) :
                (a : k) → (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w)))
              1 :
            (a : (↑x : Type w)) → (↑(ind φ x) : Type (max (max u v') w)))
          x_1 :
        (↑(ind φ x) : Type (max (max u v') w)))
      ((((TensorProduct.AlgebraTensorModule.curry
                      ((Hom.hom (𝟙 (ind φ x))).toLinearMap ∘ₗ
                        Representation.Coinvariants.mk
                          (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x.ρ)) ∘ₗ
                    lsingle a :
                  k →ₗ[k] (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w))) :
                (a : k) → (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w)))
              1 :
            (a : (↑x : Type w)) → (↑(ind φ x) : Type (max (max u v') w)))
          x_1 :
        (↑(ind φ x) : Type (max (max u v') w)))
⊢ indMap φ (𝟙 x) = 𝟙 (ind φ x)

Tactic:
ext
-- 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 x : Rep.{w, u, v} k G
a : H
x_1 : (↑x : Type w)
⊢ Eq (α := (↑(ind φ x) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((Hom.hom (indMap φ (𝟙 x))).toLinearMap ∘ₗ
                      Representation.Coinvariants.mk
                        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x.ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k] (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w))) :
              (a : k) → (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w)))
            1 :
          (a : (↑x : Type w)) → (↑(ind φ x) : Type (max (max u v') w)))
        x_1 :
      (↑(ind φ x) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((Hom.hom (𝟙 (ind φ x))).toLinearMap ∘ₗ
                      Representation.Coinvariants.mk
                        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x.ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k] (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w))) :
              (a : k) → (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w)))
            1 :
          (a : (↑x : Type w)) → (↑(ind φ x) : Type (max (max u v') w)))
        x_1 :
      (↑(ind φ x) : Type (max (max u v') w)))

Tactic:
rfl
-- 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 X Y Z : Rep.{w, u, v} k G
x : X ⟶ Y
x_1 : Y ⟶ Z
hf :
  ∀ (a : H) (x_2 : (↑X : Type w)),
    Eq (α := (↑(ind φ Z) : Type (max (max u v') w)))
      ((((TensorProduct.AlgebraTensorModule.curry
                      ((Hom.hom (indMap φ (x ≫ x_1))).toLinearMap ∘ₗ
                        Representation.Coinvariants.mk
                          (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X.ρ)) ∘ₗ
                    lsingle a :
                  k →ₗ[k] (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w))) :
                (a : k) → (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w)))
              1 :
            (a : (↑X : Type w)) → (↑(ind φ Z) : Type (max (max u v') w)))
          x_2 :
        (↑(ind φ Z) : Type (max (max u v') w)))
      ((((TensorProduct.AlgebraTensorModule.curry
                      ((Hom.hom (indMap φ x ≫ indMap φ x_1)).toLinearMap ∘ₗ
                        Representation.Coinvariants.mk
                          (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X.ρ)) ∘ₗ
                    lsingle a :
                  k →ₗ[k] (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w))) :
                (a : k) → (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w)))
              1 :
            (a : (↑X : Type w)) → (↑(ind φ Z) : Type (max (max u v') w)))
          x_2 :
        (↑(ind φ Z) : Type (max (max u v') w)))
⊢ indMap φ (x ≫ x_1) = indMap φ x ≫ indMap φ x_1

Tactic:
ext
-- 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 X Y Z : Rep.{w, u, v} k G
x : X ⟶ Y
x_1 : Y ⟶ Z
a : H
x_2 : (↑X : Type w)
⊢ Eq (α := (↑(ind φ Z) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((Hom.hom (indMap φ (x ≫ x_1))).toLinearMap ∘ₗ
                      Representation.Coinvariants.mk
                        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X.ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k] (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w))) :
              (a : k) → (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w)))
            1 :
          (a : (↑X : Type w)) → (↑(ind φ Z) : Type (max (max u v') w)))
        x_2 :
      (↑(ind φ Z) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((Hom.hom (indMap φ x ≫ indMap φ x_1)).toLinearMap ∘ₗ
                      Representation.Coinvariants.mk
                        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X.ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k] (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w))) :
              (a : k) → (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w)))
            1 :
          (a : (↑X : Type w)) → (↑(ind φ Z) : Type (max (max u v') w)))
        x_2 :
      (↑(ind φ Z) : Type (max (max u v') w)))

Tactic:
rfl
-- 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 : ind φ A ⟶ B
g : G
h :
  ∀ (x : (↑A : Type (max (max u v') w))),
    Eq (α := (↑B : Type (max (max u v') w)))
      ((((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
              (A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g :
            (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
          x :
        (↑B : Type (max (max u v') w)))
      (((MonoidHom.comp B.ρ φ : (a : G) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) g ∘ₗ
              (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1 :
            (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
          x :
        (↑B : Type (max (max u v') w)))
⊢ ((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      (A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g =
    (MonoidHom.comp B.ρ φ : (a : G) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) g ∘ₗ
      (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1

Tactic:
ext x
-- 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 : ind φ A ⟶ B
g : G
x : (↑A : 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 : 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 : (↑(ind φ A) : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
          ((IndV.mk φ A.ρ 1 : (a : (↑A : Type (max (max u v') w))) → IndV φ A.ρ) x)) :
      (↑B : Type (max (max u v') w)))
    ((Hom.hom f : (a : (↑(ind φ A) : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        (((((ind φ A).ρ : (a : H) → (↑(ind φ A) : Type (max (max u v') w)) →ₗ[k] (↑(ind φ A) : Type (max (max u v') w)))
                ((φ : (a : G) → H) g) :
              (↑(ind φ A) : Type (max (max u v') w)) →ₗ[k] (↑(ind φ A) : Type (max (max u v') w))) :
            (a : (↑(ind φ A) : Type (max (max u v') w))) → (↑(ind φ A) : Type (max (max u v') w)))
          ((IndV.mk φ A.ρ 1 : (a : (↑A : Type (max (max u v') w))) → IndV φ A.ρ) x)) :
      (↑B : Type (max (max u v') w)))

Tactic:
have := (hom_comm_apply f (φ g) (IndV.mk φ A.ρ 1 x)).symm
-- 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 : ind φ A ⟶ B
g : G
x : (↑A : Type (max (max u v') w))
this :
  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 : 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 : (↑(ind φ A) : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
          ((IndV.mk φ A.ρ 1 : (a : (↑A : Type (max (max u v') w))) → IndV φ A.ρ) x)) :
      (↑B : Type (max (max u v') w)))
    ((Hom.hom f : (a : (↑(ind φ A) : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        (((((ind φ A).ρ : (a : H) → (↑(ind φ A) : Type (max (max u v') w)) →ₗ[k] (↑(ind φ A) : Type (max (max u v') w)))
                ((φ : (a : G) → H) g) :
              (↑(ind φ A) : Type (max (max u v') w)) →ₗ[k] (↑(ind φ A) : Type (max (max u v') w))) :
            (a : (↑(ind φ A) : Type (max (max u v') w))) → (↑(ind φ A) : Type (max (max u v') w)))
          ((IndV.mk φ A.ρ 1 : (a : (↑A : Type (max (max u v') w))) → IndV φ A.ρ) x)) :
      (↑B : Type (max (max u v') w)))
⊢ Eq (α := (↑B : Type (max (max u v') w)))
    ((((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
            (A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g :
          (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        x :
      (↑B : Type (max (max u v') w)))
    (((MonoidHom.comp B.ρ φ : (a : G) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) g ∘ₗ
            (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1 :
          (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_all [← Coinvariants.mk_inv_tmul]

Premises used: Representation.Coinvariants.mk_inv_tmul
-- 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
simp :
  Eq (α := TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
    (TensorProduct.lift
      (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)))
    (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))
⊢ Eq (α := TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
    (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) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ :
          (a : G) →
            TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)) →ₗ[k]
              TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)))
        g)
    (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))

Tactic:
simp only [res_obj_ρ, tprod_apply, MonoidHom.coe_comp, Function.comp_apply,
        TensorProduct.lift_comp_map]

Premises used: MonoidHom.coe_comp, Representation.tprod_apply, TensorProduct.lift_comp_map, Function.comp_apply, Rep.res_obj_ρ
-- 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' :
  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)
⊢ Eq (α := TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
    (TensorProduct.lift
      (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)))
    (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))

Tactic:
congr 1
-- 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))
⊢ 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)))

Tactic:
simp
-- 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 : H
H₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := IndV φ A.ρ →ₗ[k] (↑B : Type (max (max u v') w)))
    (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))
        ⋯ ∘ₗ
      (Representation.ind φ A.ρ : (a : H) → IndV φ A.ρ →ₗ[k] IndV φ A.ρ) g)
    ((B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) g ∘ₗ
      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))
        ⋯)

Tactic:
ext
-- 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 a : H
x : (↑A : Type (max (max u v') w))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp