awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
X Y : Grothendieck F ⥤ H
x : X ⟶ Y
j : C
w :
  ∀ (j_1 : (↑(F.obj j) : Type u_1)),
    Eq (α := (Grothendieck.ι F j ⋙ X).obj j_1 ⟶ obj colim Y)
      (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
        CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
          (map (fiberwiseColim F H ⋙ colim) x ≫
            Iso.hom
              ((fun (G : Grothendieck F ⥤ H) ↦
                  (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
                Y)))
      (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
        CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
          (Iso.hom
              ((fun (G : Grothendieck F ⥤ H) ↦
                  (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
                X) ≫
            map colim x))
⊢ Eq (α := (obj (fiberwiseColim F H) X).obj j ⟶ obj colim Y)
    (CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
      (map (fiberwiseColim F H ⋙ colim) x ≫
        Iso.hom
          ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
            Y)))
    (CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
      (Iso.hom
          ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
            X) ≫
        map colim x))

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
X Y : Grothendieck F ⥤ H
x : X ⟶ Y
w :
  ∀ (j : C) (j_1 : (↑(F.obj j) : Type u_1)),
    Eq (α := (Grothendieck.ι F j ⋙ X).obj j_1 ⟶ obj colim Y)
      (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
        CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
          (map (fiberwiseColim F H ⋙ colim) x ≫
            Iso.hom
              ((fun (G : Grothendieck F ⥤ H) ↦
                  (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
                Y)))
      (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
        CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
          (Iso.hom
              ((fun (G : Grothendieck F ⥤ H) ↦
                  (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
                X) ≫
            map colim x))
⊢ Eq (α := obj (fiberwiseColim F H ⋙ colim) X ⟶ obj colim Y)
    (map (fiberwiseColim F H ⋙ colim) x ≫
      Iso.hom
        ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G)) Y))
    (Iso.hom
        ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G)) X) ≫
      map colim x)

Tactic:
iterate 2 apply colimit.hom_ext; intro

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
X Y : Grothendieck F ⥤ H
x : X ⟶ Y
j : C
j_1 : (↑(F.obj j) : Type u_1)
⊢ Eq (α := (Grothendieck.ι F j ⋙ X).obj j_1 ⟶ obj colim Y)
    (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
      CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
        (map (fiberwiseColim F H ⋙ colim) x ≫
          Iso.hom
            ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
              Y)))
    (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
      CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
        (Iso.hom
            ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
              X) ≫
          map colim x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hI : F.I = F'.I
hm : F.m = eqToHom hI ≫ F'.m
obtain :
  ∀ (I : C) (Fm : I ⟶ Y) [m_mono : Mono Fm] (e : X ⟶ I) (Ffac : e ≫ Fm = f)
    (hI : { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.I = F'.I)
    (hm : { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m = eqToHom hI ≫ F'.m),
    { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } = F'
⊢ F = F'

Tactic:
obtain ⟨_, Fm, _, Ffac⟩ := F
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F' : MonoFactorisation f
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
hI : { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.I = F'.I
hm : { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m = eqToHom hI ≫ F'.m
obtain :
  ∀ (I_1 : C) (Fm' : I_1 ⟶ Y) [m_mono_1 : Mono Fm'] (e_1 : X ⟶ I_1) (Ffac' : e_1 ≫ Fm' = f)
    (hI :
      { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.I =
        { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.I)
    (hm :
      { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m =
        eqToHom hI ≫ { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.m),
    { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } =
      { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' }
⊢ { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } = F'

Tactic:
obtain ⟨_, Fm', _, Ffac'⟩ := F'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
I_1 : C
Fm' : I_1 ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I_1
Ffac' : e_1 ≫ Fm' = f
hI :
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.I =
    { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.I
hm :
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m =
    eqToHom hI ≫ { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.m
refl :
  ∀ (Fm' : I ⟶ Y) [m_mono_2 : Mono Fm'] (e_2 : X ⟶ I) (Ffac' : e_2 ≫ Fm' = f)
    (hm :
      { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m =
        eqToHom ⋯ ≫ { I := I, m := Fm', m_mono := m_mono_2, e := e_2, fac := Ffac' : MonoFactorisation f }.m),
    { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } =
      { I := I, m := Fm', m_mono := m_mono_2, e := e_2, fac := Ffac' }
⊢ { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } =
    { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' }

Tactic:
cases hI
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm :
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m =
    eqToHom ⋯ ≫ { I := I, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.m
⊢ Fm = Fm'

Tactic:
simpa using hm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm :
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m =
    eqToHom ⋯ ≫ { I := I, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.m
⊢ Fm = Fm'

Tactic:
replace hm : Fm = Fm' := by simpa using hm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm : Fm = Fm'
refl : e = e_1
⊢ { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } =
    { I := I, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm : Fm = Fm'
refl : e ≫ Fm = e_1 ≫ Fm
⊢ e = e_1

Tactic:
apply (cancel_mono Fm).1

Premises used: CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm : Fm = Fm'
refl : f = e_1 ≫ Fm
refl₁ : f = e_1 ≫ Fm'
refl₂ refl₃ : f = f
⊢ e ≫ Fm = e_1 ≫ Fm

Tactic:
rw [Ffac, hm, Ffac']
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
f g : Arrow.{v, u} C
F : MonoFactorisation f.hom
sq : f ⟶ g
inst_1 : IsIso sq
⊢ (inv (Arrow.Hom.left sq) ≫ F.e) ≫ F.m ≫ Arrow.Hom.right sq = g.hom

Tactic:
simp only [fac_assoc, Arrow.w, IsIso.inv_comp_eq, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.Limits.MonoFactorisation.fac_assoc, CategoryTheory.Arrow.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
m : F.I ⟶ Y
e : X ⟶ F.I
hm : m = F.m
he : e = F.e
rw : Mono F.m
⊢ Mono m

Tactic:
rw [hm]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
m : F.I ⟶ Y
e : X ⟶ F.I
hm : m = F.m
he : e = F.e
⊢ Mono F.m

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
f : F ⟶ G
X : C
H : MonoFactorisation f
x : F.obj X
⊢ Eq (α := (fun (X : Type w) ↦ X) (G.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.m.app X) :
          (a : (fun (X : Type w) ↦ X) (H.I.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app X) :
              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (H.I.obj X))
            x :
          (fun (X : Type w) ↦ X) (H.I.obj X)) :
      (fun (X : Type w) ↦ X) (G.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
        x :
      (fun (X : Type w) ↦ X) (G.obj X))

Tactic:
simp [← comp_apply, ← NatTrans.comp_app]

Premises used: CategoryTheory.comp_apply, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
hF : IsImage F
F' : MonoFactorisation f
⊢ (F.e ≫ hF.lift F') ≫ F'.m = F'.e ≫ F'.m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.lift F' ≫ hF'.lift F) ≫ F.m = 𝟙 F.I ≫ F.m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF'.lift F ≫ hF.lift F') ≫ F'.m = 𝟙 F'.I ≫ F'.m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.isoExt hF').hom ≫ F'.m = F.m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.isoExt hF').inv ≫ F.m = F'.m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F.e ≫ (hF.isoExt hF').hom = F'.e

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F'.e ≫ (hF.isoExt hF').inv = F.e

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
F_1 F'_1 : MonoFactorisation f_1
hF_1 : IsImage F_1
hF' : IsImage F'_1
f g : Arrow.{v, u} C
F : MonoFactorisation f.hom
hF : IsImage F
sq : f ⟶ g
inst_1 : IsIso sq
F' : MonoFactorisation g.hom
⊢ hF.lift (F'.ofArrowIso (inv sq)) ≫ F'.m = (F.ofArrowIso sq).m

Tactic:
simpa only [MonoFactorisation.ofArrowIso_m, Arrow.inv_right, ← Category.assoc,
      IsIso.comp_inv_eq] using hF.lift_fac (F'.ofArrowIso (inv sq))

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsImage.lift_fac, CategoryTheory.Limits.MonoFactorisation.ofArrowIso_m, CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.Limits.MonoFactorisation.ofArrowIso, CategoryTheory.inv, CategoryTheory.Arrow.inv_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : ImageFactorisation f
⊢ HasImage f

Tactic:
⟨Nonempty.intro F⟩

Premises used: CategoryTheory.Limits.HasImage.mk', Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
h : HasImage f.hom
sq : f ⟶ g
inst_1 : IsIso sq
⊢ HasImage g.hom

Tactic:
⟨⟨h.exists_image.some.ofArrowIso sq⟩⟩

Premises used: CategoryTheory.Limits.HasImage.exists_image, CategoryTheory.Limits.HasImage.mk', CategoryTheory.Limits.ImageFactorisation.ofArrowIso, Nonempty.some, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 f : X ⟶ Y
inst_1 : Mono f
⊢ HasImage f

Tactic:
HasImage.mk ⟨_, IsImage.self f⟩

Premises used: CategoryTheory.Limits.ImageFactorisation.mk, CategoryTheory.Limits.HasImage.mk, CategoryTheory.Limits.IsImage.self
-- 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
⊢ (Image.monoFactorisation f).m = ι f

Tactic:
rfl

Premises used: CategoryTheory.Limits.image.ι, rfl
-- 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
⊢ Mono (X := image f) (image.ι f)

Tactic:
(Image.monoFactorisation f).m_mono

Premises used: CategoryTheory.Limits.MonoFactorisation.m_mono, CategoryTheory.Limits.image.ι, CategoryTheory.Limits.image, CategoryTheory.Limits.Image.monoFactorisation
-- 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
⊢ (Image.monoFactorisation f).e = factorThruImage f

Tactic:
rfl

Premises used: CategoryTheory.Limits.factorThruImage, rfl
-- 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
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f) = f

Tactic:
(Image.monoFactorisation f).fac

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, CategoryTheory.Limits.factorThruImage, CategoryTheory.Limits.image.ι, CategoryTheory.Limits.image, CategoryTheory.Limits.Image.monoFactorisation
-- 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' : MonoFactorisation f
⊢ Eq (α := image f ⟶ Y) (lift F' ≫ F'.m) (ι f)

Tactic:
(Image.isImage f).lift_fac F'

Premises used: CategoryTheory.Limits.IsImage.lift_fac, CategoryTheory.Limits.image.ι, CategoryTheory.Limits.image, CategoryTheory.Limits.Image.isImage, CategoryTheory.Limits.image.lift
-- 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' : MonoFactorisation f
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f) (lift F') = F'.e

Tactic:
(Image.isImage f).fac_lift F'

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.Limits.image, CategoryTheory.Limits.IsImage.fac_lift, CategoryTheory.Limits.Image.isImage, CategoryTheory.Limits.image.lift
-- 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 : MonoFactorisation f
⊢ Eq (α := (Image.monoFactorisation f).I ⟶ F.I) (IsImage.lift (Image.isImage f) F) (lift F)

Tactic:
rfl

Premises used: CategoryTheory.Limits.image.lift, rfl
-- 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 : MonoFactorisation f
hF : IsImage F
⊢ CategoryStruct.comp (Y := (Image.monoFactorisation f).I) (hF.lift (Image.monoFactorisation f)) (image.ι f) = F.m

Tactic:
hF.lift_fac _

Premises used: CategoryTheory.Limits.IsImage.lift_fac, CategoryTheory.Limits.image.ι
-- 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
⊢ Eq (α := image f ⟶ Y)
    (lift { I := image f, m := ι f, m_mono := ⋯, e := factorThruImage f, fac := ⋯ : MonoFactorisation f } ≫ ι f) (ι f)

Tactic:
(Image.isImage f).lift_fac _

Premises used: CategoryTheory.Limits.IsImage.lift_fac, CategoryTheory.Limits.image.ι, CategoryTheory.Limits.image, CategoryTheory.Limits.Image.isImage, CategoryTheory.Limits.image.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : HasImage g
inst_2 : HasImage (f ≫ g)
h : Y ⟶ image g
H : (f ≫ h) ≫ ι g = f ≫ g
⊢ Eq (α := image (f ≫ g) ⟶ Z)
    (lift { I := image g, m := ι g, m_mono := ⋯, e := f ≫ h, fac := ⋯ : MonoFactorisation (f ≫ g) } ≫ ι g) (ι (f ≫ g))

Tactic:
image.lift_fac _

Premises used: CategoryTheory.Limits.image.ι, CategoryTheory.Limits.image.lift_fac
-- 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' : MonoFactorisation f
⊢ Mono (X := image f) (lift F')

Tactic:
@mono_of_mono _ _ _ _ _ _ F'.m ?_

Premises used: CategoryTheory.mono_of_mono, CategoryTheory.Limits.MonoFactorisation.m
-- 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' : MonoFactorisation f
refine : Mono (X := image f) (lift F' ≫ F'.m)
⊢ Mono (X := image f) (lift F')

Tactic:
refine @mono_of_mono _ _ _ _ _ _ F'.m ?_

Premises used: CategoryTheory.mono_of_mono, CategoryTheory.Limits.MonoFactorisation.m
-- 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' : MonoFactorisation f
⊢ Mono (X := image f) (lift F' ≫ F'.m)

Tactic:
simpa using MonoFactorisation.m_mono _

Premises used: CategoryTheory.Limits.MonoFactorisation.m_mono
-- 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' : MonoFactorisation f
l : image f ⟶ F'.I
w : l ≫ F'.m = image.ι f
⊢ l ≫ F'.m = image.lift F' ≫ F'.m

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ CategoryStruct.comp (Y := image f) (Iso.inv (imageMonoIsoSource f) : X ⟶ image f) (image.ι f : image f ⟶ Y) = f

Tactic:
simp [imageMonoIsoSource]

Premises used: CategoryTheory.Limits.imageMonoIsoSource
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
simp :
  Eq (α := image f ⟶ Y)
    (Iso.hom (imageMonoIsoSource f) ≫
        CategoryStruct.comp (Y := image f) (Iso.inv (imageMonoIsoSource f) : X ⟶ image f) (image.ι f : image f ⟶ Y) :
      image f ⟶ Y)
    (image.ι f : image f ⟶ Y)
⊢ Eq (α := image f ⟶ Y) (Iso.hom (imageMonoIsoSource f) ≫ f : image f ⟶ Y) (image.ι f : image f ⟶ Y)

Tactic:
simp only [← imageMonoIsoSource_inv_ι f]

Premises used: CategoryTheory.Limits.imageMonoIsoSource_inv_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
rw :
  Eq (α := image f ⟶ Y)
    (CategoryStruct.comp (Y := image f)
        (Iso.hom (imageMonoIsoSource f) ≫ Iso.inv (imageMonoIsoSource f) : image f ⟶ image f)
        (image.ι f : image f ⟶ Y) :
      image f ⟶ Y)
    (image.ι f : image f ⟶ Y)
rw₁ : 𝟙 (image f) ≫ image.ι f = image.ι f
rw₂ rw₃ : Eq (α := image f ⟶ Y) (image.ι f) (image.ι f)
⊢ Eq (α := image f ⟶ Y)
    (Iso.hom (imageMonoIsoSource f) ≫
        CategoryStruct.comp (Y := image f) (Iso.inv (imageMonoIsoSource f) : X ⟶ image f) (image.ι f : image f ⟶ Y) :
      image f ⟶ Y)
    (image.ι f : image f ⟶ Y)

Tactic:
rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.id_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
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
⊢ v ≫ q ≫ ι f = ι f

Tactic:
have t₀ : v ≫ q ≫ image.ι f = image.ι f := image.lift_fac F'
-- 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
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ v ≫ q ≫ ι f = ι f

Tactic:
t₀
-- 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
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
h₁ : (v ≫ q) ≫ ι f = v ≫ q ≫ ι f
⊢ (v ≫ q) ≫ ι f = ι f

Tactic:
convert! t₀ using 1