awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Comma
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
h₁ : (Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op = (MonoOver.mk f).arrow.unop.left.op
⊢ LE.le (α :=
    { P : Subobject.{v₁, u₁} (op A.left) //
      ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
    (({
            toFun := fun (P : Subobject (op A)) ↦
              Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                (projectQuotient P) ⋯,
            invFun :=
              fun
                (P :
                  { P : Subobject.{v₁, u₁} (op A.left) //
                    ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom }) ↦
              liftQuotient (↑P : Subobject (op A.left)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subobject (op A)) →
            { P : Subobject (op A.left) //
              ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
        (Subobject.mk f) :
      { P : Subobject.{v₁, u₁} (op A.left) //
        ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
    (({
            toFun := fun (P : Subobject (op A)) ↦
              Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                (projectQuotient P) ⋯,
            invFun :=
              fun
                (P :
                  { P : Subobject.{v₁, u₁} (op A.left) //
                    ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom }) ↦
              liftQuotient (↑P : Subobject (op A.left)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subobject (op A)) →
            { P : Subobject (op A.left) //
              ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
        (Subobject.mk g) :
      { P : Subobject.{v₁, u₁} (op A.left) //
        ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })

Tactic:
refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).unop.left.op ?_

Premises used: Quiver.Hom.op, CategoryTheory.Subobject.mk_le_mk_of_comm, Quiver.Hom.unop, CategoryTheory.CommaMorphism.left, CategoryTheory.Subobject.ofMkLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Comma
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op = (MonoOver.mk f).arrow.unop.left.op

Tactic:
Quiver.Hom.unop_inj ?_

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Subobject.Comma
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
h₁ :
  Quiver.Hom.unop ((Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op) =
    (MonoOver.mk f).arrow.unop.left.op.unop
⊢ (Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op = (MonoOver.mk f).arrow.unop.left.op

Tactic:
refine Quiver.Hom.unop_inj ?_

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Subobject.Comma
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (Subobject.ofMkLEMk f g h ≫ g).unop = f.unop

Tactic:
have := congr_arg Quiver.Hom.unop (Subobject.ofMkLEMk_comp h)
-- Module: Mathlib.CategoryTheory.Subobject.Comma
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
this : (Subobject.ofMkLEMk f g h ≫ g).unop = f.unop
⊢ Quiver.Hom.unop ((Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op) =
    (MonoOver.mk f).arrow.unop.left.op.unop

Tactic:
simpa only [unop_op, Functor.id_obj, Functor.const_obj_obj, MonoOver.mk_obj, Over.mk_left,
        MonoOver.mk_arrow, unop_comp, Quiver.Hom.unop_op, comp_left]
          using congr_arg CommaMorphism.left this

Premises used: CategoryTheory.MonoOver.mk_arrow, CategoryTheory.MonoOver.mk_obj, CategoryTheory.Over.mk_left, Quiver.Hom.unop_op, CategoryTheory.unop_comp, congr_arg, CategoryTheory.CostructuredArrow.comp_left, CategoryTheory.CommaMorphism.left, CategoryTheory.Functor.id_obj, Opposite.unop_op, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
f g : MonoOver.{v₁, u₁} X
Y : C
h : Y ⟶ X
e : f ≅ g
h_1 : f.Factors h
u : Y ⟶ f.obj (P := Over.isMono X).left
hu : u ≫ f.arrow = h
⊢ (u ≫ Over.Hom.left (Functor.map (forget X) e.hom)) ≫ g.arrow = h

Tactic:
simp [hu]
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
f g : MonoOver.{v₁, u₁} X
Y : C
h : Y ⟶ X
e : f ≅ g
h_1 : g.Factors h
u : Y ⟶ g.obj (P := Over.isMono X).left
hu : u ≫ g.arrow = h
⊢ (u ≫ Over.Hom.left (Functor.map (forget X) e.inv)) ≫ f.arrow = h

Tactic:
simp [hu]
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
a : (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P ↔ (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q
⊢ Eq (α := Prop) ((fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P) ((fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q)

Tactic:
apply propext

Premises used: propext
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
a : (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P → (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q
a₁ : (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q → (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P
⊢ (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P ↔ (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ P.obj (P := Over.isMono Y).left
w : i ≫ P.arrow = f
rw : i ≫ Over.Hom.left h.hom.hom ≫ Q.arrow = f
rw₁ : i ≫ P.obj (P := Over.isMono Y).hom = f
rw₂ rw₃ : f = f
⊢ (i ≫ Over.Hom.left h.hom.hom) ≫ Q.arrow = f

Tactic:
rw [Category.assoc, Over.w h.hom.hom, w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Over.w, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ P.obj (P := Over.isMono Y).left
w : i ≫ P.arrow = f
⊢ Q.Factors f

Tactic:
exact ⟨i ≫ h.hom.hom.left, by rw [Category.assoc, Over.w h.hom.hom, w]⟩
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ Q.obj (P := Over.isMono Y).left
w : i ≫ Q.arrow = f
rw : i ≫ Over.Hom.left h.inv.hom ≫ P.arrow = f
rw₁ : i ≫ Q.obj (P := Over.isMono Y).hom = f
rw₂ rw₃ : f = f
⊢ (i ≫ Over.Hom.left h.inv.hom) ≫ P.arrow = f

Tactic:
rw [Category.assoc, Over.w h.inv.hom, w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Over.w, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ Q.obj (P := Over.isMono Y).left
w : i ≫ Q.arrow = f
⊢ P.Factors f

Tactic:
exact ⟨i ≫ h.inv.hom.left, by rw [Category.assoc, Over.w h.inv.hom, w]⟩
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
inst_1 : Mono f
g : Z ⟶ X
⊢ (mk f).Factors g ↔ (MonoOver.mk f).Factors g

Tactic:
Iff.rfl

Premises used: CategoryTheory.Subobject.Factors, CategoryTheory.MonoOver.Factors, Quotient.liftOn', Iff.rfl
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ 𝟙 X ≫ (MonoOver.mk f).arrow = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Y
⊢ P.Factors f ↔ (Functor.obj representative P).Factors f

Tactic:
Quot.inductionOn P fun _ => MonoOver.factors_congr _ (representativeIso _).symm

Premises used: Quot.inductionOn
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Subobject.{v₁, u₁} X
⊢ 𝟙 (Functor.obj underlying P) ≫ (Functor.obj representative P).arrow = P.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Functor.obj underlying P
⊢ P.Factors (f ≫ P.arrow)

Tactic:
(factors_iff _ _).mpr ⟨f, rfl⟩

Premises used: CategoryTheory.Subobject.factors_iff, Iff.mpr, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
P : Subobject.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
h₁ : ∀ (a : MonoOver.{v₁, u₁} Z) (h : Factors (Quotient.mk'' a) g), Factors (Quotient.mk'' a) (f ≫ g)
⊢ P.Factors (f ≫ g)

Tactic:
induction P using Quotient.ind'
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
a : MonoOver.{v₁, u₁} Z
h : Factors (Quotient.mk'' a) g
h₁ : ∀ (g : Y ⟶ a.obj (P := Over.isMono Z).left), Factors (Quotient.mk'' a) (f ≫ g ≫ a.arrow)
⊢ Factors (Quotient.mk'' a) (f ≫ g)

Tactic:
obtain ⟨g, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
a : MonoOver.{v₁, u₁} Z
g : Y ⟶ a.obj (P := Over.isMono Z).left
⊢ (f ≫ g) ≫ a.arrow = f ≫ g ≫ a.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
a : MonoOver.{v₁, u₁} Z
g : Y ⟶ a.obj (P := Over.isMono Z).left
⊢ Factors (Quotient.mk'' a) (f ≫ g ≫ a.arrow)

Tactic:
exact ⟨f ≫ g, by simp⟩
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
⊢ Eq (α := X ⟶ Y) (0 ≫ (Functor.obj representative P).arrow) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject.{v₁, u₁} Y
f : Z ⟶ Y
h : P ≤ Q
simp : (Functor.obj representative P).Factors f → (Functor.obj representative Q).Factors f
⊢ P.Factors f → Q.Factors f

Tactic:
simp only [factors_iff]

Premises used: CategoryTheory.Subobject.factors_iff
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject.{v₁, u₁} Y
f : Z ⟶ Y
h : P ≤ Q
h_1 : (Functor.obj representative P).Factors f
u : Z ⟶ (Functor.obj representative P).obj (P := Over.isMono Y).left
hu : u ≫ (Functor.obj representative P).arrow = f
⊢ (u ≫ P.ofLE Q h) ≫ (Functor.obj representative Q).arrow = f

Tactic:
simp [← hu]
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject.{v₁, u₁} Y
f : Z ⟶ Y
h : P ≤ Q
⊢ (Functor.obj representative P).Factors f → (Functor.obj representative Q).Factors f

Tactic:
exact fun ⟨u, hu⟩ => ⟨u ≫ ofLE _ _ h, by simp [← hu]⟩
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Y
h : P.Factors f
⊢ P.factorThru f h ≫ P.arrow = f

Tactic:
Classical.choose_spec ((factors_iff _ _).mp h)

Premises used: CategoryTheory.Subobject.factors_iff, CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.factorThru, Classical.choose_spec, Iff.mp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Subobject.{v₁, u₁} X
h : P.Factors P.arrow
h₁ : P.factorThru P.arrow h ≫ P.arrow = 𝟙 (Functor.obj underlying P) ≫ P.arrow
⊢ P.factorThru P.arrow h = 𝟙 (Functor.obj underlying P)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Subobject.{v₁, u₁} X
h : P.Factors P.arrow
⊢ P.factorThru P.arrow h ≫ P.arrow = 𝟙 (Functor.obj underlying P) ≫ P.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h : (mk f).factorThru f ⋯ ≫ (mk f).arrow = Iso.inv (underlyingIso f) ≫ (mk f).arrow
⊢ (mk f).factorThru f ⋯ = Iso.inv (underlyingIso f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ (mk f).factorThru f ⋯ ≫ (mk f).arrow = Iso.inv (underlyingIso f) ≫ (mk f).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Functor.obj underlying P
h : P.Factors (f ≫ P.arrow)
h₁ : P.factorThru (f ≫ P.arrow) h ≫ P.arrow = f ≫ P.arrow
⊢ P.factorThru (f ≫ P.arrow) h = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Functor.obj underlying P
h : P.Factors (f ≫ P.arrow)
⊢ P.factorThru (f ≫ P.arrow) h ≫ P.arrow = f ≫ P.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Y
h : P.Factors f
mp : P.factorThru f h = 0 → f = 0
mpr : f = 0 → P.factorThru f h = 0
⊢ P.factorThru f h = 0 ↔ f = 0

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Y
h : P.Factors f
w : P.factorThru f h = 0
⊢ P.factorThru f h ≫ P.arrow = 0 ≫ P.arrow

Tactic:
replace w := w =≫ P.arrow
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f : X ⟶ Y
h : P.Factors f
w : P.factorThru f h ≫ P.arrow = 0 ≫ P.arrow
⊢ f = 0

Tactic:
simpa using w
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
h : P.Factors (X := X) 0
mpr : P.factorThru 0 h ≫ P.arrow = 0 ≫ P.arrow
⊢ P.factorThru 0 h = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
h : P.Factors (X := X) 0
⊢ P.factorThru 0 h ≫ P.arrow = 0 ≫ P.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
P : Subobject.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
apply : (f ≫ P.factorThru g h) ≫ P.arrow = P.factorThru (f ≫ g) ⋯ ≫ P.arrow
⊢ f ≫ P.factorThru g h = P.factorThru (f ≫ g) ⋯

Tactic:
apply (cancel_mono P.arrow).mp

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
P : Subobject.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ (f ≫ P.factorThru g h) ≫ P.arrow = P.factorThru (f ≫ g) ⋯ ≫ P.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
h : P.Factors (X := X) 0
⊢ P.factorThru 0 h = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject.{v₁, u₁} Y
f : Z ⟶ Y
h : P ≤ Q
w : P.Factors f
h₁ : Q.factorThru f ⋯ ≫ Q.arrow = (P.factorThru f w ≫ P.ofLE Q h) ≫ Q.arrow
⊢ Q.factorThru f ⋯ = P.factorThru f w ≫ P.ofLE Q h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject.{v₁, u₁} Y
f : Z ⟶ Y
h : P ≤ Q
w : P.Factors f
⊢ Q.factorThru f ⋯ ≫ Q.arrow = (P.factorThru f w ≫ P.ofLE Q h) ≫ Q.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y : C
P Q : Subobject.{v₁, u₁} Y
h : Q.Factors P.arrow
⊢ P ≤ Q

Tactic:
le_of_comm (Q.factorThru P.arrow h) (Q.factorThru_arrow P.arrow h)

Premises used: CategoryTheory.Subobject.le_of_comm, CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.factorThru, CategoryTheory.Subobject.factorThru_arrow
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
wf : P.Factors f
wg : P.Factors g
⊢ (P.factorThru f wf + P.factorThru g wg) ≫ (Functor.obj representative P).arrow = f + g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
wg : P.Factors g
h : P.factorThru (f + g) w ≫ P.arrow = (P.factorThru f wf + P.factorThru g wg) ≫ P.arrow
⊢ P.factorThru (f + g) w = P.factorThru f wf + P.factorThru g wg

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
wg : P.Factors g
⊢ P.factorThru (f + g) w ≫ P.arrow = (P.factorThru f wf + P.factorThru g wg) ≫ P.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ (P.factorThru (f + g) w - P.factorThru g wg) ≫ (Functor.obj representative P).arrow = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
h : (P.factorThru (f + g) w - P.factorThru g wg) ≫ P.arrow = P.factorThru f ⋯ ≫ P.arrow
⊢ P.factorThru (f + g) w - P.factorThru g wg = P.factorThru f ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ (P.factorThru (f + g) w - P.factorThru g wg) ≫ P.arrow = P.factorThru f ⋯ ≫ P.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ (P.factorThru (f + g) w - P.factorThru f wf) ≫ (Functor.obj representative P).arrow = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
h : (P.factorThru (f + g) w - P.factorThru f wf) ≫ P.arrow = P.factorThru g ⋯ ≫ P.arrow
⊢ P.factorThru (f + g) w - P.factorThru f wf = P.factorThru g ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.FactorThru
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : C
P : Subobject.{v₁, u₁} Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ (P.factorThru (f + g) w - P.factorThru f wf) ≫ P.arrow = P.factorThru g ⋯ ≫ P.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
Y : C
κ : Cardinal.{w}
h : HasCardinalLT (Subobject.{v, u} Y) κ
X : C
f : X ⟶ Y
inst_1 : Mono f
⊢ HasCardinalLT (Subobject.{v, u} X) κ

Tactic:
h.of_injective _ (map_obj_injective f)

Premises used: HasCardinalLT.of_injective, CategoryTheory.Subobject.map_obj_injective
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Over.left.{v₁, u₁} (X := X) (ObjectProperty.FullSubcategory.obj (P := Over.isMono X) ⊤) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := Over.left.{v₁, u₁} (X := X) (ObjectProperty.FullSubcategory.obj (P := Over.isMono X) ⊤) ⟶ X)
    (arrow ⊤) (𝟙 X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
f : X ⟶ Y
inst_2 : Mono f
⊢ 𝟙 (mk f).obj (P := Over.isMono Y).left ≫ ((map f).obj ⊤).arrow = (mk f).arrow

Tactic:
simp [id_comp f]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
⊢ f ≫ Over.hom (Functor.obj (forget Y) ⊤) =
    𝟙 (Over.left.{v₁, u₁} (X := X) (ObjectProperty.FullSubcategory.obj (P := Over.isMono X) ⊤)) ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} C
inst_2 : InitialMonoClass.{v₁, u₁} C
X : C
⊢ Over.left.{v₁, u₁} (X := X) (ObjectProperty.FullSubcategory.obj (P := Over.isMono X) ⊥) = initial.{v₁, u₁} C

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} C
inst_2 : InitialMonoClass.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := Over.left.{v₁, u₁} (X := X) (ObjectProperty.FullSubcategory.obj (P := Over.isMono X) ⊥) ⟶ X)
    (arrow ⊥) (initial.to X)

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit.desc, rfl