awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
B : C
⊢ Eq.{v₁ + 1} (α := Over.left.{v₁, u₁} (X := B) (ObjectProperty.FullSubcategory.obj (P := Over.isMono B) ⊥) ⟶ B)
    (arrow ⊥) 0

Tactic:
zero_of_source_iso_zero _ botCoeIsoZero

Premises used: CategoryTheory.Limits.zero_of_source_iso_zero, CategoryTheory.MonoOver.botCoeIsoZero
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
B : C
rw :
  Eq.{v₁ + 1} (α := initial.{v₁, u₁} C ⟶ B)
    (arrow ⊥ : Over.left.{v₁, u₁} (X := B) (ObjectProperty.FullSubcategory.obj (P := Over.isMono B) ⊥) ⟶ B) 0
rw₁ rw₂ : Eq.{v₁ + 1} (α := initial.{v₁, u₁} C ⟶ B) 0 0
⊢ Eq.{v₁ + 1} (α := initial.{v₁, u₁} C ⟶ B) (initial.to B) 0

Tactic:
rw [← bot_arrow, bot_arrow_eq_zero]

Premises used: CategoryTheory.MonoOver.bot_arrow, CategoryTheory.MonoOver.bot_arrow_eq_zero
-- 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
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
apply :
  ((pullback X_1.arrow ⋙ map X_1.arrow).obj g).obj (P := Over.isMono A).left ⟶
    ((pullback Y_1.arrow ⋙ map Y_1.arrow).obj g).obj (P := Over.isMono A).left
apply₁ :
  pullback.lift (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow)
        (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ⋯ ≫
      ((pullback Y_1.arrow ⋙ map Y_1.arrow).obj g).arrow =
    ((pullback X_1.arrow ⋙ map X_1.arrow).obj g).arrow
⊢ (pullback X_1.arrow ⋙ map X_1.arrow).obj g ⟶ (pullback Y_1.arrow ⋙ map Y_1.arrow).obj g

Tactic:
apply homMk _ _

Premises used: CategoryTheory.MonoOver.homMk
-- 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
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
apply :
  Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow ≫ (Functor.obj (forget A) g).hom)
    ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
⊢ ((pullback X_1.arrow ⋙ map X_1.arrow).obj g).obj (P := Over.isMono A).left ⟶
    ((pullback Y_1.arrow ⋙ map Y_1.arrow).obj g).obj (P := Over.isMono A).left

Tactic:
apply pullback.lift (pullback.fst _ _) (pullback.snd _ _ ≫ k.hom.left) _

Premises used: CategoryTheory.Limits.pullback.lift, CategoryTheory.Limits.pullback.snd, CategoryTheory.Over.Hom.left, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.InducedCategory.Hom.hom
-- 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
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
rw :
  Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
    ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
rw₁ :
  Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
    (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom ≫ Y_1.arrow)
rw₂ rw₃ :
  Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
    (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ X_1.arrow)
⊢ Eq (α := Limits.pullback (Functor.obj (forget A) g).hom X_1.arrow ⟶ A)
    (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow ≫ (Functor.obj (forget A) g).hom)
    ((pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)

Tactic:
rw [pullback.condition, assoc, w k]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoOver.w, CategoryTheory.Limits.pullback.condition
-- 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
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
dsimp :
  Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    (CategoryStruct.comp (Y := Limits.pullback g.arrow Y_1.arrow)
      (pullback.lift (pullback.fst g.obj (P := Over.isMono A).hom X_1.arrow)
        (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) ⋯)
      (pullback.snd g.obj (P := Over.isMono A).hom Y_1.arrow ≫ Y_1.arrow))
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
⊢ pullback.lift (pullback.fst (Functor.obj (forget A) g).hom X_1.arrow)
        (pullback.snd (Functor.obj (forget A) g).hom X_1.arrow ≫ Over.Hom.left k.hom) ⋯ ≫
      ((pullback Y_1.arrow ⋙ map Y_1.arrow).obj g).arrow =
    ((pullback X_1.arrow ⋙ map X_1.arrow).obj g).arrow

Tactic:
dsimp
-- 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
A : C
X_1 Y_1 : MonoOver.{v₁, u₁} A
k : X_1 ⟶ Y_1
g : MonoOver.{v₁, u₁} A
rw :
  Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    ((pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) ≫ Y_1.arrow)
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
rw₁ :
  Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom ≫ Y_1.arrow)
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
rw₂ rw₃ :
  Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A) (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)
⊢ Eq (α := Limits.pullback g.arrow X_1.arrow ⟶ A)
    (CategoryStruct.comp (Y := Limits.pullback g.arrow Y_1.arrow)
      (pullback.lift (pullback.fst g.obj (P := Over.isMono A).hom X_1.arrow)
        (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ Over.Hom.left k.hom) ⋯)
      (pullback.snd g.obj (P := Over.isMono A).hom Y_1.arrow ≫ Y_1.arrow))
    (pullback.snd g.obj (P := Over.isMono A).hom X_1.arrow ≫ X_1.arrow)

Tactic:
rw [pullback.lift_snd_assoc, assoc, w k]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_snd_assoc, CategoryTheory.MonoOver.w
-- 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
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : h ⟶ f
k₂ : h ⟶ g
⊢ Over.Hom.left k₂.hom ≫ (Functor.obj (forget A) g).hom = Over.Hom.left k₁.hom ≫ f.arrow

Tactic:
simp
-- 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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
refine :
  (coprod.inl ≫
        factorThruImage
          (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
              (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom) ≫
      ((Functor.obj sup f).obj g).arrow =
    f.arrow
⊢ f ⟶ (Functor.obj sup f).obj g

Tactic:
refine homMk (coprod.inl ≫ factorThruImage _) ?_

Premises used: CategoryTheory.Limits.coprod.inl, CategoryTheory.MonoOver.homMk, CategoryTheory.CategoryStruct.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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
erw : (Functor.obj (Functor.prod (forget A) (forget A)) (f, g)).1.hom = f.arrow
⊢ (coprod.inl ≫
        factorThruImage
          (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
              (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom) ≫
      ((Functor.obj sup f).obj g).arrow =
    f.arrow

Tactic:
erw [Category.assoc, image.fac, coprod.inl_desc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.fac, CategoryTheory.Limits.coprod.inl_desc
-- 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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
⊢ (Functor.obj (Functor.prod (forget A) (forget A)) (f, g)).1.hom = f.arrow

Tactic:
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
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
refine :
  (coprod.inr ≫
        factorThruImage
          (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
              (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom) ≫
      ((Functor.obj sup f).obj g).arrow =
    g.arrow
⊢ g ⟶ (Functor.obj sup f).obj g

Tactic:
refine homMk (coprod.inr ≫ factorThruImage _) ?_

Premises used: CategoryTheory.MonoOver.homMk, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.coprod.inr
-- 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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
erw : (Functor.obj (Functor.prod (forget A) (forget A)) (f, g)).2.hom = g.arrow
⊢ (coprod.inr ≫
        factorThruImage
          (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
              (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom) ≫
      ((Functor.obj sup f).obj g).arrow =
    g.arrow

Tactic:
erw [Category.assoc, image.fac, coprod.inr_desc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.fac, CategoryTheory.Limits.coprod.inr_desc
-- 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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g : MonoOver.{v₁, u₁} A
⊢ (Functor.obj (Functor.prod (forget A) (forget A)) (f, g)).2.hom = g.arrow

Tactic:
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
inst_2 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
refine_1 : ((Functor.obj sup f).obj g).obj (P := Over.isMono A).left ⟶ h.obj (P := Over.isMono A).left
refine_2 :
  image.lift
        { I := h.obj (P := Over.isMono A).left, m := h.arrow, m_mono := ⋯,
          e := coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom), fac := ⋯ } ≫
      h.arrow =
    ((Functor.obj sup f).obj g).arrow
⊢ (Functor.obj sup f).obj g ⟶ h

Tactic:
refine homMk ?_ ?_

Premises used: CategoryTheory.MonoOver.homMk
-- 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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
apply :
  coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
        (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom
⊢ ((Functor.obj sup f).obj g).obj (P := Over.isMono A).left ⟶ h.obj (P := Over.isMono A).left

Tactic:
apply image.lift ⟨_, h.arrow, coprod.desc k₁.hom.left k₂.hom.left, _⟩

Premises used: CategoryTheory.Limits.coprod.desc, CategoryTheory.Over.Hom.left, CategoryTheory.Limits.MonoFactorisation.mk, CategoryTheory.Limits.image.lift, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.MonoOver.arrow
-- 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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
h₁ :
  CategoryStruct.comp (Y := coprod.{v₁, u₁} f.obj (P := Over.isMono A).left g.obj (P := Over.isMono A).left) coprod.inl
      (coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow) =
    coprod.inl ≫
      (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
          (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom
h₂ :
  CategoryStruct.comp (Y := coprod.{v₁, u₁} f.obj (P := Over.isMono A).left g.obj (P := Over.isMono A).left) coprod.inr
      (coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow) =
    coprod.inr ≫
      (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
          (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom
⊢ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
        (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom

Tactic:
ext
-- 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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ CategoryStruct.comp (Y := coprod.{v₁, u₁} f.obj (P := Over.isMono A).left g.obj (P := Over.isMono A).left) coprod.inl
      (coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow) =
    coprod.inl ≫
      (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
          (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom

Tactic:
simp [w k₁]

Premises used: CategoryTheory.MonoOver.w
-- 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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ CategoryStruct.comp (Y := coprod.{v₁, u₁} f.obj (P := Over.isMono A).left g.obj (P := Over.isMono A).left) coprod.inr
      (coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow) =
    coprod.inr ≫
      (Functor.obj (Functor.obj Functor.uncurry Over.coprod)
          (Functor.obj (Functor.prod (forget A) (forget A)) (f, g))).hom

Tactic:
simp [w k₂]

Premises used: CategoryTheory.MonoOver.w
-- 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 : HasImages.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₁, u₁} C
A : C
f g h : MonoOver.{v₁, u₁} A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ image.lift
        { I := h.obj (P := Over.isMono A).left, m := h.arrow, m_mono := ⋯,
          e := coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom), fac := ⋯ } ≫
      h.arrow =
    ((Functor.obj sup f).obj g).arrow

Tactic:
apply image.lift_fac

Premises used: CategoryTheory.Limits.image.lift_fac
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
⊢ ∀ (a : Subobject.{v₁, u₁} X), a ≤ Quotient.mk'' ⊤

Tactic:
Quotient.ind' fun f => ?_

Premises used: CategoryTheory.ThinSkeleton, Quotient.ind', CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
refine : ∀ (f : MonoOver.{v₁, u₁} X), LE.le (α := Subobject.{v₁, u₁} X) (Quotient.mk'' f) (Quotient.mk'' ⊤)
⊢ ∀ (a : Subobject.{v₁, u₁} X), a ≤ Quotient.mk'' ⊤

Tactic:
refine Quotient.ind' fun f => ?_
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
f : MonoOver.{v₁, u₁} X
⊢ LE.le (α := Subobject.{v₁, u₁} X) (Quotient.mk'' f) (Quotient.mk'' ⊤)

Tactic:
⟨MonoOver.leTop f⟩

Premises used: CategoryTheory.MonoOver.leTop, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
f : MonoOver.{v₁, u₁} X
⊢ LE.le (α := Subobject.{v₁, u₁} X) (Quotient.mk'' f) (Quotient.mk'' ⊤)

Tactic:
exact ⟨MonoOver.leTop f⟩
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
⊢ Eq (α := Subobject.{v₁, u₁} B) ⊤ (mk (𝟙 B))

Tactic:
rfl

Premises used: CategoryTheory.Subobject.mk, Quotient.mk', rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
⊢ Eq.{v₁ + 1} (α := Functor.obj (C := Subobject.{v₁, u₁} B) underlying (mk (𝟙 B)) ⟶ B)
    (Iso.hom (underlyingIso (𝟙 B)) ≫ 𝟙 B) (arrow (mk (𝟙 B)))

Tactic:
underlyingIso_hom_comp_eq_mk (𝟙 B)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
h :
  Eq.{v₁ + 1} (α := Functor.obj (C := Subobject.{v₁, u₁} B) underlying (mk (𝟙 B)) ⟶ B) (Iso.hom (underlyingIso (𝟙 B)))
    (Iso.hom (underlyingIso (𝟙 B)) ≫ 𝟙 B)
⊢ Eq.{v₁ + 1} (α := Functor.obj (C := Subobject.{v₁, u₁} B) underlying (mk (𝟙 B)) ⟶ B) (Iso.hom (underlyingIso (𝟙 B)))
    (arrow ⊤)

Tactic:
convert! underlyingIso_hom_comp_eq_mk (𝟙 B)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
⊢ Eq.{v₁ + 1} (α := Functor.obj (C := Subobject.{v₁, u₁} B) underlying (mk (𝟙 B)) ⟶ B) (Iso.hom (underlyingIso (𝟙 B)))
    (Iso.hom (underlyingIso (𝟙 B)) ≫ 𝟙 B)

Tactic:
simp only [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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
B : C
rw : IsIso.{v₁, u₁} (X := Functor.obj (C := Subobject.{v₁, u₁} B) underlying ⊤) (Iso.hom (underlyingIso (𝟙 B)))
⊢ IsIso.{v₁, u₁} (C := C) (X := Functor.obj (C := Subobject.{v₁, u₁} B) underlying ⊤) (arrow ⊤)

Tactic:
rw [← underlyingIso_top_hom]

Premises used: CategoryTheory.Subobject.underlyingIso_top_hom
-- 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
B : C
⊢ IsIso.{v₁, u₁} (X := Functor.obj (C := Subobject.{v₁, u₁} B) underlying ⊤) (Iso.hom (underlyingIso (𝟙 B)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
⊢ Eq.{v₁ + 1} (α := B ⟶ B)
    (CategoryStruct.comp (Y := Functor.obj (C := Subobject.{v₁, u₁} B) underlying (mk (𝟙 B)))
      (Iso.inv (underlyingIso (𝟙 B))) (arrow ⊤))
    (𝟙 B)

Tactic:
underlyingIso_arrow _

Premises used: CategoryTheory.Subobject.underlyingIso_arrow, CategoryTheory.Subobject.mk, Quotient.mk'
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ (map f).obj ⊤ = mk f

Tactic:
Quotient.sound' ⟨MonoOver.mapTop f⟩

Premises used: Quotient.sound', CategoryTheory.MonoOver.mapTop, Quotient.map, Nonempty.intro, CategoryTheory.ThinSkeleton, CategoryTheory.Subobject.mk, Quotient.mk', Quot.map, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
⊢ Factors ⊤ f

Tactic:
⟨f, comp_id _⟩

Premises used: CategoryTheory.Subobject.Factors, CategoryTheory.MonoOver.Factors, Quotient.liftOn', CategoryTheory.Category.comp_id, Exists.intro
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h : mk f = ⊤
rw : IsIso (ofMkLEMk f (𝟙 Y) ⋯)
⊢ IsIso f

Tactic:
rw [← ofMkLEMk_comp h.le, Category.comp_id]

Premises used: Eq.le, CategoryTheory.Category.comp_id, CategoryTheory.Subobject.ofMkLEMk_comp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h : mk f = ⊤
⊢ IsIso (ofMkLEMk f (𝟙 Y) ⋯)

Tactic:
(isoOfMkEqMk _ _ h).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Subobject.isoOfMkEqMk, CategoryTheory.Subobject.ofMkLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h : mk f = ⊤
⊢ IsIso (ofMkLEMk f (𝟙 Y) ⋯)

Tactic:
exact (isoOfMkEqMk _ _ h).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Subobject.isoOfMkEqMk
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y : C
P : Subobject.{v₁, u₁} Y
rw : mk P.arrow = ⊤ ↔ P = ⊤
rw₁ rw₂ : P = ⊤ ↔ P = ⊤
⊢ IsIso P.arrow ↔ P = ⊤

Tactic:
rw [isIso_iff_mk_eq_top, mk_arrow]

Premises used: CategoryTheory.Subobject.mk_arrow, CategoryTheory.Subobject.isIso_iff_mk_eq_top
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
Y : C
rw rw₁ : Eq (α := Subobject.{v₁, u₁} Y) ⊤ ⊤
⊢ IsIso.{v₁, u₁} (C := C) (X := Functor.obj (C := Subobject.{v₁, u₁} Y) underlying ⊤) (arrow ⊤)

Tactic:
rw [isIso_arrow_iff_eq_top]

Premises used: CategoryTheory.Subobject.isIso_arrow_iff_eq_top
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ mk f = ⊤

Tactic:
(isIso_iff_mk_eq_top f).mp inferInstance

Premises used: inferInstance, Iff.mp, CategoryTheory.Subobject.isIso_iff_mk_eq_top
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y : C
P : Subobject.{v₁, u₁} Y
inst_1 : IsIso P.arrow
⊢ P = ⊤

Tactic:
(isIso_arrow_iff_eq_top P).mp inferInstance

Premises used: inferInstance, CategoryTheory.Subobject.isIso_arrow_iff_eq_top, Iff.mp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : Balanced.{v₁, u₁} C
f : X ⟶ Y
inst_2 : Mono f
rw : Epi f ↔ IsIso f
⊢ Epi f ↔ mk f = ⊤

Tactic:
rw [← isIso_iff_mk_eq_top]

Premises used: CategoryTheory.Subobject.isIso_iff_mk_eq_top
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : Balanced.{v₁, u₁} C
f : X ⟶ Y
inst_2 : Mono f
⊢ Epi f ↔ IsIso f

Tactic:
⟨fun _ ↦ isIso_of_mono_of_epi f, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : Balanced.{v₁, u₁} C
f : X ⟶ Y
inst_2 : Mono f
⊢ Epi f ↔ IsIso f

Tactic:
exact ⟨fun _ ↦ isIso_of_mono_of_epi f, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
⊢ (pullback f).obj ⊤ = ⊤

Tactic:
Quotient.sound' ⟨MonoOver.pullbackTop f⟩

Premises used: Quotient.sound', Quotient.map, Nonempty.intro, CategoryTheory.ThinSkeleton, CategoryTheory.MonoOver.pullbackTop, Quot.map, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A B : C
f : A ⟶ B
inst_2 : Mono f
⊢ (pullback f).obj (mk f) = ⊤

Tactic:
Quotient.sound' ⟨MonoOver.pullbackSelf f⟩

Premises used: Quotient.sound', CategoryTheory.MonoOver.pullbackSelf, Quotient.map, Nonempty.intro, CategoryTheory.ThinSkeleton, Quot.map, CategoryTheory.Subobject