awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 ≫ (imageSubobject f).arrow =
    (k ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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)
h₁ :
  (imageSubobject f).factorThru (k ≫ k' ≫ f) h ≫ (imageSubobject f).arrow =
    (k ≫ k' ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow
⊢ (imageSubobject f).factorThru (k ≫ k' ≫ f) h = k ≫ k' ≫ factorThruImageSubobject f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 ≫ (imageSubobject f).arrow =
    (k ≫ k' ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y X' : C
h : X' ⟶ X
f : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage (h ≫ f)
⊢ Eq (α := image (h ≫ f) ⟶ Y) (CategoryStruct.comp (Y := image f) (image.preComp h f) (image.ι f)) (image.ι (h ≫ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
rw :
  Eq.{v + 1} (α := Functor.obj (C := Subobject.{v, u} Y) underlying (imageSubobject (X := X) 0) ⟶ Y)
    (Iso.hom (imageSubobjectIso 0) ≫ image.ι 0) 0
⊢ Eq.{v + 1} (α := Functor.obj (C := Subobject.{v, u} Y) underlying (imageSubobject (X := X) 0) ⟶ Y)
    (arrow (imageSubobject (X := X) 0)) 0

Tactic:
rw [← imageSubobject_arrow]

Premises used: CategoryTheory.Limits.imageSubobject_arrow
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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)
    (Iso.hom (imageSubobjectIso 0) ≫ image.ι 0) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
A B : C
⊢ Eq.{v + 1} (α := Functor.obj (C := Subobject.{v, u} B) underlying (imageSubobject (X := A) 0) ⟶ B)
    (CategoryStruct.comp (Y := Functor.obj (C := Subobject.{v, u} B) underlying ⊥)
        (Iso.hom (imageSubobjectIso 0 ≪≫ Iso.trans (Y := 0) imageZero (Iso.symm botCoeIsoZero)) :
          Quiver.Hom.{v, u} (V := C) (Functor.obj (C := Subobject.{v, u} B) underlying (imageSubobject (X := A) 0))
            (Functor.obj (C := Subobject.{v, u} B) underlying ⊥))
        (arrow ⊥ : Functor.obj (C := Subobject.{v, u} B) underlying ⊥ ⟶ B) :
      Functor.obj (C := Subobject.{v, u} B) underlying (imageSubobject (X := A) 0) ⟶ B)
    (arrow (imageSubobject (X := A) 0) :
      Functor.obj (C := Subobject.{v, u} B) underlying (imageSubobject (X := A) 0) ⟶ B)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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)))
rw₁ : Eq (α := image (h ≫ f) ⟶ Y) (CategoryStruct.comp (Y := image f) (image.preComp h f) (image.ι f)) (image.ι (h ≫ f))
⊢ Epi (Y := Functor.obj underlying (imageSubobject f)) ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯)

Tactic:
rw [ofLE_mk_le_mk_of_comm (image.preComp h f)]

Premises used: CategoryTheory.Limits.image.preComp, CategoryTheory.Subobject.ofLE_mk_le_mk_of_comm
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 (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:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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)
⊢ Eq (α := image (h ≫ f) ⟶ Y) (CategoryStruct.comp (Y := image f) (image.preComp h f) (image.ι f)) (image.ι (h ≫ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasEqualizers.{v, u} C
f : X ⟶ Y
inst_2 : HasImage f
Y' : C
h : Y ⟶ Y'
inst_3 : IsIso h
⊢ Iso.hom (imageSubobjectCompIso f h) ≫ (imageSubobject f).arrow = (imageSubobject (f ≫ h)).arrow ≫ inv h

Tactic:
simp [imageSubobjectCompIso]

Premises used: CategoryTheory.Limits.imageSubobjectCompIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasEqualizers.{v, u} C
f : X ⟶ Y
inst_2 : HasImage f
Y' : C
h : Y ⟶ Y'
inst_3 : IsIso h
⊢ Iso.inv (imageSubobjectCompIso f h) ≫ (imageSubobject (f ≫ h)).arrow = (imageSubobject f).arrow ≫ h

Tactic:
simp [imageSubobjectCompIso]

Premises used: CategoryTheory.Limits.imageSubobjectCompIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ Iso.hom (imageSubobjectIso f ≪≫ imageMonoIsoSource f ≪≫ Iso.symm (underlyingIso f)) ≫ (Subobject.mk f).arrow =
    (imageSubobject f).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasEqualizers.{v, u} C
X' : C
h : X' ⟶ X
inst_2 : IsIso h
f : X ⟶ Y
inst_3 : HasImage f
⊢ Eq (α := image f ⟶ Y) (CategoryStruct.comp (Y := image (h ≫ f)) (inv (image.preComp h f)) (image.ι (h ≫ f)))
    (image.ι f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
rw₂ rw₃ : (imageSubobject f).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

Tactic:
rw [assoc, image.lift_fac, imageSubobject_arrow]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.lift_fac, CategoryTheory.Limits.imageSubobject_arrow
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
A B X : C
g : X ⟶ B
inst_1 : Mono g
f : A ⟶ B
inst_2 : HasImage f
h : A ⟶ X
w : h ≫ g = f
⊢ (h ≫ Iso.inv (underlyingIso g)) ≫ (Subobject.mk g).arrow = f

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
simp :
  Iso.hom (imageSubobjectIso f) ≫ CategoryStruct.comp (Y := image g) (image.map sq) (image.ι g) =
    (imageSubobject f).arrow ≫ Arrow.Hom.right sq
⊢ imageSubobjectMap sq ≫ (imageSubobject g).arrow = (imageSubobject f).arrow ≫ Arrow.Hom.right sq

Tactic:
simp only [imageSubobjectMap, Category.assoc, Arrow.mk_left, Arrow.mk_right,
    Arrow.mk_hom, imageSubobject_arrow']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Arrow.mk_right, CategoryTheory.Arrow.mk_hom, CategoryTheory.Limits.imageSubobjectMap, CategoryTheory.Arrow.mk_left, CategoryTheory.Limits.imageSubobject_arrow'
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
rw : Iso.hom (imageSubobjectIso f) ≫ image.ι f ≫ Arrow.Hom.right sq = (imageSubobject f).arrow ≫ Arrow.Hom.right sq
⊢ Iso.hom (imageSubobjectIso f) ≫ CategoryStruct.comp (Y := image g) (image.map sq) (image.ι g) =
    (imageSubobject f).arrow ≫ Arrow.Hom.right sq

Tactic:
rw [dsimp% image.map_ι sq]

Premises used: CategoryTheory.Limits.image.map_ι
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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) ≫ image.ι f ≫ Arrow.Hom.right sq = (imageSubobject f).arrow ≫ Arrow.Hom.right sq

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 ⟶ (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:
simpa using image.map_ι sq

Premises used: CategoryTheory.Limits.image.map_ι
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 (α := Functor.obj underlying (imageSubobject (Arrow.mk f).hom) ⟶ image (Arrow.mk g).hom)
    (Iso.hom (imageSubobjectIso (Arrow.mk f).hom) ≫ image.map sq) (imageSubobjectMap sq ≫ Iso.hom (imageSubobjectIso g))

Tactic:
simp [imageSubobjectMap]

Premises used: CategoryTheory.Limits.imageSubobjectMap
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : MonoOver.{v₁, u₁} X
⊢ Mono S.obj (P := Over.isMono X).hom

Tactic:
S.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
f : MonoOver.{v₁, u₁} X
⊢ (obj (forget X) f).left = f.obj (P := Over.isMono X).left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A : C
f : A ⟶ X
inst_1 : Mono f
⊢ (mk f).obj (P := Over.isMono X).left = A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A : C
f : A ⟶ X
inst_1 : Mono f
⊢ (mk f).arrow = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
f : MonoOver.{v₁, u₁} X
⊢ (obj (forget X) f).hom = f.arrow

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
f : MonoOver.{v₁, u₁} X
⊢ Mono f.arrow

Tactic:
f.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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 : MonoOver.{v₁, u₁} X
⊢ Mono (obj (forget X) f).hom

Tactic:
f.mono

Premises used: CategoryTheory.MonoOver.mono
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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₁.hom = h₂.hom
⊢ h₁ = h₂

Tactic:
apply InducedCategory.hom_ext

Premises used: CategoryTheory.InducedCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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 : Over.Hom.left h₁.hom = Over.Hom.left h₂.hom
⊢ h₁.hom = h₂.hom

Tactic:
apply Over.OverMorphism.ext

Premises used: CategoryTheory.Over.OverMorphism.ext
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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 : Over.Hom.left h₁.hom ≫ g.arrow = Over.Hom.left h₂.hom ≫ g.arrow
⊢ Over.Hom.left h₁.hom = Over.Hom.left h₂.hom

Tactic:
rw [← cancel_mono g.arrow]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.MonoOver.arrow
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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 : f.obj (P := Over.isMono X).hom = Over.Hom.left h₂.hom ≫ g.arrow
⊢ Over.Hom.left h₁.hom ≫ g.arrow = Over.Hom.left h₂.hom ≫ g.arrow

Tactic:
erw [Over.w h₁.hom]

Premises used: CategoryTheory.Over.w, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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₃ : f.obj (P := Over.isMono X).hom = f.obj (P := Over.isMono X).hom
⊢ f.obj (P := Over.isMono X).hom = Over.Hom.left h₂.hom ≫ g.arrow

Tactic:
erw [Over.w h₂.hom]

Premises used: CategoryTheory.Over.w, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
f g : MonoOver.{v₁, u₁} X
k : f ⟶ g
⊢ Over.Hom.left k.hom ≫ g.arrow = f.arrow

Tactic:
Over.w _

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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
rw₁ rw₂ : f.arrow = f.arrow
⊢ h.inv ≫ f.arrow = g.arrow

Tactic:
rw [h.inv_comp_eq, w]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A B : MonoOver.{v₁, u₁} X
f : A ⟶ B
inst_2 : IsIso f
⊢ IsIso (Over.Hom.left f.hom)

Tactic:
inferInstanceAs (IsIso ((MonoOver.forget _ ⋙ Over.forget _).map f))

Premises used: _private.0.CategoryTheory.MonoOver.instIsIsoLeftHomFullSubcategoryOverIsMono._proof_1
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
A B : MonoOver.{v₁, u₁} X
f : A ⟶ B
⊢ IsIso f ↔ IsIso (Over.Hom.left f.hom)

Tactic:
(isIso_iff_of_reflects_iso _ (MonoOver.forget X ⋙ Over.forget _)).symm

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Over.forget, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.MonoOver.forget, Iff.symm
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : Over.{v₁, u₁} Y ⥤ Over.{v₁, u₁} X
h : ∀ (f : MonoOver.{v₁, u₁} Y), Mono (F.obj (obj (forget Y) f)).hom
⊢ lift F h ⋙ forget X = forget Y ⋙ F

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.comp, CategoryTheory.CostructuredArrow, CategoryTheory.inducedFunctor, CategoryTheory.MonoOver.lift, rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
Y : D
F : Over.{v₂, u₂} Y ⥤ Over.{v₁, u₁} X
h : ∀ (f : MonoOver.{v₂, u₂} Y), Mono (F.obj (obj (forget Y) f)).hom
f : MonoOver.{v₂, u₂} Y
⊢ ((lift F h).obj f).arrow = (F.obj (obj (forget Y) f)).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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

Tactic:
(WithTerminal.isLimitEquiv.invFun p.isLimit).hom_ext (fun j ↦ ?_)

Premises used: CategoryTheory.WithTerminal.isLimitEquiv, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.LimitPresentation.isLimit, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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
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
⊢ g = h

Tactic:
refine (WithTerminal.isLimitEquiv.invFun p.isLimit).hom_ext (fun j ↦ ?_)

Premises used: CategoryTheory.WithTerminal.isLimitEquiv, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.LimitPresentation.isLimit, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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
⊢ Over.isMono X (p.diag.obj j)

Tactic:
have := hp j
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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
this : Over.isMono X (p.diag.obj j)
of :
  Eq (α := Z_1 ⟶ X)
    ((g ≫
        (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app
          (WithTerminal.of j)) ≫
      (p.diag.obj j).hom)
    ((h ≫
        (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app
          (WithTerminal.of j)) ≫
      (p.diag.obj j).hom)
⊢ 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))

Tactic:
rw [← cancel_mono ((p.diag.obj j).hom)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.LimitPresentation.diag, CategoryTheory.Over.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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
this : Over.isMono X (p.diag.obj j)
⊢ Eq (α := Z_1 ⟶ X)
    ((g ≫
        (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app
          (WithTerminal.of j)) ≫
      (p.diag.obj j).hom)
    ((h ≫
        (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app
          (WithTerminal.of j)) ≫
      (p.diag.obj j).hom)

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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
⊢ Eq (α := Z_1 ⟶ (obj WithTerminal.liftFromOver p.diag).obj WithTerminal.star)
    (g ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app WithTerminal.star)
    (h ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app WithTerminal.star)

Tactic:
e
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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
⊢ Eq (α := Z_1 ⟶ (obj WithTerminal.liftFromOver p.diag).obj WithTerminal.star)
    (g ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app WithTerminal.star)
    (h ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app WithTerminal.star)

Tactic:
exact e
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
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 : WithTerminal J
of :
  ∀ (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))
star :
  Eq (α := Z_1 ⟶ (obj WithTerminal.liftFromOver p.diag).obj WithTerminal.star)
    (g ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app WithTerminal.star)
    (h ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app WithTerminal.star)
⊢ 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:
cases j with
    | of j => have := hp j; rw [← cancel_mono ((p.diag.obj j).hom)]; simpa
    | star => exact e

Premises used: CategoryTheory.Functor.star