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
B_1 : Rep k H
A : Rep k G
B : Rep k H
x : A ⟶ res φ B
x_1 : (↑(of A.ρ) : Type (max (max u v') w))
⊢ Eq (α := (↑(of (MonoidHom.comp B.ρ φ)) : Type (max (max u v') w)))
    ((IntertwiningMap.toLinearMap
            (Hom.hom
              ((fun (f : ind φ A ⟶ B) ↦
                  (ofHom
                      { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ :
                        A.ρ.IntertwiningMap (MonoidHom.comp B.ρ φ) } :
                    of A.ρ ⟶ of (MonoidHom.comp 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' := ⋯ : (Representation.ind φ A.ρ).IntertwiningMap B.ρ } :
                      of (Representation.ind φ A.ρ) ⟶ of B.ρ))
                  x))) :
          (a : (↑(of A.ρ) : Type (max (max u v') w))) → (↑(of (MonoidHom.comp B.ρ φ)) : Type (max (max u v') w)))
        x_1 :
      (↑(of (MonoidHom.comp B.ρ φ)) : Type (max (max u v') w)))
    (((Hom.hom x).toLinearMap :
          (a : (↑(of A.ρ) : Type (max (max u v') w))) → (↑(of (MonoidHom.comp B.ρ φ)) : Type (max (max u v') w)))
        x_1 :
      (↑(of (MonoidHom.comp 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 : Rep.{w, u, v} k G
B : Rep k H
⊢ Functor.IsLeftAdjoint (C := Rep k G) (indFunctor k φ)

Tactic:
(indResAdjunction k φ).isLeftAdjoint

Premises used: Rep.indResAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- 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 : Rep.{w, u, v} k G
B : Rep k H
⊢ Functor.IsRightAdjoint (C := Rep k G) (resFunctor φ)

Tactic:
(indResAdjunction k φ).isRightAdjoint

Premises used: Rep.indResAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
x : H
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
x a : H
x_1 : (↑A : Type u)
x_2 : (↑B : Type u)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
inst : CommRing k
G H : Type u
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
x : (↑A : Type u)
y : (↑B : Type u)
⊢ Eq (α := (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (coinvariantsTensorIndHom φ A B) :
          (a : (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u)) →
            (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
        (((((ind φ A).coinvariantsTensorMk B :
                  (a : (↑(ind φ A) : Type u)) →
                    (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
                ((IndV.mk φ A.ρ h : (a : (↑A : Type u)) → IndV φ A.ρ) x) :
              (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
            (a : (↑B : Type u)) → (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
          y) :
      (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u))
    ((((A.coinvariantsTensorMk (res φ B) :
                (a : (↑A : Type u)) →
                  (↑(res φ B) : Type u) →ₗ[k] (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
              x :
            (↑(res φ B) : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u)) :
          (a : (↑(res φ B) : Type u)) → (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
        ((((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) h : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
            (a : (↑B : Type u)) → (↑B : Type u))
          y) :
      (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u))

Tactic:
simp [coinvariantsTensorIndHom, coinvariantsTensorMk]

Premises used: Rep.coinvariantsTensorMk, Rep.coinvariantsTensorIndHom
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
simp :
  TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      TensorProduct.map ((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s)
        ((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((φ : (a : G) → H) s)) =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)
⊢ TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      ((Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ :
          (a : G) →
            (↑(((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)) : Type u) →ₗ[k]
              (↑(((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)) : Type u))
        s =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)

Tactic:
simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V, tensor_ρ, tprod_apply,
      MonoidHom.coe_comp, Function.comp_apply]

Premises used: MonoidHom.coe_comp, Representation.tprod_apply, Rep.tensor_ρ, CategoryTheory.MonoidalCategory.curriedTensor_obj_obj, Function.comp_apply, Rep.tensor_V
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
a :
  ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
    Eq (α := ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
      (((((TensorProduct.AlgebraTensorModule.curry
                      (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
                        TensorProduct.map ((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s)
                          ((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((φ : (a : G) → H) s))) :
                    (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
                  (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
                x :
              (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
            (a : (↑B : Type u)) → ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
          y :
        ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
      (((((TensorProduct.AlgebraTensorModule.curry
                      (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)) :
                    (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
                  (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
                x :
              (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
            (a : (↑B : Type u)) → ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
          y :
        ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
⊢ TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      TensorProduct.map ((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s)
        ((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((φ : (a : G) → H) s)) =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)

Tactic:
ext x y
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
x : (↑A : Type u)
y : (↑B : Type u)
⊢ HSub.hSub (α := TensorProduct k (IndV φ A.ρ) (↑B : Type u)) (β := TensorProduct k (IndV φ A.ρ) (↑B : Type u))
      (((((Representation.ind φ A.ρ).tprod B.ρ :
                  (a : H) → TensorProduct k (IndV φ A.ρ) (↑B : Type u) →ₗ[k] TensorProduct k (IndV φ A.ρ) (↑B : Type u))
                ((φ : (a : G) → H) s) :
              TensorProduct k (IndV φ A.ρ) (↑B : Type u) →ₗ[k] TensorProduct k (IndV φ A.ρ) (↑B : Type u)) :
            (a : TensorProduct k (IndV φ A.ρ) (↑B : Type u)) → TensorProduct k (IndV φ A.ρ) (↑B : Type u))
          ((IndV.mk φ A.ρ 1 : (a : (↑A : Type u)) → IndV φ A.ρ) x ⊗ₜ[k] y) :
        TensorProduct k (IndV φ A.ρ) (↑B : Type u))
      ((IndV.mk φ A.ρ 1 : (a : (↑A : Type u)) → IndV φ A.ρ) x ⊗ₜ[k] y : TensorProduct k (IndV φ A.ρ) (↑B : Type u)) =
    HSub.hSub (α := TensorProduct k (IndV φ A.ρ) (↑B : Type u)) (β := TensorProduct k (IndV φ A.ρ) (↑B : Type u))
      ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) :
              (a : TensorProduct k (H →₀ k) (↑A : Type u)) → IndV φ A.ρ)
            (single 1 1 ⊗ₜ[k]
              (((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                x) ⊗ₜ[k]
          (((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((φ : (a : G) → H) s) :
                (↑B : Type u) →ₗ[k] (↑B : Type u)) :
              (a : (↑B : Type u)) → (↑B : Type u))
            y :
        TensorProduct k (IndV φ A.ρ) (↑B : Type u))
      ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) :
              (a : TensorProduct k (H →₀ k) (↑A : Type u)) → IndV φ A.ρ)
            (single 1 1 ⊗ₜ[k] x) ⊗ₜ[k]
          y :
        TensorProduct k (IndV φ A.ρ) (↑B : Type u))

Tactic:
simp [← Coinvariants.mk_inv_tmul]

Premises used: Representation.Coinvariants.mk_inv_tmul
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
x : (↑A : Type u)
y : (↑B : Type u)
⊢ Eq (α := ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
                      TensorProduct.map ((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s)
                        ((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((φ : (a : G) → H) s))) :
                  (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
                (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
              x :
            (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
          (a : (↑B : Type u)) → ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
        y :
      ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)) :
                  (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
                (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
              x :
            (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
          (a : (↑B : Type u)) → ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
        y :
      ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)

Tactic:
simpa [Coinvariants.mk_eq_iff, coinvariantsTensorMk] using
      Coinvariants.mem_ker_of_eq (φ s) (IndV.mk φ A.ρ (1 : H) x ⊗ₜ[k] y) _ <| by
      simp [← Coinvariants.mk_inv_tmul]

Premises used: Representation.IndV.mk, Representation.Coinvariants.mk_eq_iff, Rep.ρ, Representation.Coinvariants.mem_ker_of_eq, TensorProduct.tmul, OfNat.ofNat, Rep.coinvariantsTensorMk, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
inst : CommRing k
G H : Type u
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
x : (↑A : Type u)
y : (↑B : Type u)
⊢ Eq (α := (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (coinvariantsTensorIndInv φ A B) :
          (a : (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u)) →
            (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
        ((Coinvariants.mk (A.ρ.tprod (res φ B).ρ) :
            (a : TensorProduct k (↑A : Type u) (↑(res φ B) : Type u)) → (A.ρ.tprod (res φ B).ρ).Coinvariants)
          (x ⊗ₜ[k] y)) :
      (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
    (((((ind φ A).coinvariantsTensorMk B :
                (a : (↑(ind φ A) : Type u)) →
                  (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
              ((IndV.mk φ A.ρ 1 : (a : (↑A : Type u)) → IndV φ A.ρ) x) :
            (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
          (a : (↑B : Type u)) → (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
        y :
      (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))

Tactic:
simp [coinvariantsTensorIndInv, coinvariantsTensorMk]

Premises used: Rep.coinvariantsTensorIndInv, Rep.coinvariantsTensorMk
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
hfg :
  ∀ (h : H) (a : (↑A : Type u)) (b : (↑B : Type u)),
    Eq (α := (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
      ((((((TensorProduct.AlgebraTensorModule.curry
                            (((ind φ A).coinvariantsTensorMk B).compr₂
                                (ModuleCat.Hom.hom (coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B)) ∘ₗ
                              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                          lsingle h :
                        k →ₗ[k]
                          (↑A : Type u) →ₗ[k]
                            (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
                      (a : k) →
                        (↑A : Type u) →ₗ[k]
                          (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
                    1 :
                  (a : (↑A : Type u)) →
                    (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
                a :
              (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
            (a : (↑B : Type u)) → (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
          b :
        (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
      ((((((TensorProduct.AlgebraTensorModule.curry
                            (((ind φ A).coinvariantsTensorMk B).compr₂
                                (ModuleCat.Hom.hom (𝟙 ((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B))) ∘ₗ
                              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                          lsingle h :
                        k →ₗ[k]
                          (↑A : Type u) →ₗ[k]
                            (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
                      (a : k) →
                        (↑A : Type u) →ₗ[k]
                          (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
                    1 :
                  (a : (↑A : Type u)) →
                    (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
                a :
              (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
            (a : (↑B : Type u)) → (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
          b :
        (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
⊢ coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B =
    𝟙 ((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B)

Tactic:
ext h a b
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
a : (↑A : Type u)
b : (↑B : Type u)
⊢ HSub.hSub (α := TensorProduct k (IndV φ A.ρ) (↑B : Type u)) (β := TensorProduct k (IndV φ A.ρ) (↑B : Type u))
      (((((Representation.ind φ A.ρ).tprod B.ρ :
                  (a : H) → TensorProduct k (IndV φ A.ρ) (↑B : Type u) →ₗ[k] TensorProduct k (IndV φ A.ρ) (↑B : Type u))
                h :
              TensorProduct k (IndV φ A.ρ) (↑B : Type u) →ₗ[k] TensorProduct k (IndV φ A.ρ) (↑B : Type u)) :
            (a : TensorProduct k (IndV φ A.ρ) (↑B : Type u)) → TensorProduct k (IndV φ A.ρ) (↑B : Type u))
          ((IndV.mk φ A.ρ h : (a : (↑A : Type u)) → IndV φ A.ρ) a ⊗ₜ[k] b) :
        TensorProduct k (IndV φ A.ρ) (↑B : Type u))
      ((IndV.mk φ A.ρ h : (a : (↑A : Type u)) → IndV φ A.ρ) a ⊗ₜ[k] b : TensorProduct k (IndV φ A.ρ) (↑B : Type u)) =
    HSub.hSub (α := TensorProduct k (IndV φ A.ρ) (↑B : Type u)) (β := TensorProduct k (IndV φ A.ρ) (↑B : Type u))
      ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) :
              (a : TensorProduct k (H →₀ k) (↑A : Type u)) → IndV φ A.ρ)
            (single 1 1 ⊗ₜ[k] a) ⊗ₜ[k]
          (((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) h : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
              (a : (↑B : Type u)) → (↑B : Type u))
            b :
        TensorProduct k (IndV φ A.ρ) (↑B : Type u))
      ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) :
              (a : TensorProduct k (H →₀ k) (↑A : Type u)) →
                (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ).Coinvariants)
            (single h 1 ⊗ₜ[k] a) ⊗ₜ[k]
          b :
        TensorProduct k
          ((tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ).Coinvariants (k := k) (G := G) (V :=
            TensorProduct k (H →₀ k) (↑A : Type u)))
          (↑B : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
hfg :
  ∀ (x : (↑A : Type u)) (x_1 : (↑(res φ B) : Type u)),
    Eq (α := (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u))
      ((((LinearMap.compr₂ (A.coinvariantsTensorMk (res φ B))
                    (ModuleCat.Hom.hom (coinvariantsTensorIndInv φ A B ≫ coinvariantsTensorIndHom φ A B)) :
                  (a : (↑A : Type u)) →
                    (↑(res φ B) : Type u) →ₗ[k] (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
                x :
              (↑(res φ B) : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u)) :
            (a : (↑(res φ B) : Type u)) → (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
          x_1 :
        (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u))
      ((((LinearMap.compr₂ (A.coinvariantsTensorMk (res φ B))
                    (ModuleCat.Hom.hom (𝟙 ((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)))) :
                  (a : (↑A : Type u)) →
                    (↑(res φ B) : Type u) →ₗ[k] (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
                x :
              (↑(res φ B) : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u)) :
            (a : (↑(res φ B) : Type u)) → (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
          x_1 :
        (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u))
⊢ coinvariantsTensorIndInv φ A B ≫ coinvariantsTensorIndHom φ A B =
    𝟙 ((Functor.obj (coinvariantsTensor k G) A).obj (res φ B))

Tactic:
ext