awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
x : X ⟶ Y
x_1 : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((((TensorProduct.AlgebraTensorModule.curry
                  (toLinearMap
                    (Hom.hom (ofHom (lTensor (ρ (trivial k G k)) (Hom.hom x)) ≫ Iso.hom (mkIso (lid k Y.ρ))))) :
                (↑(trivial k G k) : Type u) →ₗ[k] (↑X : Type u) →ₗ[k] (↑Y : Type u)) :
              (a : k) → (↑X : Type u) →ₗ[k] (↑Y : Type u))
            1 :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x_1 :
      (↑Y : Type u))
    ((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (Hom.hom (Iso.hom (mkIso (lid k X.ρ)) ≫ x))) :
                (↑(trivial k G k) : Type u) →ₗ[k] (↑X : Type u) →ₗ[k] (↑Y : Type u)) :
              (a : k) → (↑X : Type u) →ₗ[k] (↑Y : Type u))
            1 :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x_1 :
      (↑Y : Type u))

Tactic:
simp [trivial_V]

Premises used: Rep.trivial_V
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
x : X ⟶ Y
hf : 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.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
x : X ⟶ Y
x_1 : (↑X : Type u)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [trivial_V]

Premises used: Rep.trivial_V
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 x_3 : Rep k G
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ofHom (rTensor x_3.ρ (Hom.hom (mkIso (assoc x.ρ x_1.ρ x_2.ρ)).hom)) ≫
      (mkIso (assoc x.ρ (of (x_1.ρ.tprod x_2.ρ)).ρ x_3.ρ)).hom ≫
        ofHom (lTensor x.ρ (Hom.hom (mkIso (assoc x_1.ρ x_2.ρ x_3.ρ)).hom)) =
    (mkIso (assoc (of (x.ρ.tprod x_1.ρ)).ρ x_2.ρ x_3.ρ)).hom ≫ (mkIso (assoc x.ρ x_1.ρ (of (x_2.ρ.tprod x_3.ρ)).ρ)).hom

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 x_3 : Rep k G
x_4 : (↑x : Type u)
x_5 : (↑x_1 : Type u)
x_6 : (↑x_2 : Type u)
x_7 : (↑x_3 : Type u)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
hf : 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.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
x : (↑X : Type u)
x_1 : (↑Y : Type u)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
⊢ (↑((𝟙_ (Rep k G)) (𝒞 := instCategory)) : Type u) = k

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
⊢ Eq (α := Representation k G (↑((𝟙_ (Rep k G)) (𝒞 := instCategory)) : Type u)) (ρ ((𝟙_ (Rep k G)) (𝒞 := instCategory)))
    (Representation.trivial k G k)

Tactic:
rfl

Premises used: Representation.trivial, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
⊢ (↑(tensorObj (𝒞 := instCategory) X Y) : Type u) = TensorProduct k (↑X : Type u) (↑Y : Type u)

Tactic:
rfl

Premises used: Quotient, TensorProduct, AddCon.Quotient, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
⊢ (tensorObj (𝒞 := instCategory) X Y).ρ = X.ρ.tprod Y.ρ

Tactic:
rfl

Premises used: Representation.tprod, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X₁ X₂ Y : Rep k G
f : X₁ ⟶ X₂
⊢ Hom.hom (f ▷ Y) = rTensor Y.ρ (Hom.hom f)

Tactic:
rfl

Premises used: Representation.IntertwiningMap.tensor, Representation.IntertwiningMap.rTensor, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y₁ Y₂ : Rep k G
f : Y₁ ⟶ Y₂
⊢ Hom.hom (X ◁ f) = lTensor X.ρ (Hom.hom f)

Tactic:
rfl

Premises used: Representation.IntertwiningMap.tensor, rfl, Representation.IntertwiningMap.lTensor
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X₁ X₂ Y₁ Y₂ : Rep k G
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Hom.hom (f ⊗ₘ g) = (Hom.hom f).tensor (Hom.hom g)

Tactic:
rfl

Premises used: Representation.IntertwiningMap.tensor, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Type u
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
σ : Representation k G X
ρ : Representation k G Y
⊢ of (σ.tprod ρ) = tensorObj (𝒞 := instCategory) (of σ) (of ρ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
h :
  toLinearMap (Hom.hom (Iso.hom (α_ X Y Z))) =
    (↑(assoc X.ρ Y.ρ Z.ρ) : ((X.ρ.tprod Y.ρ).tprod Z.ρ).IntertwiningMap (X.ρ.tprod (Y.ρ.tprod Z.ρ))).toLinearMap
⊢ Hom.hom (Iso.hom (α_ X Y Z)) =
    (↑(assoc X.ρ Y.ρ Z.ρ) : ((X.ρ.tprod Y.ρ).tprod Z.ρ).IntertwiningMap (X.ρ.tprod (Y.ρ.tprod Z.ρ)))

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
x : (↑X : Type u)
y : (↑Y : Type u)
z : (↑Z : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) : Type u))
    ((toLinearMap (Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : TensorProduct k (TensorProduct k (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) → (↑(X ⊗ Y ⊗ Z) : Type u))
        (x ⊗ₜ[k] y ⊗ₜ[k] z) :
      (↑(tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) : Type u))
    (((↑(assoc X.ρ Y.ρ Z.ρ) : ((X.ρ.tprod Y.ρ).tprod Z.ρ).IntertwiningMap (X.ρ.tprod (Y.ρ.tprod Z.ρ))).toLinearMap :
          (a : TensorProduct k (TensorProduct k (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) → (↑(X ⊗ Y ⊗ Z) : Type u))
        (x ⊗ₜ[k] y ⊗ₜ[k] z) :
      (↑(tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
⊢ toLinearMap (Hom.hom (Iso.hom (α_ X Y Z))) =
    (↑(assoc X.ρ Y.ρ Z.ρ) : ((X.ρ.tprod Y.ρ).tprod Z.ρ).IntertwiningMap (X.ρ.tprod (Y.ρ.tprod Z.ρ))).toLinearMap

Tactic:
refine TensorProduct.ext_threefold fun x y z ↦ by rfl

Premises used: TensorProduct.ext_threefold
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
⊢ Hom.hom (Iso.inv (α_ X Y Z)) =
    (↑(assoc X.ρ Y.ρ Z.ρ).symm : (X.ρ.tprod (Y.ρ.tprod Z.ρ)).IntertwiningMap ((X.ρ.tprod Y.ρ).tprod Z.ρ))

Tactic:
rfl

Premises used: Representation.tprod, Quotient, TensorProduct, AddCon.Quotient, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep k G
⊢ Hom.hom (Iso.hom (λ_ X)) = (↑(lid k X.ρ) : ((Representation.trivial k G k).tprod X.ρ).IntertwiningMap X.ρ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep k G
⊢ Hom.hom (Iso.inv (λ_ X)) = (↑(lid k X.ρ).symm : X.ρ.IntertwiningMap ((Representation.trivial k G k).tprod X.ρ))

Tactic:
rfl

Premises used: Representation.trivial, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep k G
⊢ Hom.hom (Iso.hom (ρ_ X)) = (↑(rid k X.ρ) : (X.ρ.tprod (Representation.trivial k G k)).IntertwiningMap X.ρ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep k G
⊢ Hom.hom (Iso.inv (ρ_ X)) = (↑(rid k X.ρ).symm : X.ρ.IntertwiningMap (X.ρ.tprod (Representation.trivial k G k)))

Tactic:
rfl

Premises used: Representation.trivial, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
hf :
  Eq (α := (tensorObj (𝒞 := instCategory) x x_1).ρ.IntertwiningMap (tensorObj (𝒞 := instCategory) x x_2).ρ)
    (Hom.hom (x ◁ 0)) (Hom.hom 0)
⊢ Eq.{u + 1} (α := tensorObj (𝒞 := instCategory) x x_1 ⟶ tensorObj (𝒞 := instCategory) x x_2) (x ◁ 0) 0

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
⊢ Eq (α := (tensorObj (𝒞 := instCategory) x x_1).ρ.IntertwiningMap (tensorObj (𝒞 := instCategory) x x_2).ρ)
    (Hom.hom (x ◁ 0)) (Hom.hom 0)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
hf :
  Eq (α := (tensorObj (𝒞 := instCategory) x_1 x).ρ.IntertwiningMap (tensorObj (𝒞 := instCategory) x_2 x).ρ)
    (Hom.hom (0 ▷ x)) (Hom.hom 0)
⊢ Eq.{u + 1} (α := tensorObj (𝒞 := instCategory) x_1 x ⟶ tensorObj (𝒞 := instCategory) x_2 x) (0 ▷ x) 0

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
⊢ Eq (α := (tensorObj (𝒞 := instCategory) x_1 x).ρ.IntertwiningMap (tensorObj (𝒞 := instCategory) x_2 x).ρ)
    (Hom.hom (0 ▷ x)) (Hom.hom 0)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
x x_1 : Y ⟶ Z
hf :
  Hom.hom (X ◁ (x + x_1)) =
    Hom.hom (HAdd.hAdd (α := tensorObj (𝒞 := instCategory) X Y ⟶ tensorObj (𝒞 := instCategory) X Z) (X ◁ x) (X ◁ x_1))
⊢ X ◁ (x + x_1) =
    HAdd.hAdd (α := tensorObj (𝒞 := instCategory) X Y ⟶ tensorObj (𝒞 := instCategory) X Z) (X ◁ x) (X ◁ x_1)

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
x x_1 : Y ⟶ Z
⊢ Hom.hom (X ◁ (x + x_1)) =
    Hom.hom (HAdd.hAdd (α := tensorObj (𝒞 := instCategory) X Y ⟶ tensorObj (𝒞 := instCategory) X Z) (X ◁ x) (X ◁ x_1))

Tactic:
simp [add_hom]

Premises used: Rep.add_hom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
x x_1 : Y ⟶ Z
hf :
  Hom.hom ((x + x_1) ▷ X) =
    Hom.hom (HAdd.hAdd (α := tensorObj (𝒞 := instCategory) Y X ⟶ tensorObj (𝒞 := instCategory) Z X) (x ▷ X) (x_1 ▷ X))
⊢ (x + x_1) ▷ X =
    HAdd.hAdd (α := tensorObj (𝒞 := instCategory) Y X ⟶ tensorObj (𝒞 := instCategory) Z X) (x ▷ X) (x_1 ▷ X)

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
x x_1 : Y ⟶ Z
⊢ Hom.hom ((x + x_1) ▷ X) =
    Hom.hom (HAdd.hAdd (α := tensorObj (𝒞 := instCategory) Y X ⟶ tensorObj (𝒞 := instCategory) Z X) (x ▷ X) (x_1 ▷ X))

Tactic:
simp [add_hom]

Premises used: Rep.add_hom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
x_3 : k
x_4 : x_1 ⟶ x_2
hf :
  Hom.hom (x ◁ (x_3 • x_4)) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x x_1 ⟶ tensorObj (𝒞 := instCategory) x x_2) x_3 (x ◁ x_4))
⊢ x ◁ (x_3 • x_4) =
    HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x x_1 ⟶ tensorObj (𝒞 := instCategory) x x_2) x_3 (x ◁ x_4)

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
x_3 : k
x_4 : x_1 ⟶ x_2
⊢ Hom.hom (x ◁ (x_3 • x_4)) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x x_1 ⟶ tensorObj (𝒞 := instCategory) x x_2) x_3 (x ◁ x_4))

Tactic:
simp [smul_hom]

Premises used: Rep.smul_hom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x : k
x_1 x_2 : Rep k G
x_3 : x_1 ⟶ x_2
x_4 : Rep k G
hf :
  Hom.hom ((x • x_3) ▷ x_4) =
    Hom.hom
      (HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x_1 x_4 ⟶ tensorObj (𝒞 := instCategory) x_2 x_4) x (x_3 ▷ x_4))
⊢ (x • x_3) ▷ x_4 =
    HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x_1 x_4 ⟶ tensorObj (𝒞 := instCategory) x_2 x_4) x (x_3 ▷ x_4)

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x : k
x_1 x_2 : Rep k G
x_3 : x_1 ⟶ x_2
x_4 : Rep k G
⊢ Hom.hom ((x • x_3) ▷ x_4) =
    Hom.hom
      (HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x_1 x_4 ⟶ tensorObj (𝒞 := instCategory) x_2 x_4) x (x_3 ▷ x_4))

Tactic:
simp [smul_hom]

Premises used: Rep.smul_hom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
x_3 : x_1 ⟶ x_2
hf :
  Hom.hom (x ◁ x_3 ≫ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ≫ x_3 ▷ x)
⊢ x ◁ x_3 ≫ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom =
    (mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ≫ x_3 ▷ x

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
x_3 : x_1 ⟶ x_2
⊢ Hom.hom (x ◁ x_3 ≫ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ≫ x_3 ▷ x)

Tactic:
simp [comm_comp_lTensor]

Premises used: Representation.TensorProduct.comm_comp_lTensor
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
x : X ⟶ Y
x_1 : Rep k G
hf :
  Hom.hom (x ▷ x_1 ≫ (mkIso (Representation.TensorProduct.comm Y.ρ x_1.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm X.ρ x_1.ρ)).hom ≫ x_1 ◁ x)
⊢ x ▷ x_1 ≫ (mkIso (Representation.TensorProduct.comm Y.ρ x_1.ρ)).hom =
    (mkIso (Representation.TensorProduct.comm X.ρ x_1.ρ)).hom ≫ x_1 ◁ x

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
x : X ⟶ Y
x_1 : Rep k G
⊢ Hom.hom (x ▷ x_1 ≫ (mkIso (Representation.TensorProduct.comm Y.ρ x_1.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm X.ρ x_1.ρ)).hom ≫ x_1 ◁ x)

Tactic:
simp [comm_comp_rTensor]

Premises used: Representation.TensorProduct.comm_comp_rTensor
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
hf :
  (Hom.hom
        (Iso.hom (α_ x x_1 x_2) ≫
          (mkIso (Representation.TensorProduct.comm x.ρ (tensorObj (𝒞 := instCategory) x_1 x_2).ρ)).hom ≫
            Iso.hom (α_ x_1 x_2 x))).toLinearMap =
    (Hom.hom
        ((mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ▷ x_2 ≫
          Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom)).toLinearMap
⊢ Iso.hom (α_ x x_1 x_2) ≫
      (mkIso (Representation.TensorProduct.comm x.ρ (tensorObj (𝒞 := instCategory) x_1 x_2).ρ)).hom ≫
        Iso.hom (α_ x_1 x_2 x) =
    (mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ▷ x_2 ≫
      Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
x_3 : (↑x : Type u)
x_4 : (↑x_1 : Type u)
x_5 : (↑x_2 : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := instCategory) x_1 (tensorObj (𝒞 := instCategory) x_2 x)) : Type u))
    (((Hom.hom
              (Iso.hom (α_ x x_1 x_2) ≫
                (mkIso (Representation.TensorProduct.comm x.ρ (tensorObj (𝒞 := instCategory) x_1 x_2).ρ)).hom ≫
                  Iso.hom (α_ x_1 x_2 x))).toLinearMap :
          (a : TensorProduct k (TensorProduct k (↑x : Type u) (↑x_1 : Type u)) (↑x_2 : Type u)) →
            (↑(x_1 ⊗ x_2 ⊗ x) : Type u))
        (x_3 ⊗ₜ[k] x_4 ⊗ₜ[k] x_5) :
      (↑(tensorObj (𝒞 := instCategory) x_1 (tensorObj (𝒞 := instCategory) x_2 x)) : Type u))
    (((Hom.hom
              ((mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ▷ x_2 ≫
                Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom)).toLinearMap :
          (a : TensorProduct k (TensorProduct k (↑x : Type u) (↑x_1 : Type u)) (↑x_2 : Type u)) →
            (↑(x_1 ⊗ x_2 ⊗ x) : Type u))
        (x_3 ⊗ₜ[k] x_4 ⊗ₜ[k] x_5) :
      (↑(tensorObj (𝒞 := instCategory) x_1 (tensorObj (𝒞 := instCategory) x_2 x)) : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
⊢ (Hom.hom
        (Iso.hom (α_ x x_1 x_2) ≫
          (mkIso (Representation.TensorProduct.comm x.ρ (tensorObj (𝒞 := instCategory) x_1 x_2).ρ)).hom ≫
            Iso.hom (α_ x_1 x_2 x))).toLinearMap =
    (Hom.hom
        ((mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ▷ x_2 ≫
          Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom)).toLinearMap

Tactic:
exact TensorProduct.ext_threefold <| fun _ _ _ ↦ by simp

Premises used: TensorProduct.ext_threefold
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
hf :
  (Hom.hom
        (Iso.inv (α_ X Y Z) ≫
          (mkIso (Representation.TensorProduct.comm (tensorObj (𝒞 := instCategory) X Y).ρ Z.ρ)).hom ≫
            Iso.inv (α_ Z X Y))).toLinearMap =
    (Hom.hom
        (X ◁ (mkIso (Representation.TensorProduct.comm Y.ρ Z.ρ)).hom ≫
          Iso.inv (α_ X Z Y) ≫ (mkIso (Representation.TensorProduct.comm X.ρ Z.ρ)).hom ▷ Y)).toLinearMap
⊢ Iso.inv (α_ X Y Z) ≫
      (mkIso (Representation.TensorProduct.comm (tensorObj (𝒞 := instCategory) X Y).ρ Z.ρ)).hom ≫ Iso.inv (α_ Z X Y) =
    X ◁ (mkIso (Representation.TensorProduct.comm Y.ρ Z.ρ)).hom ≫
      Iso.inv (α_ X Z Y) ≫ (mkIso (Representation.TensorProduct.comm X.ρ Z.ρ)).hom ▷ Y

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
⊢ Hom.hom (Iso.hom (β_ X Y)) =
    (↑(Representation.TensorProduct.comm X.ρ Y.ρ) : (X.ρ.tprod Y.ρ).IntertwiningMap (Y.ρ.tprod X.ρ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
hf : Hom.hom (Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X)) = Hom.hom (𝟙 (tensorObj (𝒞 := instCategory) X Y))
⊢ Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj (𝒞 := instCategory) X Y)

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
⊢ Hom.hom (Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X)) = Hom.hom (𝟙 (tensorObj (𝒞 := instCategory) X Y))

Tactic:
simp [← comm_symm Y.ρ X.ρ, ← toIntertwiningMap_trans,
    trans_symm, toIntertwiningMap_refl]

Premises used: Representation.Equiv.trans_symm, Representation.Equiv.toIntertwiningMap_trans, Representation.Equiv.toIntertwiningMap_refl, Rep.ρ, Representation.TensorProduct.comm_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 B C : Rep.{w, u, v} k G
X Y : Rep.{u_1, u, v} k G
f : X ⟶ Y
g : G
h :
  ∀ (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))
⊢ Eq (α :=
    LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑X : Type u_1) →ₗ[k]
      LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑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.ρ.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)

Tactic:
ext