awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₁ : c'.ι.app j ≫ g = (F.obj j).obj (P := Over.isMono X).hom
⊢ c.ι.app j ≫ hc.desc c' ≫ g = c.ι.app j ≫ f
have rw₂ : (F.obj j).obj (P := Over.isMono X).hom = (F.obj j).obj (P := Over.isMono X).hom
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
⊢ ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk f
have a : ∀ (i : J), Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤ Subobject.mk f
Tactic: rw [iSup_le_iff]
-- 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)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
⊢ IsColimit (F := (F ⋙ MonoOver.forget X) ⋙ Over.forget X) (Functor.mapCocone (Over.forget X) c)
have this : Mono f
Tactic: haveI := mono_of_isColimit_monoOver F (colimit.isColimit _) f (by simp [f])
-- 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)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this : Mono f
⊢ IsColimit (F := (F ⋙ MonoOver.forget X) ⋙ Over.forget X) (Functor.mapCocone (Over.forget X) c)
have this₁ : Subobject.mk f = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
Tactic: have := subobjectMk_of_isColimit_eq_iSup F (colimit.isColimit _) f (by simp [f])
-- 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)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
⊢ IsColimit (F := (F ⋙ MonoOver.forget X) ⋙ Over.forget X) (Functor.mapCocone (Over.forget X) c)
have this₁ : Subobject.mk f = Subobject.mk c.pt.hom
Tactic: rw [← h] at this
Cleared hypotheses: this
-- 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)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
⊢ IsColimit (F := (F ⋙ MonoOver.forget X) ⋙ Over.forget X) (Functor.mapCocone (Over.forget X) c)
have refine : ∀ (j : J),
  (colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom =
    NatTrans.app (Cocone.ι (Functor.mapCocone (Over.forget X) c)) j
Tactic: refine IsColimit.ofIsoColimit (colimit.isColimit _)
    (Cocone.ext (Subobject.isoOfMkEqMk _ _ this) (fun j ↦ ?_))
-- 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)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ (colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom =
    NatTrans.app (Cocone.ι (Functor.mapCocone (Over.forget X) c)) j
have rw : ((colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom) ≫
    c.pt.hom =
  NatTrans.app (Cocone.ι (Functor.mapCocone (Over.forget X) c)) j ≫ c.pt.hom
Tactic: rw [← cancel_mono (c.pt.hom)]
-- 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)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ ((colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom) ≫
      c.pt.hom =
    NatTrans.app (Cocone.ι (Functor.mapCocone (Over.forget X) c)) j ≫ c.pt.hom
have dsimp : (colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ Subobject.ofMkLEMk f c.pt.hom sorry) ≫ c.pt.hom =
  Over.Hom.left (c.ι.app j) ≫ c.pt.hom
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)
inst_5 : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun (j : J) ↦ (F.obj j).obj (P := Over.isMono X).hom, naturality := ⋯ } }
this_1 : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ (colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ Subobject.ofMkLEMk f c.pt.hom ⋯) ≫ c.pt.hom =
    Over.Hom.left (c.ι.app j) ≫ c.pt.hom
have rw : colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ f = (F.obj j).obj (P := Over.isMono X).hom
Tactic: rw [Category.assoc, Subobject.ofMkLEMk_comp, Over.w]
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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
h : Epi f
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom
have this : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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
h : Epi f
this : IsFiltered J
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom
have this₁ : Mono f
Tactic: have := mono_of_isColimit_monoOver F hc f hf
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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
h : Epi f
this_1 : IsFiltered J
this : Mono f
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom
have h₁ : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
Tactic: rw [Subobject.epi_iff_mk_eq_top f,
    subobjectMk_of_isColimit_eq_iSup F hc f hf] at h
Cleared hypotheses: h
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom
have h' : Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
  Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) sorry
Tactic: have h' : Function.Surjective (fun (j : J) ↦ (⟨s j, _, rfl⟩ : Set.range s)) := by
    rintro ⟨_, j, rfl⟩
    exact ⟨j, rfl⟩
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom
have obtain : ∀ (σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J)
  (hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) sorry),
  ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom
Tactic: obtain ⟨σ, hσ⟩ := h'.hasRightInverse
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom
have hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
Tactic: have hs : HasCardinalLT (Set.range s) κ :=
    hXκ.of_injective (f := Subtype.val) Subtype.val_injective
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
⊢ ∃ (j : J), IsIso (F.obj j).obj (P := Over.isMono X).hom
have refine : IsIso (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom
Tactic: refine ⟨IsCardinalFiltered.max σ hs, ?_⟩
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
⊢ IsIso (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom
have rw : ∀ (i : J),
  Subobject.mk (F.obj i).obj (P := Over.isMono X).hom ≤
    Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom
Tactic: rw [Subobject.isIso_iff_mk_eq_top, ← top_le_iff, ← h, iSup_le_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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
j : J
t : (↑(Set.range s) : Type (max u v)) := Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
⊢ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤
    Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom
have trans : Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk (F.obj (σ t)).obj (P := Over.isMono X).hom
Tactic: trans Subobject.mk (F.obj (σ t)).obj.hom
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
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_1 : IsFiltered J
this : Mono f
h : Eq (α := Subobject.{v, u} X) (⨆ (j : J), Subobject.mk (F.obj j).obj (P := Over.isMono X).hom) ⊤
s : (j : J) → Subobject.{v, u} X := fun (j : J) ↦ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom
h' :
  Function.Surjective (β := { x : Subobject.{v, u} X // x ∈ Set.range s }) fun (j : J) ↦
    Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
σ : { x : Subobject.{v, u} X // x ∈ Set.range s } → J
hσ : Function.RightInverse σ fun (j : J) ↦ Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
hs : HasCardinalLT (↑(Set.range s) : Type (max u v)) κ
j : J
t : (↑(Set.range s) : Type (max u v)) := Subtype.mk (p := fun (x : Subobject.{v, u} X) ↦ x ∈ Set.range s) (s j) ⋯
trans : Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤ Subobject.mk (F.obj (σ t)).obj (P := Over.isMono X).hom
⊢ Subobject.mk (F.obj j).obj (P := Over.isMono X).hom ≤
    Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom
have trans₁ : Subobject.mk (F.obj (σ t)).obj (P := Over.isMono X).hom ≤
  Subobject.mk (F.obj (IsCardinalFiltered.max σ hs)).obj (P := Over.isMono X).hom
Tactic: trans Subobject.mk (F.obj (σ t)).obj.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ Eq (α := kernel f ⟶ Abelian.image f) (kernel.ι f ≫ kernel.lift (cokernel.π f) f ⋯) 0
have h : Eq (α := kernel f ⟶ Q)
  (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) (kernel.ι f ≫ kernel.lift (cokernel.π f) f sorry)
    (equalizer.ι (cokernel.π f) 0))
  (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) 0 (equalizer.ι (cokernel.π f) 0))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ Eq (α := Abelian.coimage f ⟶ cokernel f) (cokernel.desc (kernel.ι f) f ⋯ ≫ cokernel.π f) 0
have h : Eq (α := P ⟶ cokernel f)
  (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
    (cokernel.desc (kernel.ι f) f sorry ≫ cokernel.π f))
  (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Q : C
f : P ⟶ Q
inst_2 : HasCokernel f
inst_3 : HasKernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : HasCokernel (X := kernel f) (kernel.ι f)
⊢ Eq (α := Abelian.coimage f ⟶ Abelian.image f) (coimageImageComparison f) (coimageImageComparison' f)
have h : CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
    (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (coimageImageComparison f))
    (equalizer.ι (cokernel.π f) 0) =
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
    (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (coimageImageComparison' f))
    (equalizer.ι (cokernel.π f) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Indization (goal)
Goal:
C : Type v
inst : SmallCategory C
inst_1 : Abelian C
X Y : Ind C
f : X ⟶ Y
⊢ IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
have obtain : ∀ (I : Type v) (w : SmallCategory I) (w_1 : IsFiltered I) (F G : I ⥤ C) (ϕ : F ⟶ G)
  (i : Arrow.mk f ≅ Arrow.mk (X := Functor.obj (Ind.lim I) F) (Functor.map (Ind.lim I) ϕ)),
  IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
Tactic: obtain ⟨I, _, _, F, G, ϕ, ⟨i⟩⟩ := Ind.exists_nonempty_arrow_mk_iso_ind_lim (f := f)