awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : Functor.PreservesInjectiveObjects.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
this : Functor.PreservesMonomorphisms.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
⊢ PreservesBinaryBiproducts.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)

Tactic:
have : PreservesBinaryBiproducts (tensorObj G) :=
    preservesBinaryBiproducts_of_preservesBinaryCoproducts _
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : Functor.PreservesInjectiveObjects.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
this_2 : Functor.PreservesMonomorphisms.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
this : PreservesBinaryBiproducts.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
⊢ Functor.Additive.{v, v + 1, v, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)

Tactic:
have : (tensorObj G).Additive := Functor.additive_of_preservesBinaryBiproducts _
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : Functor.PreservesInjectiveObjects.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
this_2 : Functor.PreservesMonomorphisms.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
this_3 : PreservesBinaryBiproducts.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
this : Functor.Additive.{v, v + 1, v, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
⊢ Functor.PreservesHomology.{v, v + 1, v, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)

Tactic:
have : (tensorObj G).PreservesHomology :=
    (tensorObj G).preservesHomology_of_preservesMonos_and_cokernels
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : Functor.PreservesInjectiveObjects.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
this_2 : Functor.PreservesMonomorphisms.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
this_3 : PreservesBinaryBiproducts.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
this_4 : Functor.Additive.{v, v + 1, v, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
this : Functor.PreservesHomology.{v, v + 1, v, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
⊢ PreservesFiniteLimits.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)

Tactic:
(tensorObj G).preservesFiniteLimits_of_preservesHomology

Premises used: CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology, CategoryTheory.IsGrothendieckAbelian.tensorObj
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : Functor.PreservesInjectiveObjects.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
this_2 : Functor.PreservesMonomorphisms.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
this_3 : PreservesBinaryBiproducts.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
this_4 : Functor.Additive.{v, v + 1, v, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
this : Functor.PreservesHomology.{v, v + 1, v, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
⊢ PreservesFiniteLimits.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)

Tactic:
exact (tensorObj G).preservesFiniteLimits_of_preservesHomology

Premises used: CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology, CategoryTheory.IsGrothendieckAbelian.tensorObj
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective.{v, u} (projectiveSeparator.{v, u} C)

Tactic:
(has_projective_separator (coseparator Cᵒᵖ) (isCoseparator_coseparator Cᵒᵖ)).choose_spec.1

Premises used: Exists.choose_spec, Opposite, CategoryTheory.isCoseparator_coseparator, _private.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator, CategoryTheory.Abelian.has_projective_separator, And.left, CategoryTheory.coseparator
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
⊢ IsSeparator.{v, u} (projectiveSeparator.{v, u} C)

Tactic:
(has_projective_separator (coseparator Cᵒᵖ) (isCoseparator_coseparator Cᵒᵖ)).choose_spec.2

Premises used: Exists.choose_spec, Opposite, CategoryTheory.isCoseparator_coseparator, _private.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator, And.right, CategoryTheory.Abelian.has_projective_separator, CategoryTheory.coseparator
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
X : D
⊢ ∃ (f : generator F ⟶ F.obj X), Epi.{v, u} (C := Cᵒᵖ) (X := generator F) (Y := F.obj X) f

Tactic:
⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, Pi.single, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
X : D
refine :
  Epi.{v, u} (C := Cᵒᵖ) (X := generator F) (Y := F.obj X)
    (CategoryStruct.comp (Y := ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
      (Sigma.desc
        (Pi.single (M := fun (b : D) ↦
          Quiver.Hom.{v, u} (V := Cᵒᵖ)
            (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj b) ↦ projectiveSeparator.{v, u} C)
            (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
          X (𝟙 (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))))
      (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f))
⊢ ∃ (f : generator F ⟶ F.obj X), Epi.{v, u} (C := Cᵒᵖ) (X := generator F) (Y := F.obj X) f

Tactic:
refine ⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
X : D
⊢ Epi.{v, u} (C := Cᵒᵖ) (X := ∐ fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C) (Y :=
    F.obj X) (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f)

Tactic:
have h := (isSeparator_iff_epi (projectiveSeparator C)).1
    isSeparator_projectiveSeparator (F.obj X)
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
X : D
h :
  Epi.{v, u} (C := Cᵒᵖ) (X := ∐ fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C) (Y :=
    F.obj X) (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f)
suffices :
  Epi.{v, u} (C := Cᵒᵖ) (X :=
    ∐ fun (X : D) ↦ ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C) (Y :=
    ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
    (Sigma.desc
      (Pi.single (M := fun (b : D) ↦
        Quiver.Hom.{v, u} (V := Cᵒᵖ) (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj b) ↦ projectiveSeparator.{v, u} C)
          (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
        X (𝟙 (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))))
⊢ Epi.{v, u} (C := Cᵒᵖ) (X := generator F) (Y := F.obj X)
    (CategoryStruct.comp (Y := ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
      (Sigma.desc
        (Pi.single (M := fun (b : D) ↦
          Quiver.Hom.{v, u} (V := Cᵒᵖ)
            (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj b) ↦ projectiveSeparator.{v, u} C)
            (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
          X (𝟙 (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))))
      (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f))

Tactic:
suffices Epi (Sigma.desc (Pi.single X (𝟙 _))) from epi_comp' this h
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
X : D
h :
  Epi.{v, u} (C := Cᵒᵖ) (X := ∐ fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C) (Y :=
    F.obj X) (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f)
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := Cᵒᵖ) (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
      (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
    (CategoryStruct.comp (Y :=
        ∐ fun (X : D) ↦ ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
        (Sigma.ι.{v, v, u} (C := Cᵒᵖ)
          (fun (X : D) ↦ ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C) X)
        (Sigma.desc
          (Pi.single (M := fun (b : D) ↦
            Quiver.Hom.{v, u} (V := Cᵒᵖ)
              (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj b) ↦ projectiveSeparator.{v, u} C)
              (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
            X (𝟙 (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)))) :
      Quiver.Hom.{v, u} (V := Cᵒᵖ) (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
        (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
    (𝟙 (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C) :
      Quiver.Hom.{v, u} (V := Cᵒᵖ) (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
        (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
X : D
h :
  Epi.{v, u} (C := Cᵒᵖ) (X := ∐ fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C) (Y :=
    F.obj X) (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f)
⊢ Epi.{v, u} (C := Cᵒᵖ) (X :=
    ∐ fun (X : D) ↦ ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C) (Y :=
    ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
    (Sigma.desc
      (Pi.single (M := fun (b : D) ↦
        Quiver.Hom.{v, u} (V := Cᵒᵖ) (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj b) ↦ projectiveSeparator.{v, u} C)
          (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
        X (𝟙 (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))))

Tactic:
exact SplitEpi.epi ⟨Sigma.ι (fun (X : D) => ∐ fun _ => projectiveSeparator C) X, by simp⟩

Premises used: CategoryTheory.Limits.Sigma.ι, _private.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator, CategoryTheory.SplitEpi.mk, CategoryTheory.Limits.sigmaObj, CategoryTheory.SplitEpi.epi
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
⊢ Projective.{v, u} (C := Cᵒᵖ)
    (∐ fun (X : D) ↦ ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
inst_4 : Nonempty D
apply :
  IsSeparator.{v, u} (C := Cᵒᵖ)
    (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj Classical.ofNonempty) ↦ projectiveSeparator.{v, u} C)
⊢ IsSeparator.{v, u} (generator F)

Tactic:
apply isSeparator_sigma_of_isSeparator _ Classical.ofNonempty

Premises used: Classical.ofNonempty, CategoryTheory.isSeparator_sigma_of_isSeparator
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
inst_4 : Nonempty D
apply : IsSeparator.{v, u} (projectiveSeparator.{v, u} C)
⊢ IsSeparator.{v, u} (C := Cᵒᵖ)
    (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj Classical.ofNonempty) ↦ projectiveSeparator.{v, u} C)

Tactic:
apply isSeparator_sigma_of_isSeparator _ 0

Premises used: CategoryTheory.isSeparator_sigma_of_isSeparator, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
inst_4 : Nonempty D
⊢ IsSeparator.{v, u} (projectiveSeparator.{v, u} C)

Tactic:
isSeparator_projectiveSeparator

Premises used: _private.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.isSeparator_projectiveSeparator
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
inst_4 : Nonempty D
⊢ IsSeparator.{v, u} (projectiveSeparator.{v, u} C)

Tactic:
exact isSeparator_projectiveSeparator

Premises used: _private.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.isSeparator_projectiveSeparator
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
inst_4 : Nonempty D
⊢ Functor.Faithful (D := ModuleCat (EmbeddingRing F)) (embedding F)

Tactic:
(isSeparator_iff_faithful_preadditiveCoyonedaObj _).1 (isSeparator F)

Premises used: CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing, _private.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.isSeparator, CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj, CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding, Iff.mp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
inst_4 : Nonempty D
inst_5 : F.Full
⊢ Functor.Full (D := ModuleCat (EmbeddingRing F)) (F ⋙ embedding F)

Tactic:
full_comp_preadditiveCoyonedaObj _ (isSeparator F) (exists_epi F)

Premises used: CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing, _private.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.isSeparator, CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj, CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding, _private.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.exists_epi
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
h :
  ∀ (J : Type v) {𝒥 : SmallCategory J} (x : FinCategory J),
    PreservesLimitsOfShape (D := ModuleCat (EmbeddingRing F)) J (preadditiveCoyonedaObj (generator F))
⊢ PreservesFiniteLimits.{v, v, u, v + 1} (D := ModuleCat (EmbeddingRing F)) (preadditiveCoyonedaObj (generator F))

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
⊢ ∀ (J : Type v) {𝒥 : SmallCategory J} (x : FinCategory J),
    PreservesLimitsOfShape (D := ModuleCat (EmbeddingRing F)) J (preadditiveCoyonedaObj (generator F))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
⊢ PreservesFiniteColimits (D := ModuleCat (EmbeddingRing F)) (embedding F)

Tactic:
apply preservesFiniteColimits_preadditiveCoyonedaObj_of_projective

Premises used: CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
⊢ IsStableUnderTransfiniteComposition.{w, v, u} (monomorphisms C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ Functor.obj (Functor.const J) X :=
  { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ }
⊢ Mono α

Tactic:
have := NatTrans.mono_of_mono_app α
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ Functor.obj (Functor.const J) X :=
  { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ }
this : Mono α
⊢ ∀ (j : J), c.ι.app j ≫ f = α.app j ≫ NatTrans.app (Cocone.ι (constCocone J X)) j

Tactic:
simpa using hf
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ Functor.obj (Functor.const J) X :=
  { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ }
this : Mono α
⊢ Mono f

Tactic:
exact colim.map_mono' α hc (isColimitConstCocone J X) f (by simpa using hf)

Premises used: CategoryTheory.Limits.isColimitConstCocone, CategoryTheory.Limits.colim.map_mono'
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
⊢ Mono f

Tactic:
haveI := mono_of_isColimit_monoOver F hc f hf
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this : Mono f
a : Subobject.mk f ≤ ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
a₁ : ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk f
⊢ Subobject.mk f = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this : Mono f
a :
  ∀ (b : Subobject.{v, u} X), (∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ b) → Subobject.mk f ≤ b
⊢ Subobject.mk f ≤ ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom

Tactic:
rw [le_iSup_iff]

Premises used: le_iSup_iff
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
F : J ⥤ MonoOver.{v, u} X
inst_4 : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
this : Mono f
s : Subobject.{v, u} X
H : ∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ s
a :
  ∀ ⦃A : C⦄ (g : A ⟶ X) [inst_5 : Mono g]
    (H : ∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ Subobject.mk g),
    Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.mk f ≤ s

Tactic:
induction s using Subobject.ind with | _ g

Premises used: CategoryTheory.Subobject.ind