awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A B C : Rep.{w, u, v} k G
X Y : Rep.{u_1, u, v} k G
f : X ⟶ Y
g : G
x : LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑X : Type u_1)
x_1 : (↑A : Type w)
⊢ Eq.{u_1 + 1} (α := (↑Y : Type u_1))
    (((((LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Y : Type u_1) :
                      (a : (↑X : Type u_1) →ₗ[k] (↑Y : Type u_1)) →
                        ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
                    (Hom.hom f).toLinearMap ∘ₗ
                  (A.ρ.linHom X.ρ :
                      (a : G) → ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑X : Type u_1))
                    g :
                (a : (↑A : Type w) →ₗ[k] (↑X : Type u_1)) → (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
              x :
            LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑Y : Type u_1)) :
          (a : (↑A : Type w)) → (↑Y : Type u_1))
        x_1 :
      (↑Y : Type u_1))
    (((((A.ρ.linHom Y.ρ : (a : G) → ((↑A : Type w) →ₗ[k] (↑Y : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
                    g ∘ₗ
                  (LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Y : Type u_1) :
                      (a : (↑X : Type u_1) →ₗ[k] (↑Y : Type u_1)) →
                        ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
                    (Hom.hom f).toLinearMap :
                (a : (↑A : Type w) →ₗ[k] (↑X : Type u_1)) → (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
              x :
            LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑Y : Type u_1)) :
          (a : (↑A : Type w)) → (↑Y : Type u_1))
        x_1 :
      (↑Y : Type u_1))

Tactic:
simp [Representation.IntertwiningMap.toLinearMap_apply, ← hom_comm_apply]

Premises used: Representation.IntertwiningMap.toLinearMap_apply, Rep.hom_comm_apply
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A B C : Rep.{w, u, v} k G
x : Rep.{u_1, u, v} k G
hf :
  ∀ (x_1 : (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) (x_2 : (↑A : Type w)),
    Eq.{u_1 + 1} (α := (↑x : Type u_1))
      ((((Representation.IntertwiningMap.toLinearMap
                    (Hom.hom
                      (ofHom
                        {
                          toLinearMap :=
                            (LinearMap.llcomp k (↑A : Type w) (↑x : Type u_1) (↑x : Type u_1) :
                                (a : (↑x : Type u_1) →ₗ[k] (↑x : Type u_1)) →
                                  ((↑A : Type w) →ₗ[k] (↑x : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑x : Type u_1))
                              (Hom.hom (𝟙 x)).toLinearMap,
                          isIntertwining' := ⋯ : (A.ρ.linHom x.ρ).IntertwiningMap (A.ρ.linHom x.ρ) })) :
                  (a : (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1)))
                x_1 :
              (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) :
            (a : (↑A : Type w)) → (↑x : Type u_1))
          x_2 :
        (↑x : Type u_1))
      (((((Hom.hom (𝟙 (of (A.ρ.linHom x.ρ)))).toLinearMap :
                  (a : (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1)))
                x_1 :
              (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) :
            (a : (↑A : Type w)) → (↑x : Type u_1))
          x_2 :
        (↑x : Type u_1))
⊢ ofHom
      {
        toLinearMap :=
          (LinearMap.llcomp k (↑A : Type w) (↑x : Type u_1) (↑x : Type u_1) :
              (a : (↑x : Type u_1) →ₗ[k] (↑x : Type u_1)) →
                ((↑A : Type w) →ₗ[k] (↑x : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑x : Type u_1))
            (Hom.hom (𝟙 x)).toLinearMap,
        isIntertwining' := ⋯ } =
    𝟙 (of (A.ρ.linHom x.ρ))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A B C : Rep.{w, u, v} k G
x : Rep.{u_1, u, v} k G
x_1 : (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))
x_2 : (↑A : Type w)
⊢ Eq.{u_1 + 1} (α := (↑x : Type u_1))
    ((((Representation.IntertwiningMap.toLinearMap
                  (Hom.hom
                    (ofHom
                      {
                        toLinearMap :=
                          (LinearMap.llcomp k (↑A : Type w) (↑x : Type u_1) (↑x : Type u_1) :
                              (a : (↑x : Type u_1) →ₗ[k] (↑x : Type u_1)) →
                                ((↑A : Type w) →ₗ[k] (↑x : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑x : Type u_1))
                            (Hom.hom (𝟙 x)).toLinearMap,
                        isIntertwining' := ⋯ : (A.ρ.linHom x.ρ).IntertwiningMap (A.ρ.linHom x.ρ) })) :
                (a : (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1)))
              x_1 :
            (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) :
          (a : (↑A : Type w)) → (↑x : Type u_1))
        x_2 :
      (↑x : Type u_1))
    (((((Hom.hom (𝟙 (of (A.ρ.linHom x.ρ)))).toLinearMap :
                (a : (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1)))
              x_1 :
            (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) :
          (a : (↑A : Type w)) → (↑x : Type u_1))
        x_2 :
      (↑x : Type u_1))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A B C : Rep.{w, u, v} k G
X Y Z : Rep.{u_1, u, v} k G
x : X ⟶ Y
x_1 : Y ⟶ Z
x_2 : (↑(of (A.ρ.linHom X.ρ)) : Type (max w u_1))
x_3 : (↑A : Type w)
⊢ Eq.{u_1 + 1} (α := (↑Z : Type u_1))
    ((((Representation.IntertwiningMap.toLinearMap
                  (Hom.hom
                    (ofHom
                      {
                        toLinearMap :=
                          (LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Z : Type u_1) :
                              (a : (↑X : Type u_1) →ₗ[k] (↑Z : Type u_1)) →
                                ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Z : Type u_1))
                            (Hom.hom (x ≫ x_1)).toLinearMap,
                        isIntertwining' := ⋯ : (A.ρ.linHom X.ρ).IntertwiningMap (A.ρ.linHom Z.ρ) })) :
                (a : (↑(of (A.ρ.linHom X.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom Z.ρ)) : Type (max w u_1)))
              x_2 :
            (↑(of (A.ρ.linHom Z.ρ)) : Type (max w u_1))) :
          (a : (↑A : Type w)) → (↑Z : Type u_1))
        x_3 :
      (↑Z : Type u_1))
    ((((Representation.IntertwiningMap.toLinearMap
                  (Hom.hom
                    (CategoryStruct.comp (Y := of (A.ρ.linHom Y.ρ))
                      (ofHom
                        {
                          toLinearMap :=
                            (LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Y : Type u_1) :
                                (a : (↑X : Type u_1) →ₗ[k] (↑Y : Type u_1)) →
                                  ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
                              (Hom.hom x).toLinearMap,
                          isIntertwining' := ⋯ : (A.ρ.linHom X.ρ).IntertwiningMap (A.ρ.linHom Y.ρ) })
                      (ofHom
                        {
                          toLinearMap :=
                            (LinearMap.llcomp k (↑A : Type w) (↑Y : Type u_1) (↑Z : Type u_1) :
                                (a : (↑Y : Type u_1) →ₗ[k] (↑Z : Type u_1)) →
                                  ((↑A : Type w) →ₗ[k] (↑Y : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Z : Type u_1))
                              (Hom.hom x_1).toLinearMap,
                          isIntertwining' := ⋯ : (A.ρ.linHom Y.ρ).IntertwiningMap (A.ρ.linHom Z.ρ) }))) :
                (a : (↑(of (A.ρ.linHom X.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom Z.ρ)) : Type (max w u_1)))
              x_2 :
            (↑(of (A.ρ.linHom Z.ρ)) : Type (max w u_1))) :
          (a : (↑A : Type w)) → (↑Z : Type u_1))
        x_3 :
      (↑Z : Type u_1))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A : Rep.{u_1, u, v} k G
B : Rep.{u_2, u, v} k G
g : G
x : LinearMap.{u, u, u_1, u_2} (RingHom.id k) (↑A : Type u_1) (↑B : Type u_2)
⊢ Eq (α := LinearMap.{u, u, u_1, u_2} (RingHom.id k) (↑A : Type u_1) (↑B : Type u_2))
    (((((A.ihom.obj B).ρ :
                (a : G) → ((↑A : Type u_1) →ₗ[k] (↑B : Type u_2)) →ₗ[k] (↑A : Type u_1) →ₗ[k] (↑B : Type u_2))
              g :
            LinearMap.{u, u, u_1, u_2} (RingHom.id k) (↑A : Type u_1) (↑B : Type u_2) →ₗ[k]
              LinearMap.{u, u, u_1, u_2} (RingHom.id k) (↑A : Type u_1) (↑B : Type u_2)) :
          (a : (↑A : Type u_1) →ₗ[k] (↑B : Type u_2)) → (↑A : Type u_1) →ₗ[k] (↑B : Type u_2))
        x :
      LinearMap.{u, u, u_1, u_2} (RingHom.id k) (↑A : Type u_1) (↑B : Type u_2))
    ((B.ρ : (a : G) → (↑B : Type u_2) →ₗ[k] (↑B : Type u_2)) g ∘ₗ
        x ∘ₗ (A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g⁻¹ :
      LinearMap.{u, u, u_1, u_2} (RingHom.id k) (↑A : Type u_1) (↑B : Type u_2))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A_1 B_1 C_1 : Rep.{w, u, v} k G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
g : G
h :
  ∀ (x : (↑B : Type u)) (y : (↑A : Type u)),
    Eq (α := (↑C : Type u))
      (((((TensorProduct.curry (Hom.hom f).toLinearMap).flip ∘ₗ (B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g :
                  (a : (↑B : Type u)) → (↑A : Type u) →ₗ[k] (↑C : Type u))
                x :
              (↑A : Type u) →ₗ[k] (↑C : Type u)) :
            (a : (↑A : Type u)) → (↑C : Type u))
          y :
        (↑C : Type u))
      (((((A.ρ.linHom C.ρ : (a : G) → ((↑A : Type u) →ₗ[k] (↑C : Type u)) →ₗ[k] (↑A : Type u) →ₗ[k] (↑C : Type u)) g ∘ₗ
                    (TensorProduct.curry (Hom.hom f).toLinearMap).flip :
                  (a : (↑B : Type u)) → (↑A : Type u) →ₗ[k] (↑C : Type u))
                x :
              (↑A : Type u) →ₗ[k] (↑C : Type u)) :
            (a : (↑A : Type u)) → (↑C : Type u))
          y :
        (↑C : Type u))
⊢ (TensorProduct.curry (Hom.hom f).toLinearMap).flip ∘ₗ (B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g =
    (A.ρ.linHom C.ρ : (a : G) → ((↑A : Type u) →ₗ[k] (↑C : Type u)) →ₗ[k] (↑A : Type u) →ₗ[k] (↑C : Type u)) g ∘ₗ
      (TensorProduct.curry (Hom.hom f).toLinearMap).flip

Tactic:
ext x y
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A_1 B_1 C_1 : Rep.{w, u, v} k G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
g : G
x : (↑B : Type u)
y : (↑A : Type u)
h :
  Eq (α := (↑C : Type u))
    ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
        (y ⊗ₜ[k]
            (((B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                (a : (↑B : Type u)) → (↑B : Type u))
              x :
          TensorProduct k (↑A : Type u) (↑B : Type u)) :
      (↑C : Type u))
    ((((C.ρ : (a : G) → (↑C : Type u) →ₗ[k] (↑C : Type u)) g : (↑C : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑C : Type u)) → (↑C : Type u))
        ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                    (a : (↑A : Type u)) → (↑A : Type u))
                  y ⊗ₜ[k]
                x :
              TensorProduct k (↑A : Type u) (↑B : Type u)) :
          (↑C : Type u)) :
      (↑C : Type u))
⊢ Eq (α := (↑C : Type u))
    (((((TensorProduct.curry (Hom.hom f).toLinearMap).flip ∘ₗ (B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g :
                (a : (↑B : Type u)) → (↑A : Type u) →ₗ[k] (↑C : Type u))
              x :
            (↑A : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑A : Type u)) → (↑C : Type u))
        y :
      (↑C : Type u))
    (((((A.ρ.linHom C.ρ : (a : G) → ((↑A : Type u) →ₗ[k] (↑C : Type u)) →ₗ[k] (↑A : Type u) →ₗ[k] (↑C : Type u)) g ∘ₗ
                  (TensorProduct.curry (Hom.hom f).toLinearMap).flip :
                (a : (↑B : Type u)) → (↑A : Type u) →ₗ[k] (↑C : Type u))
              x :
            (↑A : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑A : Type u)) → (↑C : Type u))
        y :
      (↑C : Type u))

Tactic:
simp only [tensor_V, tensor_ρ, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply,
      TensorProduct.curry_apply, Representation.IntertwiningMap.toLinearMap_apply,
      Representation.linHom_apply]

Premises used: Representation.linHom_apply, LinearMap.flip_apply, Rep.tensor_ρ, Representation.IntertwiningMap.toLinearMap_apply, LinearMap.coe_comp, TensorProduct.curry_apply, Function.comp_apply, Rep.tensor_V
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A_1 B_1 C_1 : Rep.{w, u, v} k G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
g : G
x : (↑B : Type u)
y : (↑A : Type u)
⊢ Eq (α := (↑C : Type u))
    ((((C.ρ : (a : G) → (↑C : Type u) →ₗ[k] (↑C : Type u)) g : (↑C : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑C : Type u)) → (↑C : Type u))
        ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                    (a : (↑A : Type u)) → (↑A : Type u))
                  y ⊗ₜ[k]
                x :
              TensorProduct k (↑A : Type u) (↑B : Type u)) :
          (↑C : Type u)) :
      (↑C : Type u))
    ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
        (y ⊗ₜ[k]
            (((B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                (a : (↑B : Type u)) → (↑B : Type u))
              x :
          TensorProduct k (↑A : Type u) (↑B : Type u)) :
      (↑C : Type u))

Tactic:
simpa using (hom_comm_apply f g (A.ρ g⁻¹ y ⊗ₜ[k] x)).symm

Premises used: Inv.inv, Rep.ρ, Rep.hom_comm_apply, TensorProduct.tmul, Eq.symm, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A_1 B_1 C_1 : Rep.{w, u, v} k G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
g : G
x : (↑B : Type u)
y : (↑A : Type u)
⊢ Eq (α := (↑C : Type u))
    ((((C.ρ : (a : G) → (↑C : Type u) →ₗ[k] (↑C : Type u)) g : (↑C : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑C : Type u)) → (↑C : Type u))
        ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                    (a : (↑A : Type u)) → (↑A : Type u))
                  y ⊗ₜ[k]
                x :
              TensorProduct k (↑A : Type u) (↑B : Type u)) :
          (↑C : Type u)) :
      (↑C : Type u))
    ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
        (y ⊗ₜ[k]
            (((B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                (a : (↑B : Type u)) → (↑B : Type u))
              x :
          TensorProduct k (↑A : Type u) (↑B : Type u)) :
      (↑C : Type u))

Tactic:
have := by simpa using (hom_comm_apply f g (A.ρ g⁻¹ y ⊗ₜ[k] x)).symm
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A_1 B_1 C_1 : Rep.{w, u, v} k G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
g : G
x : (↑B : Type u)
y : (↑A : Type u)
this :
  Eq (α := (↑C : Type u))
    ((((C.ρ : (a : G) → (↑C : Type u) →ₗ[k] (↑C : Type u)) g : (↑C : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑C : Type u)) → (↑C : Type u))
        ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                    (a : (↑A : Type u)) → (↑A : Type u))
                  y ⊗ₜ[k]
                x :
              TensorProduct k (↑A : Type u) (↑B : Type u)) :
          (↑C : Type u)) :
      (↑C : Type u))
    ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
        (y ⊗ₜ[k]
            (((B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                (a : (↑B : Type u)) → (↑B : Type u))
              x :
          TensorProduct k (↑A : Type u) (↑B : Type u)) :
      (↑C : Type u))
⊢ Eq (α := (↑C : Type u))
    ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
        (y ⊗ₜ[k]
            (((B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                (a : (↑B : Type u)) → (↑B : Type u))
              x :
          TensorProduct k (↑A : Type u) (↑B : Type u)) :
      (↑C : Type u))
    ((((C.ρ : (a : G) → (↑C : Type u) →ₗ[k] (↑C : Type u)) g : (↑C : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑C : Type u)) → (↑C : Type u))
        ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                    (a : (↑A : Type u)) → (↑A : Type u))
                  y ⊗ₜ[k]
                x :
              TensorProduct k (↑A : Type u) (↑B : Type u)) :
          (↑C : Type u)) :
      (↑C : Type u))

Tactic:
simp [this]
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A_1 B_1 C_1 : Rep.{w, u, v} k G
A B C : Rep k G
f : B ⟶ A.ihom.obj C
g : G
x : (↑A : Type u)
y : (↑B : Type u)
⊢ Eq (α := (↑C : Type u))
    (((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) (↑B : Type u) (↑C : Type u) :
                (a : (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] (↑C : Type u)) →
                  TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
              (Hom.hom f).flip ∘ₗ
            (A.ρ.tprod B.ρ :
                (a : G) → TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] TensorProduct k (↑A : Type u) (↑B : Type u))
              g :
          (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
        (x ⊗ₜ[k] y) :
      (↑C : Type u))
    (((C.ρ : (a : G) → (↑C : Type u) →ₗ[k] (↑C : Type u)) g ∘ₗ
            (TensorProduct.uncurry (RingHom.id k) (↑A : Type u) (↑B : Type u) (↑C : Type u) :
                (a : (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] (↑C : Type u)) →
                  TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
              (Hom.hom f).flip :
          (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
        (x ⊗ₜ[k] y) :
      (↑C : Type u))

Tactic:
simpa using LinearMap.ext_iff.1 (hom_comm_apply f g y) (A.ρ g x)

Premises used: LinearMap.ext_iff, Rep.ρ, Iff.mp, Rep.hom_comm_apply, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B : Rep k G
⊢ (Functor.obj (ihom A) B).ρ = (A.ihom.obj B).ρ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B C : Rep k G
⊢ Adjunction.homEquiv (ihom.adjunction A) B C = A.tensorHomEquiv B C

Tactic:
congrFun (congrFun (Adjunction.mkOfHomEquiv_homEquiv _) _) _

Premises used: Rep.ihom, CategoryTheory.Adjunction.mk', Rep.tensorHomEquiv, CategoryTheory.Adjunction.mkOfHomEquiv, congrFun, CategoryTheory.ihom, CategoryTheory.ihom.adjunction, CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B : Rep k G
h :
  ∀ (x : (↑(Functor.obj (ihom A ⋙ tensorLeft A) B) : Type u)),
    Eq (α := (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
      ((Representation.IntertwiningMap.toLinearMap (Hom.hom (NatTrans.app (ihom.ev A) B)) :
            (a : (↑((ihom A ⋙ tensorLeft A).obj B) : Type u)) → (↑((𝟭 (Rep k G)).obj B) : Type u))
          x :
        (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
      ((((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) (↑B : Type u) :
                  (a : (↑A : Type u) →ₗ[k] ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u)) →
                    TensorProduct k (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u))
                (LinearMap.flip LinearMap.id) :
              TensorProduct k (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u)) :
            (a : (↑((ihom A ⋙ tensorLeft A).obj B) : Type u)) → (↑((𝟭 (Rep k G)).obj B) : Type u))
          x :
        (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
⊢ Eq (α := (↑(Functor.obj (ihom A ⋙ tensorLeft A) B) : Type u) →ₗ[k] (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
    (Representation.IntertwiningMap.toLinearMap (Hom.hom (NatTrans.app (ihom.ev A) B)))
    ((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) (↑B : Type u) :
        (a : (↑A : Type u) →ₗ[k] ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u)) →
          TensorProduct k (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u))
      (LinearMap.flip LinearMap.id))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B : Rep k G
x : (↑(Functor.obj (ihom A ⋙ tensorLeft A) B) : Type u)
⊢ Eq (α := (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom (NatTrans.app (ihom.ev A) B)) :
          (a : (↑((ihom A ⋙ tensorLeft A).obj B) : Type u)) → (↑((𝟭 (Rep k G)).obj B) : Type u))
        x :
      (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
    ((((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) (↑B : Type u) :
                (a : (↑A : Type u) →ₗ[k] ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u)) →
                  TensorProduct k (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u))
              (LinearMap.flip LinearMap.id) :
            TensorProduct k (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u)) :
          (a : (↑((ihom A ⋙ tensorLeft A).obj B) : Type u)) → (↑((𝟭 (Rep k G)).obj B) : Type u))
        x :
      (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B : Rep k G
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (NatTrans.app (ihom.coev A) B)) =
    LinearMap.flip (TensorProduct.mk k (↑A : Type u) (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))

Tactic:
LinearMap.ext fun _ => LinearMap.ext fun _ => rfl

Premises used: LinearMap.ext, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
⊢ Representation.IntertwiningMap.toLinearMap
      (Hom.hom ((linearHomEquiv A B C : (a : A ⊗ B ⟶ C) → B ⟶ (ihom A).obj C) f)) =
    (TensorProduct.curry (Hom.hom f).toLinearMap).flip

Tactic:
rfl

Premises used: LinearMap.mk₂'ₛₗ, LinearMap.flip, TensorProduct.tmul, AddCon.toQuotient, rfl