awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (hypothesis)
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
⊢ PreservesFiniteLimits.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
have this : Functor.PreservesInjectiveObjects.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
Tactic: have := preservesInjectiveObjects G hG
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (hypothesis)
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 : Functor.PreservesInjectiveObjects.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
⊢ PreservesFiniteLimits.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
have this₁ : Functor.PreservesMonomorphisms.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
Tactic: have : (tensorObj G).PreservesMonomorphisms :=
    (tensorObj G).preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects
      (tensorObjPreadditiveCoyonedaObjAdjunction G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (hypothesis)
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)
⊢ PreservesFiniteLimits.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
have this₁ : PreservesBinaryBiproducts.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
Tactic: have : PreservesBinaryBiproducts (tensorObj G) :=
    preservesBinaryBiproducts_of_preservesBinaryCoproducts _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (hypothesis)
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)
⊢ PreservesFiniteLimits.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
have this₁ : Functor.Additive.{v, v + 1, v, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
Tactic: have : (tensorObj G).Additive := Functor.additive_of_preservesBinaryBiproducts _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (hypothesis)
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)
⊢ PreservesFiniteLimits.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)
have this₁ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite (goal)
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
have 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))
Tactic: refine ⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite (hypothesis)
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 := 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))
have 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)
Tactic: have h := (isSeparator_iff_epi (projectiveSeparator C)).1
    isSeparator_projectiveSeparator (F.obj X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite (goal)
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 := 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))
have 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))))
Tactic: suffices Epi (Sigma.desc (Pi.single X (𝟙 _))) from epi_comp' this h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite (goal)
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
have 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))
Tactic: classical
  refine ⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩
  have h := (isSeparator_iff_epi (projectiveSeparator C)).1
    isSeparator_projectiveSeparator (F.obj X)
  suffices Epi (Sigma.desc (Pi.single X (𝟙 _))) from epi_comp' this h
  exact SplitEpi.epi ⟨Sigma.ι (fun (X : D) => ∐ fun _ => projectiveSeparator C) X, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite (goal)
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
have refine₁ : ∀
  (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 := 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: classical
  refine ⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩
  have h := (isSeparator_iff_epi (projectiveSeparator C)).1
    isSeparator_projectiveSeparator (F.obj X)
  suffices Epi (Sigma.desc (Pi.single X (𝟙 _))) from epi_comp' this h
  exact SplitEpi.epi ⟨Sigma.ι (fun (X : D) => ∐ fun _ => projectiveSeparator C) X, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite (goal)
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))
refine₁ :
  ∀
    (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 := 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
have refine₂ : ∀
  (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: classical
  refine ⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩
  have h := (isSeparator_iff_epi (projectiveSeparator C)).1
    isSeparator_projectiveSeparator (F.obj X)
  suffices Epi (Sigma.desc (Pi.single X (𝟙 _))) from epi_comp' this h
  exact SplitEpi.epi ⟨Sigma.ι (fun (X : D) => ∐ fun _ => projectiveSeparator C) X, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite (goal)
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} (generator F)
have apply : 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 _ Classical.ofNonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite (goal)
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} (C := Cᵒᵖ)
    (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj Classical.ofNonempty) ↦ projectiveSeparator.{v, u} C)
have apply : IsSeparator.{v, u} (projectiveSeparator.{v, u} C)
Tactic: apply isSeparator_sigma_of_isSeparator _ 0
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite (goal)
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
⊢ PreservesFiniteLimits.{v, v, u, v + 1} (D := ModuleCat (EmbeddingRing F)) (preadditiveCoyonedaObj (generator F))
have h : ∀ (J : Type v) {𝒥 : SmallCategory J} (x : FinCategory J),
  PreservesLimitsOfShape (D := ModuleCat (EmbeddingRing F)) J (preadditiveCoyonedaObj (generator F))
Tactic: apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject (hypothesis)
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 f
have this : Mono α
Tactic: have := NatTrans.mono_of_mono_app α
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject (hypothesis)
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
⊢ Subobject.mk f = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
have this : Mono f
Tactic: haveI := mono_of_isColimit_monoOver F hc f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject (goal)
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
⊢ Subobject.mk f = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
have a : Subobject.mk f ≤ ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject (goal)
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
⊢ Subobject.mk f = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
have a₁ : ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject (goal)
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
⊢ Subobject.mk f ≤ ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
have a : ∀ (b : Subobject.{v, u} X), (∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ b) → Subobject.mk f ≤ b
Tactic: rw [le_iSup_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject (goal)
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
⊢ Subobject.mk f ≤ s
have 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
Tactic: induction s using Subobject.ind with | _ g
Cleared hypotheses: s, H
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject (goal)
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_1 : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f_1 = (F.obj j).obj (P := Over.isMono X).hom
this : Mono f_1
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
j j' : J
f : j ⟶ j'
⊢ (F ⋙ MonoOver.forget X ⋙ Over.forget X).map f ≫ Subobject.ofMkLEMk (F.obj j').obj (P := Over.isMono X).hom g ⋯ =
    Subobject.ofMkLEMk (F.obj j).obj (P := Over.isMono X).hom g ⋯ ≫ Functor.map (Functor.obj (Functor.const J) A) f
have dsimp : Over.Hom.left (F.map f).hom ≫ Subobject.ofMkLEMk (F.obj j').obj (P := Over.isMono X).hom g sorry =
  Subobject.ofMkLEMk (F.obj j).obj (P := Over.isMono X).hom g sorry ≫ 𝟙 A
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject (goal)
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 : 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
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := A,
    ι := { app := fun (j : J) ↦ Subobject.ofMkLEMk (F.obj j).obj (P := Over.isMono X).hom g ⋯, naturality := ⋯ } }
j : J
⊢ c.ι.app j ≫ hc.desc c' ≫ g = c.ι.app j ≫ f
have rw : c'.ι.app j ≫ g = c.ι.app j ≫ f
Tactic: rw [hc.fac_assoc c' j, hf, Subobject.ofMkLEMk_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject (goal)
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 : 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
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := A,
    ι := { app := fun (j : J) ↦ Subobject.ofMkLEMk (F.obj j).obj (P := Over.isMono X).hom g ⋯, naturality := ⋯ } }
j : J
rw : c'.ι.app j ≫ g = c.ι.app j ≫ f
⊢ c.ι.app j ≫ hc.desc c' ≫ g = c.ι.app j ≫ f
have rw₁ : c'.ι.app j ≫ g = (F.obj j).obj (P := Over.isMono X).hom
Tactic: rw [hc.fac_assoc c' j, hf, Subobject.ofMkLEMk_comp]