awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.lift
      (fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦ Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f))) ⋯
      (Subobject.mk f) ≤
    Subobject.lift
      (fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦ Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f))) ⋯
      (Subobject.mk g)
have dsimp : LE.le (α := (Subobject.{v, u} (op X))ᵒᵈ) (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)))
  (Subobject.mk (A := op (cokernel g)) (Quiver.Hom.op (cokernel.π g)))
Tactic: dsimp only [Subobject.lift_mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ LE.le (α := (Subobject.{v, u} (op X))ᵒᵈ) (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)))
    (Subobject.mk (A := op (cokernel g)) (Quiver.Hom.op (cokernel.π g)))
have refine_1 : Eq (α := A ⟶ cokernel g) (f ≫ cokernel.π g) 0
Tactic: refine Subobject.mk_le_mk_of_comm (cokernel.desc f (cokernel.π g) ?_).op ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := A ⟶ cokernel g) (f ≫ cokernel.π g) 0
⊢ LE.le (α := (Subobject.{v, u} (op X))ᵒᵈ) (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)))
    (Subobject.mk (A := op (cokernel g)) (Quiver.Hom.op (cokernel.π g)))
have refine_2 : Eq.{v + 1} (α := op (cokernel g) ⟶ op X)
  (CategoryStruct.comp (Y := op (cokernel f)) (Quiver.Hom.op (cokernel.desc f (cokernel.π g) sorry))
    (Quiver.Hom.op (cokernel.π f)))
  (Quiver.Hom.op (cokernel.π g))
Tactic: refine Subobject.mk_le_mk_of_comm (cokernel.desc f (cokernel.π g) ?_).op ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Eq (α := A ⟶ cokernel g) (f ≫ cokernel.π g) 0
have refine_1 : Eq (α := A ⟶ cokernel g) ((ofMkLEMk f g h ≫ g) ≫ cokernel.π g) 0
Tactic: rw [← Subobject.ofMkLEMk_comp h, Category.assoc, cokernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := A ⟶ cokernel g) ((ofMkLEMk f g h ≫ g) ≫ cokernel.π g) 0
⊢ Eq (α := A ⟶ cokernel g) (f ≫ cokernel.π g) 0
have refine_1₁ : Eq (α := A ⟶ cokernel g) (ofMkLEMk f g h ≫ g ≫ cokernel.π g) 0
Tactic: rw [← Subobject.ofMkLEMk_comp h, Category.assoc, cokernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := A ⟶ cokernel g) ((ofMkLEMk f g h ≫ g) ≫ cokernel.π g) 0
refine_1₁ : Eq (α := A ⟶ cokernel g) (ofMkLEMk f g h ≫ g ≫ cokernel.π g) 0
⊢ Eq (α := A ⟶ cokernel g) (f ≫ cokernel.π g) 0
have refine_1₂ : Eq (α := A ⟶ cokernel g) (ofMkLEMk f g h ≫ 0) 0
Tactic: rw [← Subobject.ofMkLEMk_comp h, Category.assoc, cokernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasCokernels.{v, u} C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := A ⟶ cokernel g) ((ofMkLEMk f g h ≫ g) ≫ cokernel.π g) 0
refine_1₁ : Eq (α := A ⟶ cokernel g) (ofMkLEMk f g h ≫ g ≫ cokernel.π g) 0
refine_1₂ : Eq (α := A ⟶ cokernel g) (ofMkLEMk f g h ≫ 0) 0
⊢ Eq (α := A ⟶ cokernel g) (f ≫ cokernel.π g) 0
have refine_1₃ : Eq.{v + 1} (α := A ⟶ cokernel g) 0 0
Tactic: rw [← Subobject.ofMkLEMk_comp h, Category.assoc, cokernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Eq (α := Subobject.{v, u} X)
    ((fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) A (i.hom ≫ g)
      hf)
    ((fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) B g hg)
have refine_1 : kernel (i.hom ≫ g).unop ≅ kernel g.unop
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
refine_1 : kernel (i.hom ≫ g).unop ≅ kernel g.unop
⊢ Eq (α := Subobject.{v, u} X)
    ((fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) A (i.hom ≫ g)
      hf)
    ((fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) B g hg)
have refine_2 : Eq (α := kernel (i.hom ≫ g).unop ⟶ X)
  (CategoryStruct.comp (Y := kernel g.unop)
    (Iso.hom
      (IsLimit.conePointUniqueUpToIso (limit.isLimit (parallelPair (g.unop ≫ i.unop.hom) 0))
        (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom sorry)))
    (kernel.ι g.unop))
  (kernel.ι (i.hom ≫ g).unop)
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Eq (α := kernel (i.hom ≫ g).unop ⟶ X)
    (CategoryStruct.comp (Y := kernel g.unop)
      (Iso.hom
        (IsLimit.conePointUniqueUpToIso (limit.isLimit (parallelPair (g.unop ≫ i.unop.hom) 0))
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom ⋯)))
      (kernel.ι g.unop))
    (kernel.ι (i.hom ≫ g).unop)
have refine_2 : Eq (α := kernel (g.unop ≫ i.hom.unop) ⟶ X)
  (CategoryStruct.comp (Y := kernel g.unop)
    (Iso.hom
      (IsLimit.conePointUniqueUpToIso (limit.isLimit (parallelPair (g.unop ≫ i.hom.unop) 0))
        (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.hom.unop sorry)))
    (kernel.ι g.unop))
  (kernel.ι (g.unop ≫ i.hom.unop))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.lift (fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) ⋯
      (Subobject.mk f) ≤
    Subobject.lift (fun (x : Cᵒᵖ) (f : x ⟶ op X) (x_1 : Mono f) ↦ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop)) ⋯
      (Subobject.mk g)
have dsimp : Subobject.mk (A := kernel f.unop) (kernel.ι f.unop) ≤ Subobject.mk (A := kernel g.unop) (kernel.ι g.unop)
Tactic: dsimp only [Subobject.lift_mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop) ≤ Subobject.mk (A := kernel g.unop) (kernel.ι g.unop)
have refine_1 : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ g.unop) 0
Tactic: refine Subobject.mk_le_mk_of_comm (kernel.lift g.unop (kernel.ι f.unop) ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ g.unop) 0
⊢ Subobject.mk (A := kernel f.unop) (kernel.ι f.unop) ≤ Subobject.mk (A := kernel g.unop) (kernel.ι g.unop)
have refine_2 : Eq (α := kernel f.unop ⟶ X)
  (CategoryStruct.comp (Y := kernel g.unop) (kernel.lift g.unop (kernel.ι f.unop) sorry) (kernel.ι g.unop))
  (kernel.ι f.unop)
Tactic: refine Subobject.mk_le_mk_of_comm (kernel.lift g.unop (kernel.ι f.unop) ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ g.unop) 0
have refine_1 : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ (ofMkLEMk g f h ≫ f).unop) 0
Tactic: rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ (ofMkLEMk g f h ≫ f).unop) 0
⊢ Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ g.unop) 0
have refine_1₁ : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ f.unop ≫ (ofMkLEMk g f h).unop) 0
Tactic: rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ (ofMkLEMk g f h ≫ f).unop) 0
refine_1₁ : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ f.unop ≫ (ofMkLEMk g f h).unop) 0
⊢ Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ g.unop) 0
have refine_1₂ : Eq (α := kernel f.unop ⟶ unop B) (0 ≫ (ofMkLEMk g f h).unop) 0
Tactic: rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X_1 ⟶ Y
inst_2 : HasKernel f_1
inst_3 : HasKernels.{v, u} C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
refine_1 : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ (ofMkLEMk g f h ≫ f).unop) 0
refine_1₁ : Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ f.unop ≫ (ofMkLEMk g f h).unop) 0
refine_1₂ : Eq (α := kernel f.unop ⟶ unop B) (0 ≫ (ofMkLEMk g f h).unop) 0
⊢ Eq (α := kernel f.unop ⟶ unop B) (kernel.ι f.unop ≫ g.unop) 0
have refine_1₃ : Eq.{v + 1} (α := kernel f.unop ⟶ unop B) 0 0
Tactic: rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasEqualizers.{v, u} C
⊢ Epi (Y := Functor.obj underlying (imageSubobject f)) (factorThruImageSubobject f)
have dsimp : Epi (Y := Functor.obj underlying (imageSubobject f)) (factorThruImage f ≫ Iso.inv (imageSubobjectIso f))
Tactic: dsimp [factorThruImageSubobject]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
k : W ⟶ X
h : (imageSubobject f).Factors (k ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ f) h = k ≫ factorThruImageSubobject f
have h₁ : (imageSubobject f).factorThru (k ≫ f) h ≫ (imageSubobject f).arrow =
  (k ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W W' : C
k : W ⟶ W'
k' : W' ⟶ X
h : (imageSubobject f).Factors (k ≫ k' ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ k' ≫ f) h = k ≫ k' ≫ factorThruImageSubobject f
have h₁ : (imageSubobject f).factorThru (k ≫ k' ≫ f) h ≫ (imageSubobject f).arrow =
  (k ≫ k' ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
⊢ Eq.{v + 1} (α := Functor.obj (C := Subobject.{v, u} Y) underlying (imageSubobject (X := X) 0) ⟶ Y)
    (arrow (imageSubobject (X := X) 0)) 0
have rw : Eq.{v + 1} (α := Functor.obj (C := Subobject.{v, u} Y) underlying (imageSubobject (X := X) 0) ⟶ Y)
  (Iso.hom (imageSubobjectIso 0) ≫ image.ι 0) 0
Tactic: rw [← imageSubobject_arrow]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f_1 : X ⟶ Y
inst_1 : HasImage f_1
inst_2 : HasEqualizers.{v, u} C
X' : C
h : X' ⟶ X
inst_3 : Epi h
f : X ⟶ Y
inst_4 : HasImage f
inst_5 : HasImage (h ≫ f)
⊢ Epi (Y := Functor.obj underlying (imageSubobject f)) ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯)
have rw : Epi (X := Functor.obj underlying (imageSubobject (h ≫ f))) (Y := Functor.obj underlying (imageSubobject f))
  (Iso.hom (underlyingIso (image.ι (h ≫ f))) ≫ image.preComp h f ≫ Iso.inv (underlyingIso (image.ι f)))
Tactic: rw [ofLE_mk_le_mk_of_comm (image.preComp h f)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f_1 : X ⟶ Y
inst_1 : HasImage f_1
inst_2 : HasEqualizers.{v, u} C
X' : C
h : X' ⟶ X
inst_3 : Epi h
f : X ⟶ Y
inst_4 : HasImage f
inst_5 : HasImage (h ≫ f)
rw :
  Epi (X := Functor.obj underlying (imageSubobject (h ≫ f))) (Y := Functor.obj underlying (imageSubobject f))
    (Iso.hom (underlyingIso (image.ι (h ≫ f))) ≫ image.preComp h f ≫ Iso.inv (underlyingIso (image.ι f)))
⊢ Epi (Y := Functor.obj underlying (imageSubobject f)) ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯)
have rw₁ : Eq (α := image (h ≫ f) ⟶ Y) (CategoryStruct.comp (Y := image f) (image.preComp h f) (image.ι f)) (image.ι (h ≫ f))
Tactic: rw [ofLE_mk_le_mk_of_comm (image.preComp h f)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
X : Subobject.{v, u} B
f : A ⟶ B
inst_1 : HasImage f
h : A ⟶ Functor.obj underlying X
w : h ≫ X.arrow = f
⊢ (Iso.hom (imageSubobjectIso f) ≫
        image.lift { I := Functor.obj underlying X, m := X.arrow, m_mono := ⋯, e := h, fac := ⋯ }) ≫
      X.arrow =
    (imageSubobject f).arrow
have rw : Iso.hom (imageSubobjectIso f) ≫
    image.lift { I := Functor.obj underlying X, m := X.arrow, m_mono := sorry, e := h, fac := sorry } ≫ X.arrow =
  (imageSubobject f).arrow
Tactic: rw [assoc, image.lift_fac, imageSubobject_arrow]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
X : Subobject.{v, u} B
f : A ⟶ B
inst_1 : HasImage f
h : A ⟶ Functor.obj underlying X
w : h ≫ X.arrow = f
rw :
  Iso.hom (imageSubobjectIso f) ≫
      image.lift { I := Functor.obj underlying X, m := X.arrow, m_mono := ⋯, e := h, fac := ⋯ } ≫ X.arrow =
    (imageSubobject f).arrow
⊢ (Iso.hom (imageSubobjectIso f) ≫
        image.lift { I := Functor.obj underlying X, m := X.arrow, m_mono := ⋯, e := h, fac := ⋯ }) ≫
      X.arrow =
    (imageSubobject f).arrow
have rw₁ : Iso.hom (imageSubobjectIso f) ≫ image.ι f = (imageSubobject f).arrow
Tactic: rw [assoc, image.lift_fac, imageSubobject_arrow]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
X : Subobject.{v, u} B
f : A ⟶ B
inst_1 : HasImage f
h : A ⟶ Functor.obj underlying X
w : h ≫ X.arrow = f
rw :
  Iso.hom (imageSubobjectIso f) ≫
      image.lift { I := Functor.obj underlying X, m := X.arrow, m_mono := ⋯, e := h, fac := ⋯ } ≫ X.arrow =
    (imageSubobject f).arrow
rw₁ : Iso.hom (imageSubobjectIso f) ≫ image.ι f = (imageSubobject f).arrow
⊢ (Iso.hom (imageSubobjectIso f) ≫
        image.lift { I := Functor.obj underlying X, m := X.arrow, m_mono := ⋯, e := h, fac := ⋯ }) ≫
      X.arrow =
    (imageSubobject f).arrow
have rw₂ : (imageSubobject f).arrow = (imageSubobject f).arrow
Tactic: rw [assoc, image.lift_fac, imageSubobject_arrow]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst_1 : HasImage f
g : Y ⟶ Z
inst_2 : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst_3 : HasImageMap sq
⊢ imageSubobjectMap sq ≫ (imageSubobject g).arrow = (imageSubobject f).arrow ≫ Arrow.Hom.right sq
have simp : Iso.hom (imageSubobjectIso f) ≫ CategoryStruct.comp (Y := image g) (image.map sq) (image.ι g) =
  (imageSubobject f).arrow ≫ Arrow.Hom.right sq
Tactic: simp only [imageSubobjectMap, Category.assoc, Arrow.mk_left, Arrow.mk_right,
    Arrow.mk_hom, imageSubobject_arrow']
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst_1 : HasImage f
g : Y ⟶ Z
inst_2 : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst_3 : HasImageMap sq
⊢ Iso.hom (imageSubobjectIso f) ≫ CategoryStruct.comp (Y := image g) (image.map sq) (image.ι g) =
    (imageSubobject f).arrow ≫ Arrow.Hom.right sq
have rw : Iso.hom (imageSubobjectIso f) ≫ image.ι f ≫ Arrow.Hom.right sq = (imageSubobject f).arrow ≫ Arrow.Hom.right sq
Tactic: rw [dsimp% image.map_ι sq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst_1 : HasImage f
g : Y ⟶ Z
inst_2 : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst_3 : HasImageMap sq
⊢ Eq (α := image (Arrow.mk f).hom ⟶ Functor.obj underlying (imageSubobject (Arrow.mk g).hom))
    (image.map sq ≫ Iso.inv (imageSubobjectIso (Arrow.mk g).hom)) (Iso.inv (imageSubobjectIso f) ≫ imageSubobjectMap sq)
have h : Eq (α := image (Arrow.mk f).hom ⟶ (Arrow.mk g).right)
  ((image.map sq ≫ Iso.inv (imageSubobjectIso (Arrow.mk g).hom)) ≫ (imageSubobject (Arrow.mk g).hom).arrow)
  ((Iso.inv (imageSubobjectIso f) ≫ imageSubobjectMap sq) ≫ (imageSubobject (Arrow.mk g).hom).arrow)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
f g : MonoOver.{v₁, u₁} X
h₁ h₂ : f ⟶ g
⊢ h₁ = h₂
have h : h₁.hom = h₂.hom
Tactic: apply InducedCategory.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
f g : MonoOver.{v₁, u₁} X
h₁ h₂ : f ⟶ g
⊢ h₁.hom = h₂.hom
have h : Over.Hom.left h₁.hom = Over.Hom.left h₂.hom
Tactic: apply Over.OverMorphism.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
f g : MonoOver.{v₁, u₁} X
h₁ h₂ : f ⟶ g
⊢ Over.Hom.left h₁.hom = Over.Hom.left h₂.hom
have h : Over.Hom.left h₁.hom ≫ g.arrow = Over.Hom.left h₂.hom ≫ g.arrow
Tactic: rw [← cancel_mono g.arrow]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
f g : MonoOver.{v₁, u₁} X
h₁ h₂ : f ⟶ g
⊢ Over.Hom.left h₁.hom ≫ g.arrow = Over.Hom.left h₂.hom ≫ g.arrow
have h : f.obj (P := Over.isMono X).hom = Over.Hom.left h₂.hom ≫ g.arrow
Tactic: erw [Over.w h₁.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
f g : MonoOver.{v₁, u₁} X
h₁ h₂ : f ⟶ g
⊢ f.obj (P := Over.isMono X).hom = Over.Hom.left h₂.hom ≫ g.arrow
have h : f.obj (P := Over.isMono X).hom = f.obj (P := Over.isMono X).hom
Tactic: erw [Over.w h₂.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
f g : MonoOver.{v₁, u₁} X
h : f.obj (P := Over.isMono X).left ≅ g.obj (P := Over.isMono X).left
w : h.hom ≫ g.arrow = f.arrow
⊢ h.inv ≫ f.arrow = g.arrow
have rw : f.arrow = h.hom ≫ g.arrow
Tactic: rw [h.inv_comp_eq, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
f g : MonoOver.{v₁, u₁} X
h : f.obj (P := Over.isMono X).left ≅ g.obj (P := Over.isMono X).left
w : h.hom ≫ g.arrow = f.arrow
rw : f.arrow = h.hom ≫ g.arrow
⊢ h.inv ≫ f.arrow = g.arrow
have rw₁ : f.arrow = f.arrow
Tactic: rw [h.inv_comp_eq, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u₃
inst_2 : Category.{v₃, u₃} J
X : C
F : Over.{v₁, u₁} X
h_1 : ObjectProperty.limitsOfShape (Over.isMono X) J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z_1 : C
g h : Z_1 ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
⊢ g = h
have refine : ∀ (j : WithTerminal J),
  g ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app j =
    h ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app j
Tactic: refine (WithTerminal.isLimitEquiv.invFun p.isLimit).hom_ext (fun j ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u₃
inst_2 : Category.{v₃, u₃} J
X : C
F : Over.{v₁, u₁} X
h_1 : ObjectProperty.limitsOfShape (Over.isMono X) J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z_1 : C
g h : Z_1 ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
⊢ Eq (α := Z_1 ⟶ (obj WithTerminal.liftFromOver p.diag).obj (WithTerminal.of j))
    (g ≫
      (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app (WithTerminal.of j))
    (h ≫
      (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app (WithTerminal.of j))
have this : Over.isMono X (p.diag.obj j)
Tactic: have := hp j