awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
X Y : Action (TopModuleCat R) G
f : X ⟶ Y
⊢ Eq (α :=
    (LeftHomologyData.ofIsLimitKernelFork (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0) ⋯
          (Limits.KernelFork.ofι
            (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0))) ⋯)
          (TopModuleCat.isLimitKer
            ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0)))).K ⟶
      obj (invariants R G) Y)
    (cyclesMap'
        (CategoryTheory.Functor.map (HomologicalComplex.shortComplexFunctor (TopModuleCat R) (ComplexShape.up ℕ) 0)
          (CategoryTheory.Functor.map (homogeneousCochains.{u_1, u_2, u_3} R G) f))
        (LeftHomologyData.ofIsLimitKernelFork
          (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0) ⋯
          (Limits.KernelFork.ofι
            (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0))) ⋯)
          (TopModuleCat.isLimitKer
            ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0))))
        (LeftHomologyData.ofIsLimitKernelFork
          (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y) 0) ⋯
          (Limits.KernelFork.ofι
            (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0))) ⋯)
          (TopModuleCat.isLimitKer
            ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0)))) ≫
      (LeftHomologyData.ofIsLimitKernelFork (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y) 0)
            ⋯
            (Limits.KernelFork.ofι
              (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0)))
              ⋯)
            (TopModuleCat.isLimitKer
              ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) Y).d 0 ((ComplexShape.up ℕ).next 0)))).π ≫
        Iso.hom
          (TopModuleCat.ofIso
            (kerHomogeneousCochainsZeroEquiv R G Y ((ComplexShape.up ℕ).next 0) continuousCohomologyZeroIso._proof_2)))
    ((LeftHomologyData.ofIsLimitKernelFork (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0) ⋯
          (Limits.KernelFork.ofι
            (TopModuleCat.kerι ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0))) ⋯)
          (TopModuleCat.isLimitKer
            ((obj (homogeneousCochains.{u_1, u_2, u_3} R G) X).d 0 ((ComplexShape.up ℕ).next 0)))).π ≫
      Iso.hom
          (TopModuleCat.ofIso
            (kerHomogeneousCochainsZeroEquiv R G X ((ComplexShape.up ℕ).next 0) continuousCohomologyZeroIso._proof_2)) ≫
        CategoryTheory.Functor.map (invariants R G) f)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Abelian
Goal:
k : Type u
inst : Ring k
inst_1 : IsNoetherianRing k
X Y : FGModuleCat.{u_1, u} k
f : X ⟶ Y
⊢ IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (Abelian.coimageImageComparison f)

Tactic:
have := IsIso.of_isIso_fac_right (Abelian.PreservesCoimage.hom_coimageImageComparison
      (forget₂ (FGModuleCat k) (ModuleCat k)) f).symm
  Functor.FullyFaithful.isIso_of_isIso_map (ModuleCat.isFG k).fullyFaithfulι _

Premises used: ModuleCat, ModuleCat.isFG, CategoryTheory.ObjectProperty.fullyFaithfulι, CategoryTheory.IsIso.of_isIso_fac_right, CategoryTheory.forget₂, CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map, CategoryTheory.Abelian.PreservesCoimage.hom_coimageImageComparison, FGModuleCat, Eq.symm, CategoryTheory.Abelian.coimageImageComparison
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V : ModuleCat.{v, u} R
⊢ isFG R V ↔ Module.Finite.{u, v} R (↑V : Type v)

Tactic:
Iff.rfl

Premises used: Iff.rfl, ModuleCat.isFG
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : FGModuleCat.{v, u} R
⊢ (↑(M.obj (P := ModuleCat.isFG R)) : Type v) = (↑M : Type v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : FGModuleCat.{v, u} R
⊢ Module.Finite.{u, v} R (↑M : Type v)

Tactic:
M.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, ModuleCat.isFG
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
A B C : FGModuleCat.{v, u} R
f : A ⟶ B
g : B ⟶ C
⊢ ModuleCat.Hom.hom (f ≫ g).hom = ModuleCat.Hom.hom g.hom ∘ₗ ModuleCat.Hom.hom f.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
A : FGModuleCat.{v, u} R
⊢ ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 A)) = LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
⊢ Module.Finite.{u, v} R (↑(ModuleCat.of R PUnit.{v + 1}) : Type v)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
⊢ (↑(of R V) : Type v) = V

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V W : FGModuleCat.{v, u} R
f g : V ⟶ W
h : ModuleCat.Hom.hom f.hom = ModuleCat.Hom.hom g.hom
⊢ f = g

Tactic:
ObjectProperty.hom_ext _ (ModuleCat.hom_ext h)

Premises used: CategoryTheory.ObjectProperty.hom_ext, ModuleCat.hom_ext
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V : FGModuleCat.{v, u} R
⊢ Module.Finite.{u, v} R (↑V : Type v)

Tactic:
V.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, ModuleCat.isFG
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V W : Type v
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : Module.Finite R W
e : V ≃ₗ[R] W
h :
  ∀ (x : (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v)),
    Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
      ((ModuleCat.Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y := of R W)
                  (ConcreteCategory.ofHom (FC :=
                    fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W))
                  (ConcreteCategory.ofHom (FC :=
                    fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V)))) :
            (a : (↑(of R V).obj : Type v)) → (↑(of R V).obj : Type v))
          x :
        (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
      ((ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 (of R V))) :
            (a : (↑(of R V).obj : Type v)) → (↑(of R V).obj : Type v))
          x :
        (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
⊢ Eq (α := Quiver.Hom (V := FGModuleCat.{v, u} R) (of R V) (of R V))
    (CategoryStruct.comp (Y := of R W)
      (ConcreteCategory.ofHom (FC :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W))
      (ConcreteCategory.ofHom (FC :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V)))
    (𝟙 (of R V))

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V W : Type v
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : Module.Finite R W
e : V ≃ₗ[R] W
x : (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v)
⊢ Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
    ((ModuleCat.Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := of R W)
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W))
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V)))) :
          (a : (↑(of R V).obj : Type v)) → (↑(of R V).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
    ((ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 (of R V))) :
          (a : (↑(of R V).obj : Type v)) → (↑(of R V).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))

Tactic:
e.left_inv x

Premises used: LinearEquiv.left_inv
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V W : Type v
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : Module.Finite R W
e : V ≃ₗ[R] W
x : (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v)
⊢ Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
    ((ModuleCat.Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := of R W)
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W))
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V)))) :
          (a : (↑(of R V).obj : Type v)) → (↑(of R V).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
    ((ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 (of R V))) :
          (a : (↑(of R V).obj : Type v)) → (↑(of R V).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))

Tactic:
exact e.left_inv x

Premises used: LinearEquiv.left_inv
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V W : Type v
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : Module.Finite R W
e : V ≃ₗ[R] W
h :
  ∀ (x : (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v)),
    Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
      ((ModuleCat.Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y := of R V)
                  (ConcreteCategory.ofHom (FC :=
                    fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V))
                  (ConcreteCategory.ofHom (FC :=
                    fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v))
                    (CC := fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                    (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W)))) :
            (a : (↑(of R W).obj : Type v)) → (↑(of R W).obj : Type v))
          x :
        (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
      ((ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 (of R W))) :
            (a : (↑(of R W).obj : Type v)) → (↑(of R W).obj : Type v))
          x :
        (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
⊢ Eq (α := Quiver.Hom (V := FGModuleCat.{v, u} R) (of R W) (of R W))
    (CategoryStruct.comp (Y := of R V)
      (ConcreteCategory.ofHom (FC :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V))
      (ConcreteCategory.ofHom (FC :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W)))
    (𝟙 (of R W))

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V W : Type v
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : Module.Finite R W
e : V ≃ₗ[R] W
x : (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v)
⊢ Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
    ((ModuleCat.Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := of R V)
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V))
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W)))) :
          (a : (↑(of R W).obj : Type v)) → (↑(of R W).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
    ((ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 (of R W))) :
          (a : (↑(of R W).obj : Type v)) → (↑(of R W).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))

Tactic:
e.right_inv x

Premises used: LinearEquiv.right_inv
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
V W : Type v
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : Module.Finite R W
e : V ≃ₗ[R] W
x : (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v)
⊢ Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
    ((ModuleCat.Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := of R V)
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V))
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W)))) :
          (a : (↑(of R W).obj : Type v)) → (↑(of R W).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
    ((ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 (of R W))) :
          (a : (↑(of R W).obj : Type v)) → (↑(of R W).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))

Tactic:
exact e.right_inv x

Premises used: LinearEquiv.right_inv
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
⊢ Functor.Faithful (C := FGModuleCat.{u_1, u} R) (ulift.{u_1, u_2, u} R)

Tactic:
(fullyFaithfulULift R).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, FGModuleCat.fullyFaithfulULift
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : Ring R
⊢ Functor.Full (C := FGModuleCat.{u_1, u} R) (ulift.{u_1, u_2, u} R)

Tactic:
(fullyFaithfulULift R).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, FGModuleCat.fullyFaithfulULift
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : CommRing R
⊢ Eq.{u + 2} (α := ModuleCat R)
    (ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R)
      ((𝟙_ (FGModuleCat R)) (𝒞 := ObjectProperty.FullSubcategory.category (ModuleCat.isFG R))))
    ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : CommRing R
M N : FGModuleCat R
⊢ (tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (ModuleCat.isFG R)) M N).obj (P := ModuleCat.isFG R) =
    tensorObj (𝒞 := ModuleCat.moduleCategory R) (M.obj (P := ModuleCat.isFG R)) (N.obj (P := ModuleCat.isFG R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : CommRing R
V W : FGModuleCat.{u_1, u} R
i : V ≅ W
f : CategoryTheory.End V
⊢ Eq (α := CategoryTheory.End W) ((i.conj : (a : CategoryTheory.End V) → CategoryTheory.End W) f : CategoryTheory.End W)
    (ofHom
        (((LinearEquiv.conj.{u, u, u_1, u_1} (R₁' := R) (R₂' := R) (M₁' := (↑V : Type u_1)) (M₂' := (↑W : Type u_1))
                (σ₁'₂' := RingHom.id R) (σ₂'₁' := RingHom.id R) (isoToLinearEquiv i) :
              Module.End R (↑V : Type u_1) ≃ₗ[R] Module.End R (↑W : Type u_1)) :
            (a : Module.End R (↑V : Type u_1)) → Module.End R (↑W : Type u_1))
          (ModuleCat.Hom.hom f.hom)) :
      Quiver.Hom (V := FGModuleCat.{u_1, u} R) (of R (↑W : Type u_1)) (of R (↑W : Type u_1)))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
R : Type u
inst : CommRing R
V W : FGModuleCat.{u_1, u} R
i : V ≅ W
f : CategoryTheory.End V
⊢ Eq.{u_1 + 1} (α := (↑(W.obj (P := ModuleCat.isFG R)) : Type u_1) →ₗ[R] (↑(W.obj (P := ModuleCat.isFG R)) : Type u_1))
    (ModuleCat.Hom.hom (InducedCategory.Hom.hom ((i.conj : (a : CategoryTheory.End V) → CategoryTheory.End W) f)))
    (((LinearEquiv.conj.{u, u, u_1, u_1} (R₁' := R) (R₂' := R) (M₁' := (↑V : Type u_1)) (M₂' := (↑W : Type u_1))
            (σ₁'₂' := RingHom.id R) (σ₂'₁' := RingHom.id R) (isoToLinearEquiv i) :
          Module.End R (↑V : Type u_1) ≃ₗ[R] Module.End R (↑W : Type u_1)) :
        (a : Module.End R (↑V : Type u_1)) → Module.End R (↑W : Type u_1))
      (ModuleCat.Hom.hom f.hom))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
K : Type u
inst : Field K
V W : FGModuleCat.{v, u} K
⊢ Module.Finite.{u, v} K (V.obj (P := ModuleCat.isFG K) ⟶ W.obj (P := ModuleCat.isFG K))

Tactic:
((inferInstance : Module.Finite K (V →ₗ[K] W))).equiv ModuleCat.homLinearEquiv.symm

Premises used: LinearEquiv.symm, ModuleCat.homLinearEquiv, Module.Finite.equiv
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
K : Type u
inst : Field K
V W : FGModuleCat.{v, u} K
⊢ Module.Finite.{u, v} K (V ⟶ W)

Tactic:
((inferInstance : Module.Finite K (V.obj ⟶ W.obj))).equiv
    InducedCategory.homLinearEquiv.symm

Premises used: LinearEquiv.symm, CategoryTheory.InducedCategory.homLinearEquiv, Module.Finite.equiv
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
K : Type u
inst : Field K
V W : FGModuleCat K
⊢ Functor.obj (ihom V) W = of K (V.obj (P := ModuleCat.isFG K) ⟶ W.obj (P := ModuleCat.isFG K))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
K : Type u
inst : Field K
V : FGModuleCat.{u_1, u} K
⊢ (FGModuleCatDual K V).obj (P := ModuleCat.isFG K) = ModuleCat.of K (Dual.{u, u_1} K (↑V : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.FGModuleCat.Basic
Goal:
K : Type u
inst : Field K
V : FGModuleCat K
⊢ (↑(FGModuleCatDual K V) : Type u) = Dual K (↑V : Type u)

Tactic:
rfl

Premises used: rfl