awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst_1 : Mono f
X : Subobject.{v₁, u₁} B
g : A₂ ⟶ B
inst_2 : Mono g
h₁ : mk f ≤ X
h₂ : X ≤ mk g
⊢ Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso g) =
    Iso.inv (underlyingIso f) ≫ Functor.map underlying ⋯.hom ≫ Iso.hom (underlyingIso g)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst_1 : Mono f
g : A₂ ⟶ B
inst_2 : Mono g
X : Subobject.{v₁, u₁} B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
simp :
  Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) =
    Iso.inv (underlyingIso f) ≫ Functor.map underlying ⋯.hom
⊢ ofMkLEMk f g h₁ ≫ ofMkLE g X h₂ = ofMkLE f X ⋯

Tactic:
simp only [ofMkLE, ofLE, ofMkLEMk, ← Functor.map_comp underlying,
    assoc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.underlying, CategoryTheory.Subobject.ofLE, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Subobject.ofMkLEMk, CategoryTheory.Subobject.ofMkLE
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst_1 : Mono f
g : A₂ ⟶ B
inst_2 : Mono g
X : Subobject.{v₁, u₁} B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
⊢ Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) =
    Iso.inv (underlyingIso f) ≫ Functor.map underlying ⋯.hom

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ A₃ : C
f : A₁ ⟶ B
inst_1 : Mono f
g : A₂ ⟶ B
inst_2 : Mono g
h : A₃ ⟶ B
inst_3 : Mono h
h₁ : mk f ≤ mk g
h₂ : mk g ≤ mk h
simp :
  Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso h) =
    Iso.inv (underlyingIso f) ≫ Functor.map underlying ⋯.hom ≫ Iso.hom (underlyingIso h)
⊢ ofMkLEMk f g h₁ ≫ ofMkLEMk g h h₂ = ofMkLEMk f h ⋯

Tactic:
simp only [ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc,
    Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.underlying, CategoryTheory.Subobject.ofLE, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Subobject.ofMkLEMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ A₂ A₃ : C
f : A₁ ⟶ B
inst_1 : Mono f
g : A₂ ⟶ B
inst_2 : Mono g
h : A₃ ⟶ B
inst_3 : Mono h
h₁ : mk f ≤ mk g
h₂ : mk g ≤ mk h
⊢ Iso.inv (underlyingIso f) ≫ Functor.map underlying (h₁.hom ≫ h₂.hom) ≫ Iso.hom (underlyingIso h) =
    Iso.inv (underlyingIso f) ≫ Functor.map underlying ⋯.hom ≫ Iso.hom (underlyingIso h)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X : Subobject.{v₁, u₁} B
apply : X.ofLE X ⋯ ≫ X.arrow = 𝟙 (Functor.obj underlying X) ≫ X.arrow
⊢ X.ofLE X ⋯ = 𝟙 (Functor.obj underlying X)

Tactic:
apply (cancel_mono X.arrow).mp

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B : C
X : Subobject.{v₁, u₁} B
⊢ X.ofLE X ⋯ ≫ X.arrow = 𝟙 (Functor.obj underlying X) ≫ X.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst_1 : Mono f
apply : ofMkLEMk f f ⋯ ≫ f = 𝟙 A₁ ≫ f
⊢ ofMkLEMk f f ⋯ = 𝟙 A₁

Tactic:
apply (cancel_mono f).mp

Premises used: CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst_1 : Mono f
⊢ ofMkLEMk f f ⋯ ≫ f = 𝟙 A₁ ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
inl : mk i₁ < mk i₂ → mk i₁ < mk i₂
inr : ∀ (h : mk i₁ = mk i₂), mk i₁ < mk i₂
⊢ mk i₁ < mk i₂

Tactic:
obtain _ | h := (mk_le_mk_of_comm _ fac).lt_or_eq

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm, LE.le.lt_or_eq
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ < mk i₂
⊢ mk i₁ < mk i₂

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
inr : False
⊢ mk i₁ < mk i₂

Tactic:
exfalso
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
inr : IsIso f
⊢ False

Tactic:
apply hf
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ IsIso (isoOfMkEqMk i₁ i₂ h).hom

Tactic:
(isoOfMkEqMk i₁ i₂ h).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Subobject.isoOfMkEqMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
h₁ : f = (isoOfMkEqMk i₁ i₂ h).hom
⊢ IsIso f

Tactic:
convert! (isoOfMkEqMk i₁ i₂ h).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Subobject.isoOfMkEqMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
h₁ : f ≫ i₂ = (isoOfMkEqMk i₁ i₂ h).hom ≫ i₂
h₂ : f ≫ i₂ = ofMkLEMk i₁ i₂ ⋯ ≫ i₂
h₃ : f ≫ i₂ = i₁
h₄ h₅ : i₁ = i₁
⊢ f = (isoOfMkEqMk i₁ i₂ h).hom

Tactic:
rw [← cancel_mono i₂, isoOfMkEqMk_hom, ofMkLEMk_comp, fac]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Subobject.ofMkLEMk_comp, CategoryTheory.Subobject.isoOfMkEqMk_hom
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
h : mk i₁ < mk i₂
hf : IsIso f
⊢ False

Tactic:
simp only [mk_eq_mk_of_comm i₁ i₂ (asIso f) fac, lt_self_iff_false] at h

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, lt_self_iff_false, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P Q : MonoOver.{v₁, u₁} X
f : P ⟶ Q
⊢ Over.Hom.left f.hom ≫ Q.obj (P := Over.isMono X).hom = P.obj (P := Over.isMono X).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P Q : MonoOver.{v₁, u₁} X
f : P ⟶ Q
h : IsIso (Over.Hom.left f.hom)
⊢ (asIso (Over.Hom.left f.hom)).hom ≫ Q.obj (P := Over.isMono X).hom = P.obj (P := Over.isMono X).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P Q : MonoOver.{v₁, u₁} X
f : P ⟶ Q
h : Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom
⊢ Over.Hom.left f.hom ≫ Subobject.ofMkLEMk Q.obj (P := Over.isMono X).hom P.obj (P := Over.isMono X).hom ⋯ =
    𝟙 P.obj (P := Over.isMono X).left

Tactic:
simp [← cancel_mono P.1.hom]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.cancel_mono, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P Q : MonoOver.{v₁, u₁} X
f : P ⟶ Q
h : Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom
⊢ Subobject.ofMkLEMk Q.obj (P := Over.isMono X).hom P.obj (P := Over.isMono X).hom ⋯ ≫ Over.Hom.left f.hom =
    𝟙 Q.obj (P := Over.isMono X).left

Tactic:
simp [← cancel_mono Q.1.hom]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.cancel_mono, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P Q : MonoOver.{v₁, u₁} X
f : P ⟶ Q
rw :
  IsIso (Over.Hom.left f.hom) ↔
    Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom
rw₁ rw₂ :
  Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom ↔
    Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom
⊢ IsIso f ↔ Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom

Tactic:
rw [isIso_iff_isIso_hom_left, isIso_hom_left_iff_subobjectMk_eq]

Premises used: CategoryTheory.MonoOver.isIso_hom_left_iff_subobjectMk_eq, CategoryTheory.MonoOver.isIso_iff_isIso_hom_left
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F₁ F₂ : MonoOver.{v₁, u₁} X ⥤ MonoOver.{v₁, u₁} Y
h : F₁ ≅ F₂
⊢ lower F₁ = lower F₂

Tactic:
ThinSkeleton.map_iso_eq h

Premises used: CategoryTheory.ThinSkeleton.map_iso_eq, CategoryTheory.ThinSkeleton, CategoryTheory.Subobject, CategoryTheory.Subobject.lower
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : MonoOver.{v₁, u₁} Y ⥤ MonoOver.{v₁, u₁} X
⊢ toThinSkeleton (MonoOver.{v₁, u₁} Y) ⋙ lower F = F ⋙ toThinSkeleton (MonoOver.{v₁, u₁} X)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ThinSkeleton, Quotient, CategoryTheory.toThinSkeleton, Quotient.mk', CategoryTheory.homOfLE, rfl, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
p : 𝟭 (Subobject.{v₁, u₁} A) = lower e.functor ⋙ lower e.inverse
⊢ 𝟭 (Subobject.{v₁, u₁} A) ≅ lower e.functor ⋙ lower e.inverse

Tactic:
apply eqToIso

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ ThinSkeleton.map (𝟭 (MonoOver.{v₁, u₁} A)) = ThinSkeleton.map (e.functor ⋙ e.inverse)

Tactic:
ThinSkeleton.map_iso_eq e.unitIso

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.ThinSkeleton.map_iso_eq
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
h :
  Eq (α := Subobject.{v₁, u₁} A ⥤ Subobject.{v₁, u₁} A) (𝟭 (Subobject.{v₁, u₁} A))
    (ThinSkeleton.map (𝟭 (MonoOver.{v₁, u₁} A)))
h₁ : lower e.functor ⋙ lower e.inverse = ThinSkeleton.map (e.functor ⋙ e.inverse)
⊢ 𝟭 (Subobject.{v₁, u₁} A) = lower e.functor ⋙ lower e.inverse

Tactic:
convert! ThinSkeleton.map_iso_eq e.unitIso

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.ThinSkeleton.map_iso_eq
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ Eq (α := Subobject.{v₁, u₁} A ⥤ Subobject.{v₁, u₁} A) (𝟭 (Subobject.{v₁, u₁} A))
    (ThinSkeleton.map (𝟭 (MonoOver.{v₁, u₁} A)))

Tactic:
ThinSkeleton.map_id_eq.symm

Premises used: CategoryTheory.ThinSkeleton, CategoryTheory.ThinSkeleton.map_id_eq, Eq.symm, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ Eq (α := Subobject.{v₁, u₁} A ⥤ Subobject.{v₁, u₁} A) (𝟭 (Subobject.{v₁, u₁} A))
    (ThinSkeleton.map (𝟭 (MonoOver.{v₁, u₁} A)))

Tactic:
exact ThinSkeleton.map_id_eq.symm

Premises used: CategoryTheory.ThinSkeleton.map_id_eq, Eq.symm
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ lower e.functor ⋙ lower e.inverse = ThinSkeleton.map (e.functor ⋙ e.inverse)

Tactic:
(ThinSkeleton.map_comp_eq _ _).symm

Premises used: CategoryTheory.ThinSkeleton, Eq.symm, CategoryTheory.ThinSkeleton.map_comp_eq, CategoryTheory.Subobject, CategoryTheory.Subobject.lower
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ lower e.functor ⋙ lower e.inverse = ThinSkeleton.map (e.functor ⋙ e.inverse)

Tactic:
exact (ThinSkeleton.map_comp_eq _ _).symm

Premises used: Eq.symm, CategoryTheory.ThinSkeleton.map_comp_eq
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
p : lower e.inverse ⋙ lower e.functor = 𝟭 (Subobject.{v₂, u₂} B)
⊢ lower e.inverse ⋙ lower e.functor ≅ 𝟭 (Subobject.{v₂, u₂} B)

Tactic:
apply eqToIso

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ ThinSkeleton.map (e.inverse ⋙ e.functor) = ThinSkeleton.map (𝟭 (MonoOver.{v₂, u₂} B))

Tactic:
ThinSkeleton.map_iso_eq e.counitIso

Premises used: CategoryTheory.ThinSkeleton.map_iso_eq, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
h : lower e.inverse ⋙ lower e.functor = ThinSkeleton.map (e.inverse ⋙ e.functor)
h₁ :
  Eq (α := Subobject.{v₂, u₂} B ⥤ Subobject.{v₂, u₂} B) (𝟭 (Subobject.{v₂, u₂} B))
    (ThinSkeleton.map (𝟭 (MonoOver.{v₂, u₂} B)))
⊢ lower e.inverse ⋙ lower e.functor = 𝟭 (Subobject.{v₂, u₂} B)

Tactic:
convert! ThinSkeleton.map_iso_eq e.counitIso

Premises used: CategoryTheory.ThinSkeleton.map_iso_eq, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ lower e.inverse ⋙ lower e.functor = ThinSkeleton.map (e.inverse ⋙ e.functor)

Tactic:
(ThinSkeleton.map_comp_eq _ _).symm

Premises used: CategoryTheory.ThinSkeleton, Eq.symm, CategoryTheory.ThinSkeleton.map_comp_eq, CategoryTheory.Subobject, CategoryTheory.Subobject.lower
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ lower e.inverse ⋙ lower e.functor = ThinSkeleton.map (e.inverse ⋙ e.functor)

Tactic:
exact (ThinSkeleton.map_comp_eq _ _).symm

Premises used: Eq.symm, CategoryTheory.ThinSkeleton.map_comp_eq
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ Eq (α := Subobject.{v₂, u₂} B ⥤ Subobject.{v₂, u₂} B) (𝟭 (Subobject.{v₂, u₂} B))
    (ThinSkeleton.map (𝟭 (MonoOver.{v₂, u₂} B)))

Tactic:
ThinSkeleton.map_id_eq.symm

Premises used: CategoryTheory.ThinSkeleton, CategoryTheory.ThinSkeleton.map_id_eq, Eq.symm, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ Eq (α := Subobject.{v₂, u₂} B ⥤ Subobject.{v₂, u₂} B) (𝟭 (Subobject.{v₂, u₂} B))
    (ThinSkeleton.map (𝟭 (MonoOver.{v₂, u₂} B)))

Tactic:
exact ThinSkeleton.map_id_eq.symm

Premises used: CategoryTheory.ThinSkeleton.map_id_eq, Eq.symm
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u₃
inst_2 : Category.{v₃, u₃} J
inst_3 : HasLimitsOfShape J (Over.{v₁, u₁} X)
⊢ HasLimitsOfShape J (Subobject.{v₁, u₁} X)

Tactic:
apply hasLimitsOfShape_thinSkeleton

Premises used: CategoryTheory.Limits.hasLimitsOfShape_thinSkeleton
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u₃
inst_2 : Category.{v₃, u₃} J
inst_3 : HasFiniteLimits (Over.{v₁, u₁} X)
x : Type
x_1 : SmallCategory x
x_2 : FinCategory x
⊢ HasLimitsOfShape x (Subobject.{v₁, u₁} X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u₃
inst_2 : Category.{v₃, u₃} J
inst_3 : HasLimitsOfSize.{w, w', v₁, max u₁ v₁} (Over.{v₁, u₁} X)
x : Type w'
x_1 : Category.{w, w'} x
⊢ HasLimitsOfShape x (Subobject.{v₁, u₁} X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasCoproducts.{w', v₁, u₁} C
inst_3 : HasStrongEpiMonoFactorisations.{v₁, u₁} C
⊢ HasColimitsOfSize.{w, w', max u₁ v₁, max u₁ v₁} (Subobject.{v₁, u₁} X)

Tactic:
apply hasColimitsOfSize_thinSkeleton

Premises used: CategoryTheory.Limits.hasColimitsOfSize_thinSkeleton
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : HasPullbacks.{v₁, u₁} C
x : Subobject.{v₁, u₁} X
h : ∀ (f : MonoOver.{v₁, u₁} X), Functor.obj (pullback (𝟙 X)) (Quotient.mk'' f) = Quotient.mk'' f
⊢ Functor.obj (pullback (𝟙 X)) x = x

Tactic:
induction x using Quotient.inductionOn' with | _ f
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : MonoOver.{v₁, u₁} X
⊢ Functor.obj (pullback (𝟙 X)) (Quotient.mk'' f) = Quotient.mk'' f

Tactic:
Quotient.sound ⟨MonoOver.pullbackId.app f⟩

Premises used: CategoryTheory.MonoOver.pullbackId, Quotient.map, Nonempty.intro, CategoryTheory.ThinSkeleton, Quot.map, Quotient.sound, CategoryTheory.Iso.app, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : MonoOver.{v₁, u₁} X
⊢ Functor.obj (pullback (𝟙 X)) (Quotient.mk'' f) = Quotient.mk'' f

Tactic:
exact Quotient.sound ⟨MonoOver.pullbackId.app f⟩
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
g : Y ⟶ Z
x : Subobject.{v₁, u₁} Z
h :
  ∀ (t : MonoOver.{v₁, u₁} Z),
    (pullback (f ≫ g)).obj (Quotient.mk'' t) = (pullback f).obj ((pullback g).obj (Quotient.mk'' t))
⊢ (pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x)

Tactic:
induction x using Quotient.inductionOn' with | _ t
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
g : Y ⟶ Z
t : MonoOver.{v₁, u₁} Z
⊢ (pullback (f ≫ g)).obj (Quotient.mk'' t) = (pullback f).obj ((pullback g).obj (Quotient.mk'' t))

Tactic:
Quotient.sound ⟨(MonoOver.pullbackComp _ _).app t⟩

Premises used: CategoryTheory.MonoOver.pullbackComp, Quotient.map, Nonempty.intro, CategoryTheory.ThinSkeleton, Quot.map, Quotient.sound, CategoryTheory.Iso.app, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
g : Y ⟶ Z
t : MonoOver.{v₁, u₁} Z
⊢ (pullback (f ≫ g)).obj (Quotient.mk'' t) = (pullback f).obj ((pullback g).obj (Quotient.mk'' t))

Tactic:
exact Quotient.sound ⟨(MonoOver.pullbackComp _ _).app t⟩
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A B X Y : C
f : Y ⟶ X
i : A ⟶ X
inst_2 : Mono i
j : B ⟶ Y
inst_3 : Mono j
f' : B ⟶ A
h : IsPullback f' j i f
⊢ (pullback f).obj (mk i) = mk j

Tactic:
((equivMonoOver Y).inverse.mapIso
    (MonoOver.pullbackObjIsoOfIsPullback _ _ _ _ h)).to_eq

Premises used: CategoryTheory.Iso.to_eq, Quotient.map, CategoryTheory.Subobject.equivMonoOver, CategoryTheory.MonoOver.pullbackObjIsoOfIsPullback, CategoryTheory.Subobject.mk, Quot.map, CategoryTheory.Functor.mapIso, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
f : Y ⟶ X
x : Subobject.{v₁, u₁} X
obtain :
  ∀ (Z : C) (i : Z ⟶ X) (w : Mono i),
    (pullback f).obj (mk i) = mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)
⊢ (pullback f).obj x = mk (A := Limits.pullback x.arrow f) (pullback.snd x.arrow f)

Tactic:
obtain ⟨Z, i, _, rfl⟩ := mk_surjective x

Premises used: CategoryTheory.Subobject.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w : Mono i
rw :
  mk (A := Limits.pullback i f) (pullback.snd i f) =
    mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)
⊢ (pullback f).obj (mk i) = mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)

Tactic:
rw [pullback_obj_mk (IsPullback.of_hasPullback i f)]

Premises used: CategoryTheory.Subobject.pullback_obj_mk, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w : Mono i
⊢ i ≫ 𝟙 X = Iso.inv (underlyingIso i) ≫ (mk i).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w : Mono i
⊢ f ≫ 𝟙 X = 𝟙 Y ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w : Mono i
⊢ Eq (α := Limits.pullback i f ⟶ Y)
    (CategoryStruct.comp (Y := Limits.pullback (mk i).arrow f)
      (Iso.hom (asIso (pullback.map i f (mk i).arrow f (Iso.inv (underlyingIso i)) (𝟙 Y) (𝟙 X) ⋯ ⋯)))
      (pullback.snd (mk i).arrow f))
    (pullback.snd i f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w : Mono i
⊢ mk (A := Limits.pullback i f) (pullback.snd i f) =
    mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)

Tactic:
exact mk_eq_mk_of_comm _ _ (asIso (pullback.map i f (mk i).arrow f
    (underlyingIso i).inv (𝟙 _) (𝟙 _) (by simp) (by simp))) (by simp)

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.CategoryStruct.id, CategoryTheory.Subobject.underlyingIso, CategoryTheory.Subobject.mk, CategoryTheory.Limits.pullback.map, CategoryTheory.Iso.inv, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
y : Subobject.{v₁, u₁} Y
obtain :
  ∀ (A : C) (i : A ⟶ Y) (w : Mono i),
    ∃ (φ : Functor.obj underlying ((pullback f).obj (mk i)) ⟶ Functor.obj underlying (mk i)),
      IsPullback φ ((pullback f).obj (mk i)).arrow (mk i).arrow f
⊢ ∃ (φ : Functor.obj underlying ((pullback f).obj y) ⟶ Functor.obj underlying y),
    IsPullback φ ((pullback f).obj y).arrow y.arrow f

Tactic:
obtain ⟨A, i, ⟨_, rfl⟩⟩ := mk_surjective y

Premises used: CategoryTheory.Subobject.mk_surjective, rfl