awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
v : V
g : G
h :
  ∀ (g' : G),
    Eq.{v' + 1} (α := V)
      (((((Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                  (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v) ∘ₗ
                (leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g) ∘ₗ
              Finsupp.lsingle g' :
            (a : k) → V)
          1 :
        V)
      ((((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
                (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                  (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v) ∘ₗ
              Finsupp.lsingle g' :
            (a : k) → V)
          1 :
        V)
⊢ Eq (α := (G →₀ k) →ₗ[k] V)
    (((Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
        (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v) ∘ₗ
      (leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g)
    ((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
      (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
        (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v)

Tactic:
ext g'
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
v : V
g g' : G
⊢ Eq.{v' + 1} (α := V)
    (((((Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v) ∘ₗ
              (leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g) ∘ₗ
            Finsupp.lsingle g' :
          (a : k) → V)
        1 :
      V)
    ((((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
              (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v) ∘ₗ
            Finsupp.lsingle g' :
          (a : k) → V)
        1 :
      V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
x : IntertwiningMap (leftRegular k G) σ
h :
  ∀ (a : G),
    Eq.{v' + 1} (α := V)
      ((IntertwiningMap.toLinearMap (G := G) (ρ := leftRegular k G) (σ := σ)
                ((fun (v : V) ↦
                    ({
                        toLinearMap :=
                          (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                            (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v,
                        isIntertwining' := ⋯ } :
                      IntertwiningMap (leftRegular k G) σ))
                  ((fun (f : IntertwiningMap (leftRegular k G) σ) ↦
                      ((LinearEquiv.symm (Finsupp.llift V k k G) : (a : (G →₀ k) →ₗ[k] V) → G → V) f.toLinearMap 1 : V))
                    x)) ∘ₗ
              Finsupp.lsingle a :
            (a : k) → V)
          1 :
        V)
      ((x.toLinearMap ∘ₗ Finsupp.lsingle a : (a : k) → V) 1 : V)
⊢ (fun (v : V) ↦
        ({
            toLinearMap :=
              (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v,
            isIntertwining' := ⋯ } :
          IntertwiningMap (leftRegular k G) σ))
      ((fun (f : IntertwiningMap (leftRegular k G) σ) ↦
          ((LinearEquiv.symm (Finsupp.llift V k k G) : (a : (G →₀ k) →ₗ[k] V) → G → V) f.toLinearMap 1 : V))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
x : IntertwiningMap (leftRegular k G) σ
a : G
⊢ Eq.{v' + 1} (α := V)
    ((IntertwiningMap.toLinearMap (G := G) (ρ := leftRegular k G) (σ := σ)
              ((fun (v : V) ↦
                  ({
                      toLinearMap :=
                        (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                          (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v,
                      isIntertwining' := ⋯ } :
                    IntertwiningMap (leftRegular k G) σ))
                ((fun (f : IntertwiningMap (leftRegular k G) σ) ↦
                    ((LinearEquiv.symm (Finsupp.llift V k k G) : (a : (G →₀ k) →ₗ[k] V) → G → V) f.toLinearMap 1 : V))
                  x)) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → V)
        1 :
      V)
    ((x.toLinearMap ∘ₗ Finsupp.lsingle a : (a : k) → V) 1 : V)

Tactic:
simp [← x.isIntertwining]

Premises used: Representation.IntertwiningMap.isIntertwining
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
v : V
⊢ (fun (f : IntertwiningMap (leftRegular k G) σ) ↦
        ((LinearEquiv.symm (Finsupp.llift V k k G) : (a : (G →₀ k) →ₗ[k] V) → G → V) f.toLinearMap 1 : V))
      ((fun (v : V) ↦
          ({
              toLinearMap :=
                (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                  (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v,
              isIntertwining' := ⋯ } :
            IntertwiningMap (leftRegular k G) σ))
        v) =
    v

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
G : Type v
inst : Monoid G
V : Type v'
inst_1 : AddCommMonoid V
k : Type u
inst_2 : CommSemiring k
inst_3 : Module k V
σ : Representation k G V
g : G
v : V
⊢ Eq.{v' + 1} (α := V)
    ((((σ.leftRegularMapEquiv.symm : (a : V) → (leftRegular k G).IntertwiningMap σ) v :
            IntertwiningMap (leftRegular k G) σ) :
          (a : G →₀ k) → V)
        (Finsupp.single g 1) :
      V)
    ((((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G_1 : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G_1
G : Type u
inst_3 : Monoid G
⊢ LargeCategory (FDRep R G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ ConcreteCategory (FDRep R G)
    (Action.HomSubtype (FGModuleCat R) G (FV :=
      fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
      (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
      fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
      (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
    (CC := fun (X : FDRep R G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ Preadditive (FDRep R G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ HasFiniteLimits (FDRep k G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ Linear R (FDRep R G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
V : FDRep R G
⊢ Module.Finite R (↑V.V : Type u)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
V W : FDRep k G
⊢ FiniteDimensional k (V ⟶ W)

Tactic:
FiniteDimensional.of_injective ((forget₂ (FDRep k G) (FGModuleCat k)).mapLinearMap k)
    (Functor.map_injective (forget₂ (FDRep k G) (FGModuleCat k)))

Premises used: FiniteDimensional.of_injective, CategoryTheory.Functor.mapLinearMap, FDRep, CategoryTheory.forget₂, CategoryTheory.Functor.map_injective, FGModuleCat
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V : FDRep R G
⊢ Eq (α := MonoidHom.{v, u} G (End (V.V.obj (P := ModuleCat.isFG R))))
    (MonoidHom.comp
      (↑V.V.obj (P := ModuleCat.isFG R).endRingEquiv.symm :
        ((↑V.V.obj : Type u) →ₗ[R] (↑V.V.obj : Type u)) →* End V.V.obj)
      V.ρ)
    (MonoidHom.comp (MulEquiv.toMonoidHom InducedCategory.endEquiv) V.ρ)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, rfl
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V : FDRep R G
⊢ MonoidHom.comp
      (↑V.V.obj (P := ModuleCat.isFG R).endRingEquiv : End V.V.obj →* (↑V.V.obj : Type u) →ₗ[R] (↑V.V.obj : Type u))
      (MonoidHom.comp (MulEquiv.toMonoidHom InducedCategory.endEquiv) V.ρ) =
    V.ρ

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, CategoryTheory.End, MulEquiv.toMonoidHom, FDRep.ρ, rfl
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V : FDRep R G
g : G
⊢ Eq.{u + 1} (α := (↑(V.V.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(V.V.obj (P := ModuleCat.isFG R)) : Type u))
    (ModuleCat.Hom.hom (InducedCategory.Hom.hom ((V.ρ : (a : G) → End V.V) g)))
    ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[R] (↑V.V : Type u)) g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
rw :
  Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
      Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := V.V) (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i))
          (CategoryStruct.comp (Y := V.V) ((V.ρ : (a : G) → End V.V) g)
            (Iso.hom (Functor.mapIso (Action.forget (FGModuleCat R) G) i)))) :
      W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))
⊢ Eq.{u + 1} (α := (↑W.V : Type u) →ₗ[R] (↑W.V : Type u))
    ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g : (↑W.V : Type u) →ₗ[R] (↑W.V : Type u))
    (((isoToLinearEquiv i).conj : (a : Module.End R (↑V.V : Type u)) → Module.End R (↑W.V : Type u))
        ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[R] (↑V.V : Type u)) g) :
      Module.End R (↑W.V : Type u))

Tactic:
rw [FDRep.isoToLinearEquiv, ← hom_hom_action_ρ V, ← FGModuleCat.Iso.conj_hom_eq_conj,
    Iso.conj_apply, ← ModuleCat.hom_ofHom (W.ρ g), ← ModuleCat.hom_ext_iff]

Premises used: FDRep.hom_hom_action_ρ, FDRep.isoToLinearEquiv, ModuleCat.hom_ext_iff, ModuleCat.hom_ofHom, DFunLike.coe, FGModuleCat.Iso.conj_hom_eq_conj, FDRep.ρ, CategoryTheory.Iso.conj_apply
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
dsimp :
  Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
      Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := V.V) (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i))
          ((V.ρ : (a : G) → End V.V) g ≫ i.hom.hom)) :
      W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))
⊢ Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
      Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := V.V) (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i))
          (CategoryStruct.comp (Y := V.V) ((V.ρ : (a : G) → End V.V) g)
            (Iso.hom (Functor.mapIso (Action.forget (FGModuleCat R) G) i)))) :
      W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))

Tactic:
dsimp only [Action.forget_map, Functor.mapIso_hom]

Premises used: CategoryTheory.Functor.mapIso_hom, Action.forget_map
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
rw :
  Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
      Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (InducedCategory.Hom.hom
        (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i) ≫ i.hom.hom ≫ (W.ρ : (a : G) → End W.V) g) :
      W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))
⊢ Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
      Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := V.V) (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i))
          ((V.ρ : (a : G) → End V.V) g ≫ i.hom.hom)) :
      W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))

Tactic:
rw [i.hom.comm g]

Premises used: CategoryTheory.Iso.hom, Action.Hom.comm
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V : Type u
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Module.Finite R V
ρ : MonoidHom.{v, u} G (V →ₗ[R] V)
⊢ (of ρ).ρ = ρ

Tactic:
rfl

Premises used: FDRep.ρ, rfl
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
inst_3 : IsNoetherianRing R
⊢ PreservesFiniteLimits
    (forget₂ (FDRep R G) (FC :=
      Action.HomSubtype (FGModuleCat R) G (FV :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
      (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u)) (Rep R G)
      (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))

Tactic:
Limits.comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ PreservesFiniteColimits
    (forget₂ (FDRep R G) (FC :=
      Action.HomSubtype (FGModuleCat R) G (FV :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
      (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u)) (Rep R G)
      (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))

Tactic:
Limits.comp_preservesFiniteColimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ MonoidalCategory (FDRep R G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ MonoidalPreadditive (FDRep R G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ MonoidalLinear R (FDRep R G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ HasKernels (FDRep k G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
k : Type u
G : Type v
inst : Field k
inst_1 : Monoid G
inst_2 : IsAlgClosed k
V W : FDRep k G
inst_3 : Simple V
inst_4 : Simple W
⊢ finrank k (V ⟶ W) = if Nonempty.{u + 1} (V ≅ W) then 1 else 0

Tactic:
CategoryTheory.finrank_hom_simple_simple k V W

Premises used: CategoryTheory.finrank_hom_simple_simple
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
X Y : FDRep R G
f :
  Functor.obj
      (forget₂ (FDRep R G) (FC :=
        Action.HomSubtype (FGModuleCat R) G (FV :=
          fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
          fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
        (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
        (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
      X ⟶
    Functor.obj
      (forget₂ (FDRep R G) (FC :=
        Action.HomSubtype (FGModuleCat R) G (FV :=
          fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
          fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
        (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
        (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
      Y
g : G
h :
  Eq.{u + 1} (α := (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.V.obj (P := ModuleCat.isFG R)) : Type u))
    (ModuleCat.Hom.hom
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := X.V) ((X.ρ : (a : G) → CategoryTheory.End X.V) g)
          (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)))))
    (ModuleCat.Hom.hom
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := Y.V) (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap))
          ((Y.ρ : (a : G) → CategoryTheory.End Y.V) g))))
⊢ Eq.{u + 1} (α := X.V ⟶ Y.V)
    (CategoryStruct.comp (Y := X.V) ((X.ρ : (a : G) → CategoryTheory.End X.V) g)
      (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)))
    (CategoryStruct.comp (Y := Y.V) (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap))
      ((Y.ρ : (a : G) → CategoryTheory.End Y.V) g))

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
X Y : FDRep R G
f :
  Functor.obj
      (forget₂ (FDRep R G) (FC :=
        Action.HomSubtype (FGModuleCat R) G (FV :=
          fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
          fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
        (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
        (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
      X ⟶
    Functor.obj
      (forget₂ (FDRep R G) (FC :=
        Action.HomSubtype (FGModuleCat R) G (FV :=
          fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
          fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
        (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
        (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
      Y
g : G
h :
  ModuleCat.Hom.hom (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) ∘ₗ
      (X.ρ : (a : G) → (↑X.V : Type u) →ₗ[R] (↑X.V : Type u)) g =
    (Y.ρ : (a : G) → (↑Y.V : Type u) →ₗ[R] (↑Y.V : Type u)) g ∘ₗ
      ModuleCat.Hom.hom (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)
⊢ Eq.{u + 1} (α := (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.V.obj (P := ModuleCat.isFG R)) : Type u))
    (ModuleCat.Hom.hom
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := X.V) ((X.ρ : (a : G) → CategoryTheory.End X.V) g)
          (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)))))
    (ModuleCat.Hom.hom
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := Y.V) (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap))
          ((Y.ρ : (a : G) → CategoryTheory.End Y.V) g))))

Tactic:
simp only [FGModuleCat.obj_carrier, ObjectProperty.FullSubcategory.comp_hom,
      InducedCategory.homMk_hom, ModuleCat.hom_comp, hom_hom_action_ρ]

Premises used: CategoryTheory.InducedCategory.homMk_hom, FDRep.hom_hom_action_ρ, FGModuleCat.obj_carrier, CategoryTheory.ObjectProperty.FullSubcategory.comp_hom, ModuleCat.hom_comp