awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A : Rep k G
x : (↑A : Type (max u v))
g : G
h :
  ∀ (a : G),
    Eq (α := (↑A : Type (max u v)))
      (((((Finsupp.lift (↑A : Type (max u v)) k G :
                  (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
                fun (g : G) ↦
                (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
                      (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
                    (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
                  x) ∘ₗ
              (Representation.ofMulAction k G G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → (↑A : Type (max u v)))
        1)
      ((((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g ∘ₗ
              (Finsupp.lift (↑A : Type (max u v)) k G :
                  (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
                fun (g : G) ↦
                (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
                      (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
                    (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
                  x) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → (↑A : Type (max u v)))
        1)
⊢ Eq (α := (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
    (((Finsupp.lift (↑A : Type (max u v)) k G : (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
        fun (g : G) ↦
        (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
              (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
            (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
          x) ∘ₗ
      (Representation.ofMulAction k G G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g)
    ((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g ∘ₗ
      (Finsupp.lift (↑A : Type (max u v)) k G : (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
        fun (g : G) ↦
        (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
              (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
            (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
          x)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A : Rep k G
x : (↑A : Type (max u v))
g a : G
⊢ Eq (α := (↑A : Type (max u v)))
    (((((Finsupp.lift (↑A : Type (max u v)) k G :
                (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
              fun (g : G) ↦
              (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
                    (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
                  (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
                x) ∘ₗ
            (Representation.ofMulAction k G G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → (↑A : Type (max u v)))
      1)
    ((((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g ∘ₗ
            (Finsupp.lift (↑A : Type (max u v)) k G :
                (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
              fun (g : G) ↦
              (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
                    (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
                  (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
                x) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → (↑A : Type (max u v)))
      1)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A : Rep k G
g : G
x : (↑A : Type (max u v))
r : k
⊢ (Hom.hom (A.leftRegularHom x) : (a : (↑(leftRegular k G) : Type (max u v))) → (↑A : Type (max u v)))
      (Finsupp.single g r) =
    HSMul.hSMul (β := (↑A : Type (max u v))) r
      ((((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
              (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
            (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
          x :
        (↑A : Type (max u v)))

Tactic:
simp [leftRegularHom]

Premises used: Rep.leftRegularHom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A : Rep.{w, u, v} k G
⊢ Functor.obj
      (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
        (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
        ModuleCat.carrier))
      A =
    ModuleCat.of k (↑A : Type w)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f : A ⟶ B
⊢ CategoryTheory.Functor.map
      (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
        (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
        ModuleCat.carrier))
      f =
    ModuleCat.ofHom (Hom.hom f).toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
⊢ Functor.Faithful
    (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
      (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
      ModuleCat.carrier))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C X Y : Rep.{w, u, v} k G
f : X ⟶ Y
g : G
⊢ Eq (α :=
    (↑(Action.V (G := G)
            { V := ModuleCat.of k (↑X : Type w),
              ρ :=
                MonoidHom.comp
                  (RingEquiv.toMonoidHom (RingEquiv.symm (ModuleCat.endRingEquiv (ModuleCat.of k (↑X : Type w)))))
                  X.ρ }) :
        Type w) →ₗ[k]
      (↑(Action.V (G := G)
            { V := ModuleCat.of k (↑Y : Type w),
              ρ :=
                MonoidHom.comp
                  (RingEquiv.toMonoidHom (RingEquiv.symm (ModuleCat.endRingEquiv (ModuleCat.of k (↑Y : Type w)))))
                  Y.ρ }) :
        Type w))
    (ModuleCat.Hom.hom
      ((Action.ρ
              { V := ModuleCat.of k (↑X : Type w),
                ρ :=
                  MonoidHom.comp
                    (RingEquiv.toMonoidHom (RingEquiv.symm (ModuleCat.endRingEquiv (ModuleCat.of k (↑X : Type w)))))
                    X.ρ } :
            (a : G) →
              End
                { V := ModuleCat.of k (↑X : Type w),
                    ρ := (ModuleCat.of k (↑X : Type w)).endRingEquiv.symm.toMonoidHom.comp X.ρ }.V)
          g ≫
        Hom.toModuleCatHom f))
    (ModuleCat.Hom.hom
      (Hom.toModuleCatHom f ≫
        (Action.ρ
              { V := ModuleCat.of k (↑Y : Type w),
                ρ :=
                  MonoidHom.comp
                    (RingEquiv.toMonoidHom (RingEquiv.symm (ModuleCat.endRingEquiv (ModuleCat.of k (↑Y : Type w)))))
                    Y.ρ } :
            (a : G) →
              End
                { V := ModuleCat.of k (↑Y : Type w),
                    ρ := (ModuleCat.of k (↑Y : Type w)).endRingEquiv.symm.toMonoidHom.comp Y.ρ }.V)
          g))

Tactic:
simp [ModuleCat.endRingEquiv, f.hom.2]

Premises used: ModuleCat.endRingEquiv, Representation.IntertwiningMap.isIntertwining', Rep.Hom.hom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
X : Rep.{w, u, v} k G
⊢ Functor.obj (RepToAction k G) X =
    { V := ModuleCat.of k (↑X : Type w),
      ρ :=
        MonoidHom.comp (RingEquiv.toMonoidHom (RingEquiv.symm (ModuleCat.endRingEquiv (ModuleCat.of k (↑X : Type w)))))
          X.ρ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
X Y : Action (ModuleCat.{w, u} k) G
f : X ⟶ Y
g : G
⊢ ModuleCat.Hom.hom f.hom ∘ₗ
      (X.V.endRingEquiv.toMonoidHom.comp X.ρ : (a : G) → (↑X.V : Type w) →ₗ[k] (↑X.V : Type w)) g =
    (Y.V.endRingEquiv.toMonoidHom.comp Y.ρ : (a : G) → (↑Y.V : Type w) →ₗ[k] (↑Y.V : Type w)) g ∘ₗ
      ModuleCat.Hom.hom f.hom

Tactic:
simpa using ModuleCat.hom_ext_iff.1 (f.comm g)

Premises used: ModuleCat.hom_ext_iff, Iff.mp, Action.Hom.comm
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A_1 B C : Rep.{w, u, v} k G
A : Action (ModuleCat.{w, u} k) G
g : G
⊢ Eq.{w + 1} (α := (Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).V ⟶ A.V)
    (((Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).ρ :
            (a : G) → End ((RepToAction k G).obj ((ActionToRep k G).obj A)).V)
          g ≫
        𝟙 (Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).V :
      (Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).V ⟶ A.V)
    (𝟙 (Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).V ≫ (A.ρ : (a : G) → End A.V) g :
      (Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).V ⟶ A.V)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A_1 B C : Rep.{w, u, v} k G
A : Action (ModuleCat.{w, u} k) G
g : G
⊢ Eq.{w + 1} (α := A.V ⟶ (Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).V)
    ((A.ρ : (a : G) → End A.V) g ≫ 𝟙 A.V : A.V ⟶ (Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).V)
    (𝟙 A.V ≫
        ((Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).ρ :
            (a : G) → End ((RepToAction k G).obj ((ActionToRep k G).obj A)).V)
          g :
      A.V ⟶ (Functor.obj (RepToAction k G) (Functor.obj (ActionToRep k G) A)).V)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C X : Rep.{w, u, v} k G
g : G
⊢ Eq.{w + 1} (α := (↑X : Type w) →ₗ[k] (↑X : Type w))
    (LinearMap.id ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g ∘ₗ LinearMap.id)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
⊢ Functor.IsEquivalence (C := Rep.{u_1, u, v} k G) (RepToAction k G)

Tactic:
repIsoAction k G |>.isEquivalence_functor

Premises used: Rep.repIsoAction, CategoryTheory.Equivalence.isEquivalence_functor, Rep.RepToAction
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
⊢ Functor.IsEquivalence (C := Action (ModuleCat.{u_1, u} k) G) (ActionToRep k G)

Tactic:
repIsoAction k G |>.isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, Rep.repIsoAction, Rep.ActionToRep
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C X Y : Rep.{w, u, v} k G
f g : X ⟶ Y
⊢ ModuleCat.Hom.hom
      (CategoryTheory.Functor.map
        (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
          (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
          ModuleCat.carrier))
        (f + g)) =
    ModuleCat.Hom.hom
      (HAdd.hAdd (α :=
        Functor.obj
            (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
              (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
              ModuleCat.carrier))
            X ⟶
          Functor.obj
            (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
              (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
              ModuleCat.carrier))
            Y)
        (CategoryTheory.Functor.map
          (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
            (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
            ModuleCat.carrier))
          f)
        (CategoryTheory.Functor.map
          (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
            (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
            ModuleCat.carrier))
          g))

Tactic:
simp [add_hom]

Premises used: Rep.add_hom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
⊢ Limits.PreservesLimitsOfSize.{w, w, w, w, max (max u v) (w + 1), max u (w + 1)}
    (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
      (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
      ModuleCat.carrier))

Tactic:
Limits.preservesLimits_of_natIso (forgetNatIsoActionForget k G).symm

Premises used: Rep.forgetNatIsoActionForget, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesLimits_of_natIso
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
⊢ Limits.PreservesColimitsOfSize.{w, w, w, w, max (max u v) (w + 1), max u (w + 1)}
    (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
      (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
      ModuleCat.carrier))

Tactic:
Limits.preservesColimits_of_natIso (forgetNatIsoActionForget k G).symm

Premises used: Rep.forgetNatIsoActionForget, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesColimits_of_natIso
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f : A ⟶ B
⊢ Epi f ↔
    Function.Surjective (α := (↑A : Type w)) (β := (↑B : Type w)) (⇑(Hom.hom f) : (a : (↑A : Type w)) → (↑B : Type w))

Tactic:
⟨fun _ => (ModuleCat.epi_iff_surjective ((forget₂ _ _).map f)).1 inferInstance,
  fun h => (forget₂ _ _).epi_of_epi_map ((ModuleCat.epi_iff_surjective <|
    (forget₂ _ _).map f).2 h)⟩

Premises used: Iff.mpr, ModuleCat, ModuleCat.epi_iff_surjective, inferInstance, CategoryTheory.Functor.map, CategoryTheory.forget₂, Rep, Iff.intro, Iff.mp, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f : A ⟶ B
⊢ Mono f ↔
    Function.Injective (α := (↑A : Type w)) (β := (↑B : Type w)) (⇑(Hom.hom f) : (a : (↑A : Type w)) → (↑B : Type w))

Tactic:
⟨fun _ => (ModuleCat.mono_iff_injective ((forget₂ _ _).map f)).1 inferInstance,
  fun h => (forget₂ _ _).mono_of_mono_map ((ModuleCat.mono_iff_injective <|
    (forget₂ _ _).map f).2 h)⟩

Premises used: Iff.mpr, ModuleCat, inferInstance, ModuleCat.mono_iff_injective, CategoryTheory.Functor.map, CategoryTheory.forget₂, Rep, Iff.intro, Iff.mp, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f : A ⟶ B
inst_2 : Mono f
⊢ Mono (Hom.toModuleCatHom f)

Tactic:
inferInstanceAs <| Mono ((forget₂ _ _).map f)

Premises used: _private.0.Rep.instMonoModuleCatToModuleCatHom._proof_1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f : A ⟶ B
inst_2 : Epi f
⊢ Epi (Hom.toModuleCatHom f)

Tactic:
inferInstanceAs <| Epi ((forget₂ _ _).map f)

Premises used: _private.0.Rep.instEpiModuleCatToModuleCatHom._proof_1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommSemiring k
inst_1 : Monoid G
M N : Type w
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module k M
inst_5 : Module k N
σ : Representation k G M
ρ : Representation k G N
f : σ.IntertwiningMap ρ
r : k
⊢ ofHom (r • f) = r • ofHom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommSemiring k
inst_1 : Monoid G
M N : Rep.{u_1, u, v} k G
f : M ⟶ N
r : k
⊢ Hom.hom (r • f) = r • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommSemiring k
inst_1 : Monoid G
M N O : Rep.{u_1, u, v} k G
r : k
f : M ⟶ N
g : N ⟶ O
hf : Hom.hom ((r • f) ≫ g) = Hom.hom (r • f ≫ g)
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommSemiring k
inst_1 : Monoid G
M N O : Rep.{u_1, u, v} k G
r : k
f : M ⟶ N
g : N ⟶ O
⊢ Hom.hom ((r • f) ≫ g) = Hom.hom (r • f ≫ g)

Tactic:
simp [smul_hom, Representation.IntertwiningMap.comp_smul]

Premises used: Rep.smul_hom, Representation.IntertwiningMap.comp_smul
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommSemiring k
inst_1 : Monoid G
M N O : Rep.{u_1, u, v} k G
f : M ⟶ N
r : k
g : N ⟶ O
hf :
  ∀ (x : (↑M : Type u_1)),
    Eq (α := (↑O : Type u_1))
      (((Hom.hom (f ≫ (r • g))).toLinearMap : (a : (↑M : Type u_1)) → (↑O : Type u_1)) x : (↑O : Type u_1))
      (((Hom.hom (r • f ≫ g)).toLinearMap : (a : (↑M : Type u_1)) → (↑O : Type u_1)) x : (↑O : Type u_1))
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommSemiring k
inst_1 : Monoid G
M N O : Rep.{u_1, u, v} k G
f : M ⟶ N
r : k
g : N ⟶ O
x : (↑M : Type u_1)
⊢ Eq (α := (↑O : Type u_1))
    (((Hom.hom (f ≫ (r • g))).toLinearMap : (a : (↑M : Type u_1)) → (↑O : Type u_1)) x : (↑O : Type u_1))
    (((Hom.hom (r • f ≫ g)).toLinearMap : (a : (↑M : Type u_1)) → (↑O : Type u_1)) x : (↑O : Type u_1))

Tactic:
simp [smul_hom, Representation.IntertwiningMap.smul_comp]

Premises used: Rep.smul_hom, Representation.IntertwiningMap.smul_comp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommSemiring k
inst_1 : Monoid G
M N : Rep.{u_1, u, v} k G
⊢ ∀ (c : k) (x : M ⟶ N),
    ({ toFun := Hom.hom, map_zero' := ⋯, map_add' := ⋯ } : (a : M ⟶ N) → M.ρ.IntertwiningMap N.ρ) (c • x) =
      HSMul.hSMul (β := M.ρ.IntertwiningMap N.ρ) c
        (({ toFun := Hom.hom, map_zero' := ⋯, map_add' := ⋯ : (M ⟶ N) →+ M.ρ.IntertwiningMap N.ρ } :
              (a : M ⟶ N) → M.ρ.IntertwiningMap N.ρ)
            x :
          M.ρ.IntertwiningMap N.ρ)

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₂ X₃ Y₁ Y₂ Y₃ : Rep k G
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : X₃ ⟶ Y₃
x_3 : (↑X₁ : Type u)
x_4 : (↑X₂ : Type u)
x_5 : (↑X₃ : Type u)
⊢ Eq (α := (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            (Hom.hom
                                (ofHom ((Hom.hom (ofHom ((Hom.hom x).tensor (Hom.hom x_1)))).tensor (Hom.hom x_2)) ≫
                                  (mkIso (assoc Y₁.ρ Y₂.ρ Y₃.ρ)).hom)).toLinearMap) :
                        (↑X₁ : Type u) →ₗ[k]
                          (↑X₂ : Type u) →ₗ[k]
                            (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
                      (a : (↑X₁ : Type u)) →
                        (↑X₂ : Type u) →ₗ[k]
                          (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
                    x_3 :
                  (↑X₂ : Type u) →ₗ[k] (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
                (a : (↑X₂ : Type u)) → (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
              x_4 :
            (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
          (a : (↑X₃ : Type u)) → (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
        x_5 :
      (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            (Hom.hom
                                ((mkIso (assoc X₁.ρ X₂.ρ X₃.ρ)).hom ≫
                                  ofHom
                                    ((Hom.hom x).tensor
                                      (Hom.hom (ofHom ((Hom.hom x_1).tensor (Hom.hom x_2))))))).toLinearMap) :
                        (↑X₁ : Type u) →ₗ[k]
                          (↑X₂ : Type u) →ₗ[k]
                            (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
                      (a : (↑X₁ : Type u)) →
                        (↑X₂ : Type u) →ₗ[k]
                          (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
                    x_3 :
                  (↑X₂ : Type u) →ₗ[k] (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
                (a : (↑X₂ : Type u)) → (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
              x_4 :
            (↑X₃ : Type u) →ₗ[k] (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u)) :
          (a : (↑X₃ : Type u)) → (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))
        x_5 :
      (↑(of (Y₁.ρ.tprod (of (Y₂.ρ.tprod Y₃.ρ)).ρ)) : Type u))

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
x : X ⟶ Y
hf :
  ∀ (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))
⊢ Eq (α :=
    of (X := TensorProduct k (↑(trivial k G k) : Type u) (↑X : Type u)) (Representation.tprod (ρ (trivial k G k)) X.ρ) ⟶
      Y)
    (ofHom (lTensor (ρ (trivial k G k)) (Hom.hom x)) ≫ Iso.hom (mkIso (lid k Y.ρ))) (Iso.hom (mkIso (lid k X.ρ)) ≫ x)

Tactic:
ext