awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ Eq (α := image f ⟶ Y) ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) (image.lift F'.ofCompIso ≫ F'.ofCompIso.m)

Tactic:
simp only [MonoFactorisation.ofCompIso_I, Category.assoc,
                MonoFactorisation.ofCompIso_m]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.MonoFactorisation.ofCompIso_m, CategoryTheory.Limits.MonoFactorisation.ofCompIso_I
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ Eq (α := image f ⟶ Y) ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) (image.lift F'.ofCompIso ≫ F'.ofCompIso.m)

Tactic:
have : (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g =
            image.lift (MonoFactorisation.ofCompIso F') ≫
            ((MonoFactorisation.ofCompIso F').m) := by
              simp only [MonoFactorisation.ofCompIso_I, Category.assoc,
                MonoFactorisation.ofCompIso_m]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
this : Eq (α := image f ⟶ Y) ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) (image.lift F'.ofCompIso ≫ F'.ofCompIso.m)
rw : image.lift F'.ofCompIso ≫ F'.ofCompIso.m = (Image.monoFactorisation f).m
rw₁ : image.ι f = (Image.monoFactorisation f).m
rw₂ rw₃ : Eq (α := image f ⟶ Y) (image.ι f) (image.ι f)
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m

Tactic:
rw [this, image.lift_fac (MonoFactorisation.ofCompIso F'), image.as_ι]

Premises used: CategoryTheory.Limits.image.lift_fac, CategoryTheory.Limits.MonoFactorisation.ofCompIso, CategoryTheory.Limits.image.as_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
w :
  CategoryStruct.comp (Y := image f) (factorThruImage f)
      (CategoryStruct.comp (Y := image (f ≫ g)) (Iso.hom (compIso f g) : image f ⟶ image (f ≫ g))
        (ι (f ≫ g) : image (f ≫ g) ⟶ Z)) =
    CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f ≫ g)
⊢ Eq (α := image f ⟶ Z)
    (CategoryStruct.comp (Y := image (f ≫ g)) (Iso.hom (compIso f g) : image f ⟶ image (f ≫ g))
      (ι (f ≫ g) : image (f ≫ g) ⟶ Z))
    (ι f ≫ g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f)
      (CategoryStruct.comp (Y := image (f ≫ g)) (Iso.hom (compIso f g) : image f ⟶ image (f ≫ g))
        (ι (f ≫ g) : image (f ≫ g) ⟶ Z)) =
    CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f ≫ g)

Tactic:
simp [image.compIso]

Premises used: CategoryTheory.Limits.image.compIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
w :
  CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g) : X ⟶ image (f ≫ g))
      (CategoryStruct.comp (Y := image f) (Iso.inv (compIso f g)) (ι f) : image (f ≫ g) ⟶ Y) =
    CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g)) (ι (f ≫ g) ≫ inv g)
⊢ Eq (α := image (f ≫ g) ⟶ Y) (CategoryStruct.comp (Y := image f) (Iso.inv (compIso f g)) (ι f) : image (f ≫ g) ⟶ Y)
    (ι (f ≫ g) ≫ inv g : image (f ≫ g) ⟶ Y)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
⊢ CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g) : X ⟶ image (f ≫ g))
      (CategoryStruct.comp (Y := image f) (Iso.inv (compIso f g)) (ι f) : image (f ≫ g) ⟶ Y) =
    CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g)) (ι (f ≫ g) ≫ inv g)

Tactic:
simp [image.compIso]

Premises used: CategoryTheory.Limits.image.compIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
⊢ HasImage (Arrow.mk f).hom

Tactic:
inferInstanceAs <| HasImage f

Premises used: _private.0.CategoryTheory.Limits.instHasImageHomMk._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f : Arrow.{v, u} C
inst_1 : HasImage f.hom
⊢ 𝟙 (image f.hom) ≫ image.ι f.hom = image.ι f.hom ≫ Arrow.Hom.right (𝟙 f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
m : ImageMap sq
⊢ (factorThruImage f.hom ≫ m.map) ≫ image.ι g.hom =
    CategoryStruct.comp (Y := image g.hom) (Arrow.Hom.left sq ≫ factorThruImage g.hom) (image.ι g.hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
F : MonoFactorisation f.hom
F' : MonoFactorisation g.hom
hF' : IsImage F'
map : F.I ⟶ F'.I
map_ι : map ≫ F'.m = F.m ≫ Arrow.Hom.right sq
⊢ Eq (α := image f.hom ⟶ g.right)
    (CategoryStruct.comp (Y := image g.hom) (image.lift F ≫ map ≫ hF'.lift (Image.monoFactorisation g.hom))
      (image.ι g.hom))
    (image.ι f.hom ≫ Arrow.Hom.right sq)

Tactic:
simp [map_ι]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
m : ImageMap sq
⊢ HasImageMap sq

Tactic:
⟨Nonempty.intro m⟩

Premises used: CategoryTheory.Limits.HasImageMap.mk', Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
F : MonoFactorisation f.hom
F' : MonoFactorisation g.hom
hF' : IsImage F'
map : F.I ⟶ F'.I
map_ι : map ≫ F'.m = F.m ≫ Arrow.Hom.right sq
⊢ HasImageMap sq

Tactic:
HasImageMap.mk <| ImageMap.transport sq F hF' map_ι

Premises used: CategoryTheory.Limits.ImageMap.transport, CategoryTheory.Limits.HasImageMap.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
inst_3 : IsIso sq
erw :
  Eq (α := image f.hom ⟶ f.right)
    ((image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫ image.ι g.hom) ≫ Arrow.Hom.right (inv sq))
    ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₁ :
  Eq (α := image f.hom ⟶ f.right)
    (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫ image.ι g.hom ≫ Arrow.Hom.right (inv sq))
    ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₂ :
  Eq (α := image f.hom ⟶ f.right)
    (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫
      ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)).m)
    ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₃ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₄ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ Arrow.Hom.right sq ≫ Arrow.Hom.right (inv sq))
erw₅ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ (sq ≫ inv sq).right)
erw₆ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ CommaMorphism.right (𝟙 f))
erw₇ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ 𝟙 f.right)
erw₈ erw₉ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom)
⊢ Eq (α := image f.hom ⟶ g.right) (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫ image.ι g.hom)
    (image.ι f.hom ≫ Arrow.Hom.right sq)

Tactic:
erw [← cancel_mono (inv sq).right, Category.assoc, ← MonoFactorisation.ofArrowIso_m,
          image.lift_fac, Category.assoc, ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right,
          Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Arrow.Hom.right, CategoryTheory.Comma.comp_right, CategoryTheory.Limits.image.lift_fac, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Limits.MonoFactorisation.ofArrowIso_m, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.Comma.id_right, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g h : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
inst_3 : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst_4 : HasImageMap sq1
inst_5 : HasImageMap sq2
rw :
  Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1))
      (CategoryStruct.comp (Y := image h.hom) (ImageMap.map (imageMap sq2)) (image.ι h.hom)))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
rw₁ :
  Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1)) (image.ι g.hom ≫ Arrow.Hom.right sq2))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
rw₂ :
  Eq (α := image f.hom ⟶ h.right) (image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2)
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
rw₃ rw₄ :
  Eq (α := image f.hom ⟶ h.right) (image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2)
    (image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2)
⊢ Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image h.hom)
      (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1)) (ImageMap.map (imageMap sq2)))
      (image.ι h.hom))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))

Tactic:
rw [Category.assoc, ImageMap.map_ι, ImageMap.map_ι_assoc, Arrow.comp_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ImageMap.map_ι, CategoryTheory.Limits.ImageMap.map_ι_assoc, CategoryTheory.Arrow.comp_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
rw : image.ι f.hom ≫ Arrow.Hom.right sq = map' ≫ image.ι g.hom
rw₁ rw₂ : Eq (α := image f.hom ⟶ g.right) (image.ι f.hom ≫ Arrow.Hom.right sq) (image.ι f.hom ≫ Arrow.Hom.right sq)
⊢ map ≫ image.ι g.hom = map' ≫ image.ι g.hom

Tactic:
rw [map_ι, map_ι']
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
⊢ map ≫ image.ι g.hom = map' ≫ image.ι g.hom

Tactic:
have : map ≫ image.ι g.hom = map' ≫ image.ι g.hom := by rw [map_ι, map_ι']
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
this : map ≫ image.ι g.hom = map' ≫ image.ι g.hom
⊢ map = map'

Tactic:
apply (cancel_mono (image.ι g.hom)).1 this

Premises used: CategoryTheory.Limits.image.ι, CategoryTheory.Arrow.hom, CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
F G : ImageMap sq
⊢ F.map = G.map

Tactic:
apply ImageMap.map_uniq_aux _ F.map_ι _ G.map_ι

Premises used: CategoryTheory.Limits.ImageMap.map_uniq_aux, CategoryTheory.Limits.ImageMap.map_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
⊢ Subsingleton.{v + 1} (ImageMap sq)

Tactic:
Subsingleton.intro fun a b =>
    ImageMap.ext <| ImageMap.map_uniq a b

Premises used: CategoryTheory.Limits.ImageMap.ext, Subsingleton.intro, CategoryTheory.Limits.ImageMap.map_uniq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
inst_3 : HasImageMap sq
⊢ Eq (α := f.left ⟶ image g.hom) (CategoryStruct.comp (Y := image f.hom) (factorThruImage f.hom) (map sq))
    (Arrow.Hom.left sq ≫ factorThruImage g.hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
inst_3 : HasImageMap sq
⊢ Eq (α := image f.hom ⟶ g.right) (CategoryStruct.comp (Y := image g.hom) (map sq) (ι g.hom))
    (ι f.hom ≫ Arrow.Hom.right sq)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y P Q : C
k : X ⟶ Y
inst_1 : HasImage k
l : P ⟶ Q
inst_2 : HasImage l
m : X ⟶ P
n : Y ⟶ Q
w : m ≫ l = k ≫ n
inst_3 : HasImageMap (Arrow.homMk' m n w)
⊢ Eq (α := image (Arrow.mk k).hom ⟶ Q)
    (CategoryStruct.comp (Y := image (Arrow.mk l).hom) (map (Arrow.homMk' m n w)) (ι l)) (ι k ≫ n)

Tactic:
image.map_ι _

Premises used: CategoryTheory.Limits.image.map_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
inst_3 : HasImageMap sq
h : Arrow.{v, u} C
inst_4 : HasImage h.hom
sq' : g ⟶ h
inst_5 : HasImageMap sq'
inst_6 : HasImageMap (sq ≫ sq')
e_self : Eq (α := ImageMap (sq ≫ sq')) (HasImageMap.imageMap (sq ≫ sq')) (imageMapComp sq sq')
⊢ Eq (α := image f.hom ⟶ image h.hom) (ImageMap.map (HasImageMap.imageMap (sq ≫ sq')))
    (ImageMap.map (imageMapComp sq sq'))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
inst_3 : HasImageMap sq
h : Arrow.{v, u} C
inst_4 : HasImage h.hom
sq' : g ⟶ h
inst_5 : HasImageMap sq'
inst_6 : HasImageMap (sq ≫ sq')
⊢ Eq (α := ImageMap (sq ≫ sq')) (HasImageMap.imageMap (sq ≫ sq')) (imageMapComp sq sq')

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImageMap (𝟙 f)
e_self : Eq (α := ImageMap (𝟙 f)) (HasImageMap.imageMap (𝟙 f)) (imageMapId f)
⊢ Eq (α := image f.hom ⟶ image f.hom) (ImageMap.map (HasImageMap.imageMap (𝟙 f))) (ImageMap.map (imageMapId f))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImageMap (𝟙 f)
⊢ Eq (α := ImageMap (𝟙 f)) (HasImageMap.imageMap (𝟙 f)) (imageMapId f)

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : StrongEpi f
⊢ f ≫ 𝟙 Y = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
G : MonoFactorisation f
rw : G.e ≫ G.m = f
rw₁ rw₂ : f = f
⊢ G.e ≫ G.m = F.e ≫ F.m

Tactic:
rw [F.toMonoFactorisation.fac, G.fac]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
d : {X Y : C} → (f : X ⟶ Y) → StrongEpiMonoFactorisation f
⊢ HasStrongEpiMonoFactorisations.{v, u} C

Tactic:
⟨fun f => Nonempty.intro <| d f⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasStrongEpiMonoFactorisations.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
rw : StrongEpi (F.e ≫ (F.toMonoIsImage.isoExt hF').hom)
⊢ StrongEpi F'.e

Tactic:
rw [← IsImage.e_isoExt_hom F.toMonoIsImage hF']

Premises used: CategoryTheory.Limits.IsImage.e_isoExt_hom, CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi (F.e ≫ (F.toMonoIsImage.isoExt hF').hom)

Tactic:
apply strongEpi_comp

Premises used: CategoryTheory.strongEpi_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
F : StrongEpiMonoFactorisation f
⊢ StrongEpi (Q := image f) (factorThruImage f)

Tactic:
strongEpi_of_strongEpiMonoFactorisation F <| Image.isImage f

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation, CategoryTheory.Limits.image, CategoryTheory.Limits.Image.isImage
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasImages.{v, u} C
inst_2 : HasStrongEpiImages.{v, u} C
f g : Arrow.{v, u} C
st : f ⟶ g
⊢ CategoryStruct.comp (Y := image g.hom) (Arrow.Hom.left st ≫ factorThruImage g.hom) (image.ι g.hom) =
    CategoryStruct.comp (Y := image f.hom) (factorThruImage f.hom) (image.ι f.hom ≫ Arrow.Hom.right st)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasImages.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : HasEqualizers.{v, u} C
X Y : C
f : X ⟶ Y
A B : C
h : A ⟶ B
h_mono : Mono h
x : X ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f)
      (image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
            e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ : MonoFactorisation f } ≫
        pullback.fst h y) =
    x

Tactic:
simp only [image.fac_lift_assoc, pullback.lift_fst]

Premises used: CategoryTheory.Limits.image.fac_lift_assoc, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasImages.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : HasEqualizers.{v, u} C
X Y : C
f : X ⟶ Y
A B : C
h : A ⟶ B
h_mono : Mono h
x : X ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
w :
  CategoryStruct.comp (Y := image f) (factorThruImage f)
      ((image.lift
            { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
              e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ : MonoFactorisation f } ≫
          pullback.fst h y) ≫
        h) =
    factorThruImage f ≫ y
⊢ (image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
            e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ : MonoFactorisation f } ≫
        pullback.fst h y) ≫
      h =
    y

Tactic:
apply image.ext

Premises used: CategoryTheory.Limits.image.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasImages.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : HasEqualizers.{v, u} C
X Y : C
f : X ⟶ Y
A B : C
h : A ⟶ B
h_mono : Mono h
x : X ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f)
      ((image.lift
            { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
              e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ : MonoFactorisation f } ≫
          pullback.fst h y) ≫
        h) =
    factorThruImage f ≫ y

Tactic:
simp only [sq.w, Category.assoc, image.fac_lift_assoc, pullback.lift_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.Limits.image.fac_lift_assoc, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrongEpiMonoFactorisations.{v, u} C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst_2 : StrongEpi e
inst_3 : Mono m
dsimp :
  CategoryStruct.comp (Y := image f)
      ({ I := I', m := m, m_mono := inst_3, e := e, fac := ⋯, e_strong_epi := inst_2 :
              StrongEpiMonoFactorisation f }.toMonoIsImage.lift
        (Image.monoFactorisation f))
      (ι f) =
    m
⊢ CategoryStruct.comp (Y := image f) (Iso.hom (isoStrongEpiMono e m comm) : I' ⟶ image f) (ι f : image f ⟶ Y) = m

Tactic:
dsimp [isoStrongEpiMono]

Premises used: CategoryTheory.Limits.image.isoStrongEpiMono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrongEpiMonoFactorisations.{v, u} C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst_2 : StrongEpi e
inst_3 : Mono m
⊢ CategoryStruct.comp (Y := image f)
      ({ I := I', m := m, m_mono := inst_3, e := e, fac := ⋯, e_strong_epi := inst_2 :
              StrongEpiMonoFactorisation f }.toMonoIsImage.lift
        (Image.monoFactorisation f))
      (ι f) =
    m

Tactic:
apply IsImage.lift_fac

Premises used: CategoryTheory.Limits.IsImage.lift_fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrongEpiMonoFactorisations.{v, u} C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst_2 : StrongEpi e
inst_3 : Mono m
⊢ Eq (α := image f ⟶ Y) (Iso.inv (isoStrongEpiMono e m comm) ≫ m : image f ⟶ Y) (ι f : image f ⟶ Y)

Tactic:
image.lift_fac _

Premises used: CategoryTheory.Limits.image.lift_fac, CategoryTheory.Limits.image.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
h : HasStrongEpiMonoFactorisations.{v_1, u_1} C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
⊢ Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)

Tactic:
haveI : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
h : HasStrongEpiMonoFactorisations.{v_1, u_1} C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
⊢ StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)

Tactic:
haveI : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _