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
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₁ h₂ : v ≫ q ≫ ι f = v ≫ q ≫ ι f
⊢ (v ≫ q) ≫ ι f = v ≫ q ≫ ι f

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 = 𝟙 (image f)

Tactic:
have t : v ≫ q = 𝟙 (image f) :=
    (cancel_mono_id (image.ι f)).1
      (by
        convert! t₀ using 1
        rw [Category.assoc])
-- 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
t : v ≫ q = 𝟙 (image f)
rw rw₁ : g = g
⊢ g = 𝟙 (image f) ≫ g

Tactic:
rw [Category.id_comp]

Premises used: 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'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
rw : (v ≫ q) ≫ g = v ≫ q ≫ g
rw₁ rw₂ : v ≫ q ≫ g = v ≫ q ≫ g
⊢ 𝟙 (image f) ≫ g = v ≫ q ≫ g

Tactic:
rw [← t, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
t : v ≫ q = 𝟙 (image f)
rw rw₁ : v ≫ equalizer.ι g h ≫ h = v ≫ q ≫ h
⊢ v ≫ q ≫ g = v ≫ q ≫ h

Tactic:
rw [equalizer.condition g h]

Premises used: CategoryTheory.Limits.equalizer.condition
-- 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
t : v ≫ q = 𝟙 (image f)
rw : (v ≫ q) ≫ h = 𝟙 (image f) ≫ h
rw₁ rw₂ : 𝟙 (image f) ≫ h = 𝟙 (image f) ≫ h
⊢ v ≫ q ≫ h = 𝟙 (image f) ≫ h

Tactic:
rw [← Category.assoc, t]

Premises used: CategoryTheory.Category.assoc
-- 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
t : v ≫ q = 𝟙 (image f)
rw rw₁ : h = h
⊢ 𝟙 (image f) ≫ h = h

Tactic:
rw [Category.id_comp]

Premises used: 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'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
g₁ : g = 𝟙 (image f) ≫ g
g₂ : 𝟙 (image f) ≫ g = v ≫ q ≫ g
g₃ : v ≫ q ≫ g = v ≫ q ≫ h
g₄ : v ≫ q ≫ h = 𝟙 (image f) ≫ h
g₅ : 𝟙 (image f) ≫ h = h
⊢ g = h

Tactic:
calc
    g = 𝟙 (image f) ≫ g := by rw [Category.id_comp]
    _ = v ≫ q ≫ g := by rw [← t, Category.assoc]
    _ = v ≫ q ≫ h := by rw [equalizer.condition g h]
    _ = 𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
    _ = h := by rw [Category.id_comp]

Premises used: CategoryTheory.CategoryStruct.id, 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
inst_2 : ∀ {Z : C} (g h : image f ⟶ Z), HasLimit (parallelPair g h)
⊢ Epi (Y := image f) (factorThruImage f)

Tactic:
⟨fun _ _ w => image.ext f w⟩

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

Tactic:
rw [← image.fac f] at E

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

Tactic:
epi_of_epi (factorThruImage f) (image.ι f)

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

Tactic:
exact epi_of_epi (factorThruImage f) (image.ι f)

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.epi_of_epi, 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
inst_2 : Epi (X := image f) (image.ι f)
inst_3 : Epi (Y := image f) (factorThruImage f)
rw : Epi (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))
⊢ Epi f

Tactic:
rw [← image.fac f]

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

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
h : f = f'
rw : CategoryStruct.comp (Y := image f') (factorThruImage f') (ι f') = f'
⊢ CategoryStruct.comp (Y := image f') (factorThruImage f') (ι f') = f

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
h : f = f'
⊢ CategoryStruct.comp (Y := image f') (factorThruImage f') (ι f') = f'

Tactic:
simp only [image.fac]

Premises used: CategoryTheory.Limits.image.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
h : f = f'
subst :
  ∀ [inst_3 : HasImage f],
    CategoryStruct.comp (Y := image f) (CategoryStruct.comp (Y := image f) (image.eqToHom ⋯) (image.eqToHom ⋯))
        (image.ι f) =
      𝟙 (image f) ≫ image.ι f
⊢ CategoryStruct.comp (Y := image f) (CategoryStruct.comp (Y := image f') (image.eqToHom h) (image.eqToHom ⋯))
      (image.ι f) =
    𝟙 (image f) ≫ image.ι f

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 inst_2 : HasImage f
⊢ CategoryStruct.comp (Y := image f) (CategoryStruct.comp (Y := image f) (image.eqToHom ⋯) (image.eqToHom ⋯))
      (image.ι f) =
    𝟙 (image f) ≫ image.ι f

Tactic:
simp [image.eqToHom, Category.assoc, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.eqToHom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
h : f = f'
subst :
  ∀ [inst_3 : HasImage f],
    CategoryStruct.comp (Y := image f) (CategoryStruct.comp (Y := image f) (image.eqToHom ⋯) (image.eqToHom ⋯))
        (image.ι f) =
      𝟙 (image f) ≫ image.ι f
⊢ CategoryStruct.comp (Y := image f') (CategoryStruct.comp (Y := image f) (image.eqToHom ⋯) (image.eqToHom h))
      (image.ι f') =
    𝟙 (image f') ≫ image.ι f'

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 inst_2 : HasImage f
⊢ CategoryStruct.comp (Y := image f) (CategoryStruct.comp (Y := image f) (image.eqToHom ⋯) (image.eqToHom ⋯))
      (image.ι f) =
    𝟙 (image f) ≫ image.ι f

Tactic:
simp [image.eqToHom]

Premises used: CategoryTheory.Limits.image.eqToHom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
inst_3 : HasEqualizers.{v, u} C
h : f = f'
w :
  CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f) =
    CategoryStruct.comp (Y := image f) (factorThruImage f)
      (CategoryStruct.comp (Y := image f') (Iso.hom (eqToIso h)) (ι f'))
⊢ Eq (α := image f ⟶ Y) (ι f) (CategoryStruct.comp (Y := image f') (Iso.hom (eqToIso h)) (ι f'))

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
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
inst_3 : HasEqualizers.{v, u} C
h : f = f'
w :
  ∀ [inst_4 : HasImage f],
    CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f) =
      CategoryStruct.comp (Y := image f) (factorThruImage f)
        (CategoryStruct.comp (Y := image f) (Iso.hom (eqToIso ⋯)) (ι f))
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f) =
    CategoryStruct.comp (Y := image f) (factorThruImage f)
      (CategoryStruct.comp (Y := image f') (Iso.hom (eqToIso h)) (ι f'))

Tactic:
subst h
-- 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
inst_2 : HasEqualizers.{v, u} C
inst_3 : HasImage f
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f) =
    CategoryStruct.comp (Y := image f) (factorThruImage f)
      (CategoryStruct.comp (Y := image f) (Iso.hom (eqToIso ⋯)) (ι f))

Tactic:
simp [asIso, image.eqToIso, image.eqToHom]

Premises used: CategoryTheory.Limits.image.eqToHom, CategoryTheory.Limits.image.eqToIso, CategoryTheory.asIso
-- 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 : HasImage g
inst_2 : HasImage (f ≫ g)
⊢ Eq (α := image (f ≫ g) ⟶ Z) (CategoryStruct.comp (Y := image g) (preComp f g) (ι g)) (ι (f ≫ g))

Tactic:
simp [image.preComp]

Premises used: CategoryTheory.Limits.image.preComp
-- 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 : HasImage g
inst_2 : HasImage (f ≫ g)
⊢ Eq (α := X ⟶ image g) (CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g)) (preComp f g))
    (f ≫ factorThruImage g)

Tactic:
simp [image.preComp]

Premises used: CategoryTheory.Limits.image.preComp
-- 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 : HasImage g
inst_2 : HasImage (f ≫ g)
⊢ Mono (X := image (f ≫ g)) (Y := image g) (preComp f g)

Tactic:
@mono_of_mono _ _ _ _ _ _ (image.ι g) ?_

Premises used: CategoryTheory.Limits.image.ι, CategoryTheory.mono_of_mono
-- 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 : HasImage g
inst_2 : HasImage (f ≫ g)
refine : Mono (X := image (f ≫ g)) (CategoryStruct.comp (Y := image g) (preComp f g) (ι g))
⊢ Mono (X := image (f ≫ g)) (Y := image g) (preComp f g)

Tactic:
refine @mono_of_mono _ _ _ _ _ _ (image.ι g) ?_

Premises used: CategoryTheory.Limits.image.ι, CategoryTheory.mono_of_mono
-- 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 : HasImage g
inst_2 : HasImage (f ≫ g)
simp : Mono (X := image (f ≫ g)) (ι (f ≫ g))
⊢ Mono (X := image (f ≫ g)) (CategoryStruct.comp (Y := image g) (preComp f g) (ι g))

Tactic:
simp only [image.preComp_ι]

Premises used: CategoryTheory.Limits.image.preComp_ι
-- 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 : HasImage g
inst_2 : HasImage (f ≫ g)
⊢ Mono (X := image (f ≫ g)) (ι (f ≫ g))

Tactic:
infer_instance
-- 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
W : C
h : Z ⟶ W
inst_1 : HasImage (g ≫ h)
inst_2 : HasImage (f ≫ g ≫ h)
inst_3 : HasImage h
inst_4 : HasImage ((f ≫ g) ≫ h)
apply :
  Eq (α := image (f ≫ g ≫ h) ⟶ W)
    (CategoryStruct.comp (Y := image h) (CategoryStruct.comp (Y := image (g ≫ h)) (preComp f (g ≫ h)) (preComp g h))
      (ι h))
    (CategoryStruct.comp (Y := image h) (CategoryStruct.comp (Y := image ((f ≫ g) ≫ h)) (eqToHom ⋯) (preComp (f ≫ g) h))
      (ι h))
⊢ Eq (α := image (f ≫ g ≫ h) ⟶ image h) (CategoryStruct.comp (Y := image (g ≫ h)) (preComp f (g ≫ h)) (preComp g h))
    (CategoryStruct.comp (Y := image ((f ≫ g) ≫ h)) (eqToHom ⋯) (preComp (f ≫ g) h))

Tactic:
apply (cancel_mono (image.ι h)).1

Premises used: CategoryTheory.Limits.image.ι, 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
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst_1 : HasImage (g ≫ h)
inst_2 : HasImage (f ≫ g ≫ h)
inst_3 : HasImage h
inst_4 : HasImage ((f ≫ g) ≫ h)
simp :
  Eq (α := image (f ≫ g ≫ h) ⟶ W) (ι (f ≫ g ≫ h))
    (lift
        { I := image ((f ≫ g) ≫ h), m := ι ((f ≫ g) ≫ h), m_mono := ⋯, e := factorThruImage ((f ≫ g) ≫ h), fac := ⋯ :
          MonoFactorisation (f ≫ g ≫ h) } ≫
      ι ((f ≫ g) ≫ h))
⊢ Eq (α := image (f ≫ g ≫ h) ⟶ W)
    (CategoryStruct.comp (Y := image h) (CategoryStruct.comp (Y := image (g ≫ h)) (preComp f (g ≫ h)) (preComp g h))
      (ι h))
    (CategoryStruct.comp (Y := image h) (CategoryStruct.comp (Y := image ((f ≫ g) ≫ h)) (eqToHom ⋯) (preComp (f ≫ g) h))
      (ι h))

Tactic:
simp only [preComp, Category.assoc, fac, lift_mk_comp, eqToHom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.eqToHom, CategoryTheory.Limits.image.preComp, CategoryTheory.Limits.image.fac, CategoryTheory.Limits.image.lift_mk_comp
-- 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
W : C
h : Z ⟶ W
inst_1 : HasImage (g ≫ h)
inst_2 : HasImage (f ≫ g ≫ h)
inst_3 : HasImage h
inst_4 : HasImage ((f ≫ g) ≫ h)
rw rw₁ : Eq (α := image (f ≫ g ≫ h) ⟶ W) (ι (f ≫ g ≫ h)) (ι (f ≫ g ≫ h))
⊢ Eq (α := image (f ≫ g ≫ h) ⟶ W) (ι (f ≫ g ≫ h))
    (lift
        { I := image ((f ≫ g) ≫ h), m := ι ((f ≫ g) ≫ h), m_mono := ⋯, e := factorThruImage ((f ≫ g) ≫ h), fac := ⋯ :
          MonoFactorisation (f ≫ g ≫ h) } ≫
      ι ((f ≫ g) ≫ h))

Tactic:
rw [image.lift_fac]

Premises used: 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage g
inst_3 : HasImage (f ≫ g)
inst_4 : Epi f
apply : Epi (Y := image g) (f ≫ factorThruImage g)
⊢ Epi (X := image (f ≫ g)) (Y := image g) (preComp f g)

Tactic:
apply @epi_of_epi_fac _ _ _ _ _ _ _ _ ?_ (image.factorThruImage_preComp _ _)

Premises used: CategoryTheory.Limits.image.factorThruImage_preComp, CategoryTheory.epi_of_epi_fac
-- 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 g
inst_3 : HasImage (f ≫ g)
inst_4 : Epi f
⊢ Epi (Y := image g) (f ≫ factorThruImage g)

Tactic:
epi_comp _ _

Premises used: CategoryTheory.epi_comp
-- 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 g
inst_3 : HasImage (f ≫ g)
inst_4 : Epi f
⊢ Epi (Y := image g) (f ≫ factorThruImage g)

Tactic:
exact epi_comp _ _

Premises used: CategoryTheory.epi_comp
-- 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 : IsIso f
inst_3 : HasImage g
F' : MonoFactorisation (f ≫ g)
dsimp : Eq (α := (Image.monoFactorisation g).I ⟶ Z) (image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m) (image.ι g)
⊢ image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m = ((Image.monoFactorisation g).isoComp f).m

Tactic:
dsimp
-- 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 : IsIso f
inst_3 : HasImage g
F' : MonoFactorisation (f ≫ g)
⊢ (MonoFactorisation.ofIsoComp f F').m = F'.m

Tactic:
have : (MonoFactorisation.ofIsoComp f F').m = F'.m := rfl
-- 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 : IsIso f
inst_3 : HasImage g
F' : MonoFactorisation (f ≫ g)
this : (MonoFactorisation.ofIsoComp f F').m = F'.m
rw :
  Eq (α := (Image.monoFactorisation g).I ⟶ Z)
    (image.lift (MonoFactorisation.ofIsoComp f F') ≫ (MonoFactorisation.ofIsoComp f F').m) (image.ι g)
rw₁ rw₂ : Eq (α := (Image.monoFactorisation g).I ⟶ Z) (image.ι g) (image.ι g)
⊢ Eq (α := (Image.monoFactorisation g).I ⟶ Z) (image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m) (image.ι g)

Tactic:
rw [← this, image.lift_fac (MonoFactorisation.ofIsoComp f F')]

Premises used: CategoryTheory.Limits.image.lift_fac, CategoryTheory.Limits.MonoFactorisation.ofIsoComp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
f : X ⟶ Y
inst_2 : IsIso f
inst_3 : HasImage g
w :
  CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g))
      (CategoryStruct.comp (Y := image g) (preComp f g)
        (lift
          { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ :
            MonoFactorisation g })) =
    factorThruImage (f ≫ g) ≫ 𝟙 (image (f ≫ g))
⊢ CategoryStruct.comp (Y := image g) (preComp f g)
      (lift { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ }) =
    𝟙 (image (f ≫ g))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
f : X ⟶ Y
inst_2 : IsIso f
inst_3 : HasImage g
⊢ CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g))
      (CategoryStruct.comp (Y := image g) (preComp f g)
        (lift
          { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ :
            MonoFactorisation g })) =
    factorThruImage (f ≫ g) ≫ 𝟙 (image (f ≫ g))

Tactic:
simp [image.preComp]

Premises used: CategoryTheory.Limits.image.preComp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
f : X ⟶ Y
inst_2 : IsIso f
inst_3 : HasImage g
w :
  CategoryStruct.comp (Y := image g) (factorThruImage g)
      (lift
          { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ :
            MonoFactorisation g } ≫
        preComp f g) =
    factorThruImage g ≫ 𝟙 (image g)
⊢ lift
        { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ :
          MonoFactorisation g } ≫
      preComp f g =
    𝟙 (image g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
f : X ⟶ Y
inst_2 : IsIso f
inst_3 : HasImage g
⊢ CategoryStruct.comp (Y := image g) (factorThruImage g)
      (lift
          { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ :
            MonoFactorisation g } ≫
        preComp f g) =
    factorThruImage g ≫ 𝟙 (image g)

Tactic:
simp [image.preComp]

Premises used: CategoryTheory.Limits.image.preComp
-- 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)
rw : ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) ≫ g = ((Image.monoFactorisation f).compMono g).m
⊢ image.lift F'.ofCompIso ≫ F'.m = ((Image.monoFactorisation f).compMono g).m

Tactic:
rw [← Category.comp_id (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m),
            ← IsIso.inv_hom_id g, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.MonoFactorisation.ofCompIso, CategoryTheory.Limits.image.lift, 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) ≫ g = ((Image.monoFactorisation f).compMono g).m

Tactic:
congrArg (· ≫ g) ?_

Premises used: congrArg, CategoryTheory.Limits.image, CategoryTheory.CategoryStruct.comp
-- 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)
refine : (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m
⊢ ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) ≫ g = ((Image.monoFactorisation f).compMono g).m

Tactic:
refine congrArg (· ≫ g) ?_

Premises used: congrArg, CategoryTheory.CategoryStruct.comp