awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
A : C
i : A ⟶ Y
w : Mono i
rw :
  ∃ (φ :
    Functor.obj underlying (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)) ⟶
      Functor.obj underlying (mk i)),
    IsPullback φ (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)).arrow (mk i).arrow f
⊢ ∃ (φ : Functor.obj underlying ((pullback f).obj (mk i)) ⟶ Functor.obj underlying (mk i)),
    IsPullback φ ((pullback f).obj (mk i)).arrow (mk i).arrow f

Tactic:
rw [pullback_obj]

Premises used: CategoryTheory.Subobject.pullback_obj
-- 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
A : C
i : A ⟶ Y
w : Mono i
exists :
  IsPullback (Iso.hom (underlyingIso (pullback.snd (mk i).arrow f)) ≫ pullback.fst (mk i).arrow f)
    (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)).arrow (mk i).arrow f
⊢ ∃ (φ :
    Functor.obj underlying (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)) ⟶
      Functor.obj underlying (mk i)),
    IsPullback φ (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)).arrow (mk i).arrow f

Tactic:
exists (underlyingIso (pullback.snd (mk i).arrow f)).hom ≫ pullback.fst (mk i).arrow f

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Limits.pullback.snd, CategoryTheory.Subobject.underlyingIso, CategoryTheory.Subobject.mk, CategoryTheory.Limits.pullback.fst, CategoryTheory.Iso.hom
-- 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
A : C
i : A ⟶ Y
w : Mono i
⊢ Eq (α := Limits.pullback (mk i).arrow f ⟶ Functor.obj underlying (mk i))
    (pullback.fst (mk i).arrow f ≫ Iso.hom (Iso.refl (Functor.obj underlying (mk i))))
    (CategoryStruct.comp (Y :=
      Functor.obj underlying (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)))
      (Iso.hom (Iso.symm (underlyingIso (pullback.snd (mk i).arrow f))))
      (Iso.hom (underlyingIso (pullback.snd (mk i).arrow f)) ≫ pullback.fst (mk i).arrow f))

Tactic:
simp
-- 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
A : C
i : A ⟶ Y
w : Mono i
⊢ pullback.snd (mk i).arrow f ≫ Iso.hom (Iso.refl X) =
    Iso.hom (Iso.symm (underlyingIso (pullback.snd (mk i).arrow f))) ≫
      (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)).arrow

Tactic:
simp
-- 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
A : C
i : A ⟶ Y
w : Mono i
⊢ (mk i).arrow ≫ Iso.hom (Iso.refl Y) = Iso.hom (Iso.refl (Functor.obj underlying (mk i))) ≫ (mk i).arrow

Tactic:
simp
-- 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
A : C
i : A ⟶ Y
w : Mono i
⊢ f ≫ Iso.hom (Iso.refl Y) = Iso.hom (Iso.refl X) ≫ f

Tactic:
simp
-- 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
A : C
i : A ⟶ Y
w : Mono i
⊢ IsPullback (Iso.hom (underlyingIso (pullback.snd (mk i).arrow f)) ≫ pullback.fst (mk i).arrow f)
    (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)).arrow (mk i).arrow f

Tactic:
exact IsPullback.of_iso (IsPullback.of_hasPullback (mk i).arrow f)
        (underlyingIso (pullback.snd (mk i).arrow f)).symm (Iso.refl _) (Iso.refl _) (Iso.refl _)
        (by simp) (by simp) (by simp) (by simp)

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Limits.pullback.snd, CategoryTheory.Subobject.underlyingIso, CategoryTheory.Iso.refl, CategoryTheory.IsPullback.of_iso, CategoryTheory.Subobject.mk, CategoryTheory.Iso.symm, CategoryTheory.IsPullback.of_hasPullback
-- 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
⊢ IsPullback (pullbackπ f y) ((pullback f).obj y).arrow y.arrow f

Tactic:
(isPullback_aux f y).choose_spec

Premises used: Exists.choose_spec, CategoryTheory.Subobject.isPullback_aux, CategoryTheory.Subobject.pullbackπ
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A X Y : C
i : A ⟶ X
inst_1 : Mono i
f : X ⟶ Y
inst_2 : Mono f
⊢ (map f).obj (mk i) = mk (i ≫ f)

Tactic:
rfl

Premises used: CategoryTheory.Over.mk, CategoryTheory.MonoOver.mk, CategoryTheory.Subobject.mk, Quotient.mk', CategoryTheory.CostructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
x : Subobject.{v₁, u₁} X
h : ∀ (f : MonoOver.{v₁, u₁} X), Functor.obj (map (𝟙 X)) (Quotient.mk'' f) = Quotient.mk'' f
⊢ Functor.obj (map (𝟙 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
f : MonoOver.{v₁, u₁} X
⊢ Functor.obj (map (𝟙 X)) (Quotient.mk'' f) = Quotient.mk'' f

Tactic:
Quotient.sound ⟨(MonoOver.mapId _).app f⟩

Premises used: Quotient.map, Nonempty.intro, CategoryTheory.ThinSkeleton, CategoryTheory.MonoOver.mapId, 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
f : MonoOver.{v₁, u₁} X
⊢ Functor.obj (map (𝟙 X)) (Quotient.mk'' f) = Quotient.mk'' f

Tactic:
exact Quotient.sound ⟨(MonoOver.mapId _).app f⟩
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : Mono f
inst_2 : Mono g
x : Subobject.{v₁, u₁} X
h : ∀ (t : MonoOver.{v₁, u₁} X), (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))
⊢ (map (f ≫ g)).obj x = (map g).obj ((map f).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
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : Mono f
inst_2 : Mono g
t : MonoOver.{v₁, u₁} X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))

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

Premises used: Quotient.map, Nonempty.intro, CategoryTheory.ThinSkeleton, CategoryTheory.MonoOver.mapComp, 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
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : Mono f
inst_2 : Mono g
t : MonoOver.{v₁, u₁} X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))

Tactic:
exact Quotient.sound ⟨(MonoOver.mapComp _ _).app t⟩
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
X₁ X₂ : Subobject.{v₁, u₁} X
h : (map f).obj X₁ = (map f).obj X₂
h₁ : ∀ ⦃A : C⦄ (f_1 : A ⟶ X) [inst_2 : Mono f_1] (h : (map f).obj (mk f_1) = (map f).obj X₂), mk f_1 = X₂
⊢ X₁ = X₂

Tactic:
induction X₁ using Subobject.ind

Premises used: CategoryTheory.Subobject.ind
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
X₂ : Subobject.{v₁, u₁} X
A : C
f_1 : A ⟶ X
inst_2 : Mono f_1
h : (map f).obj (mk f_1) = (map f).obj X₂
h₁ : ∀ ⦃A_1 : C⦄ (f_2 : A_1 ⟶ X) [inst_3 : Mono f_2] (h : (map f).obj (mk f_1) = (map f).obj (mk f_2)), mk f_1 = mk f_2
⊢ mk f_1 = X₂

Tactic:
induction X₂ using Subobject.ind

Premises used: CategoryTheory.Subobject.ind
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
A : C
f_1 : A ⟶ X
inst_2 : Mono f_1
A_1 : C
f_2 : A_1 ⟶ X
inst_3 : Mono f_2
h : mk (f_1 ≫ f) = mk (f_2 ≫ f)
⊢ (isoOfMkEqMk (f_1 ≫ f) (f_2 ≫ f) h).hom ≫ f_2 = f_1

Tactic:
simp [← cancel_mono f]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
A : C
f_1 : A ⟶ X
inst_2 : Mono f_1
A_1 : C
f_2 : A_1 ⟶ X
inst_3 : Mono f_2
h : mk (f_1 ≫ f) = mk (f_2 ≫ f)
⊢ mk f_1 = mk f_2

Tactic:
exact mk_eq_mk_of_comm _ _ (isoOfMkEqMk _ _ h) (by simp [← cancel_mono f])

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.Subobject.isoOfMkEqMk
-- 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
e : X ≅ Y
g : Subobject.{v₁, u₁} X
simp_rw : (map (e.hom ≫ e.inv)).obj g = g
simp_rw₁ : Functor.obj (map (𝟙 X)) g = g
⊢ (map e.inv).obj ((map e.hom).obj g) = g

Tactic:
simp_rw [← map_comp, e.hom_inv_id, map_id]

Premises used: CategoryTheory.Subobject.map_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Subobject.map_id
-- 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
e : X ≅ Y
g : Subobject.{v₁, u₁} Y
simp_rw : (map (e.inv ≫ e.hom)).obj g = g
simp_rw₁ : Functor.obj (map (𝟙 Y)) g = g
⊢ (map e.hom).obj ((map e.inv).obj g) = g

Tactic:
simp_rw [← map_comp, e.inv_hom_id, map_id]

Premises used: CategoryTheory.Subobject.map_comp, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Subobject.map_id
-- 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
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
dsimp : (map e.hom).obj A ≤ (map e.hom).obj B ↔ A ≤ B
⊢ LE.le (α := Subobject.{v₁, u₁} Y)
      (({ toFun := (map e.hom).obj, invFun := (map e.inv).obj, left_inv := ⋯, right_inv := ⋯ :
              Subobject.{v₁, u₁} X ≃ Subobject.{v₁, u₁} Y } :
            (a : Subobject X) → Subobject Y)
          A :
        Subobject.{v₁, u₁} Y)
      (({ toFun := (map e.hom).obj, invFun := (map e.inv).obj, left_inv := ⋯, right_inv := ⋯ :
              Subobject.{v₁, u₁} X ≃ Subobject.{v₁, u₁} Y } :
            (a : Subobject X) → Subobject Y)
          B :
        Subobject.{v₁, u₁} Y) ↔
    A ≤ B

Tactic:
dsimp
-- 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
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
mp : (map e.hom).obj A ≤ (map e.hom).obj B → A ≤ B
mpr : A ≤ B → (map e.hom).obj A ≤ (map e.hom).obj B
⊢ (map e.hom).obj A ≤ (map e.hom).obj B ↔ A ≤ B

Tactic:
constructor
-- 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
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : (map e.hom).obj A ≤ (map e.hom).obj B
mp : ∀ (h : (map e.inv).obj ((map e.hom).obj A) ≤ (map e.inv).obj ((map e.hom).obj B)), A ≤ B
apply_fun : Monotone (map e.inv).obj
⊢ A ≤ B

Tactic:
apply_fun (map e.inv).obj at h

Premises used: CategoryTheory.Subobject.map, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- 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
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : (map e.inv).obj ((map e.hom).obj A) ≤ (map e.inv).obj ((map e.hom).obj B)
⊢ A ≤ B

Tactic:
simpa only [← map_comp, e.hom_inv_id, map_id] using h

Premises used: CategoryTheory.Subobject.map_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Subobject.map_id
-- 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
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : (map e.hom).obj A ≤ (map e.hom).obj B
⊢ Monotone (map e.inv).obj

Tactic:
apply Functor.monotone

Premises used: CategoryTheory.Functor.monotone
-- 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
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : A ≤ B
mpr : ∀ (h : (map e.hom).obj A ≤ (map e.hom).obj B), (map e.hom).obj A ≤ (map e.hom).obj B
apply_fun : Monotone (map e.hom).obj
⊢ (map e.hom).obj A ≤ (map e.hom).obj B

Tactic:
apply_fun (map e.hom).obj at h

Premises used: CategoryTheory.Subobject.map, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- 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
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : (map e.hom).obj A ≤ (map e.hom).obj B
⊢ (map e.hom).obj A ≤ (map e.hom).obj B

Tactic:
h
-- 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
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : (map e.hom).obj A ≤ (map e.hom).obj B
⊢ (map e.hom).obj A ≤ (map e.hom).obj B

Tactic:
exact h
-- 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
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : A ≤ B
⊢ Monotone (map e.hom).obj

Tactic:
apply Functor.monotone

Premises used: CategoryTheory.Functor.monotone
-- 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
inst_2 : Mono f
g : Subobject.{v₁, u₁} X
revert : ∀ (g : Subobject.{v₁, u₁} X), (pullback f).obj ((map f).obj g) = g
⊢ (pullback f).obj ((map f).obj g) = g

Tactic:
revert g
-- 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
inst_2 : Mono f
⊢ ∀ (g : Subobject.{v₁, u₁} X), (pullback f).obj ((map f).obj g) = g

Tactic:
Quotient.ind (fun g' => Quotient.sound ⟨(MonoOver.pullbackMapSelf f).app _⟩)

Premises used: CategoryTheory.MonoOver.pullbackMapSelf, Quotient.ind, Nonempty.intro, CategoryTheory.ThinSkeleton, Quotient.sound, CategoryTheory.Iso.app, CategoryTheory.Subobject
-- 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
inst_2 : Mono f
⊢ ∀ (g : Subobject.{v₁, u₁} X), (pullback f).obj ((map f).obj g) = g

Tactic:
exact Quotient.ind (fun g' => Quotient.sound ⟨(MonoOver.pullbackMapSelf f).app _⟩)
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
p : Subobject.{v₁, u₁} Y
revert : ∀ (p : Subobject.{v₁, u₁} Y), (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)
⊢ (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)

Tactic:
revert p
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
h₁ :
  ∀ (a : MonoOver.{v₁, u₁} Y),
    (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
⊢ ∀ (p : Subobject.{v₁, u₁} Y), (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)

Tactic:
apply Quotient.ind'
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
h₁ : (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ≈ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
⊢ (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
h₁ : (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ⟶ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
h₂ : (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ≈ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)

Tactic:
apply ThinSkeleton.equiv_of_both_ways

Premises used: CategoryTheory.ThinSkeleton.equiv_of_both_ways
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
h₁ :
  pullback.fst (Functor.obj (MonoOver.forget Y) a).hom f ≫
      (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom =
    ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow ≫ k
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ⟶ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)

Tactic:
refine MonoOver.homMk (pullback.lift (pullback.fst _ _) _ ?_) (pullback.lift_snd _ _ _)

Premises used: CategoryTheory.MonoOver.homMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ pullback.fst (Functor.obj (MonoOver.forget Y) a).hom f ≫
      (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom =
    ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow ≫ k

Tactic:
simp [← comm, pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
h₁ :
  Eq (α := ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).obj (P := Over.isMono Z).left ⟶ W)
    ((pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
        (Functor.obj (MonoOver.forget Y) a).hom) ≫
      h)
    (pullback.snd (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫ k)
h₂ :
  pullback.lift (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k)
        (PullbackCone.IsLimit.lift t
          (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫ a.arrow)
          (pullback.snd (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k) ⋯)
        ⋯ ≫
      ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow =
    ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).arrow
⊢ (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)

Tactic:
refine MonoOver.homMk (pullback.lift (pullback.fst _ _)
      (PullbackCone.IsLimit.lift t (pullback.fst _ _ ≫ a.arrow) (pullback.snd _ _) _)
      (PullbackCone.IsLimit.lift_fst _ _ _ ?_).symm) ?_

Premises used: CategoryTheory.MonoOver.homMk
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
h₁ :
  Eq (α := ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).obj (P := Over.isMono Z).left ⟶ W)
    (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
      (Functor.obj (MonoOver.forget Y) a).hom ≫ h)
    (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
      (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom)
⊢ Eq (α := ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).obj (P := Over.isMono Z).left ⟶ W)
    ((pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
        (Functor.obj (MonoOver.forget Y) a).hom) ≫
      h)
    (pullback.snd (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫ k)

Tactic:
rw [← pullback.condition, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ Eq (α := ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).obj (P := Over.isMono Z).left ⟶ W)
    (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
      (Functor.obj (MonoOver.forget Y) a).hom ≫ h)
    (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
      (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
h₁ :
  Eq (α := Limits.pullback (a.arrow ≫ h) k ⟶ Z)
    (CategoryStruct.comp (Y := Limits.pullback a.arrow f)
      (pullback.lift (pullback.fst (a.arrow ≫ h) k)
        (PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯) ⋯)
      (pullback.snd a.obj (P := Over.isMono Y).hom f ≫ g))
    (pullback.snd (a.arrow ≫ h) k)
⊢ pullback.lift (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k)
        (PullbackCone.IsLimit.lift t
          (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫ a.arrow)
          (pullback.snd (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k) ⋯)
        ⋯ ≫
      ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow =
    ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).arrow

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
h₁ :
  Eq (α := Limits.pullback (a.arrow ≫ h) k ⟶ Z)
    (PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯ ≫ g)
    (pullback.snd (a.arrow ≫ h) k)
⊢ Eq (α := Limits.pullback (a.arrow ≫ h) k ⟶ Z)
    (CategoryStruct.comp (Y := Limits.pullback a.arrow f)
      (pullback.lift (pullback.fst (a.arrow ≫ h) k)
        (PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯) ⋯)
      (pullback.snd a.obj (P := Over.isMono Y).hom f ≫ g))
    (pullback.snd (a.arrow ≫ h) k)

Tactic:
rw [pullback.lift_snd_assoc]

Premises used: CategoryTheory.Limits.pullback.lift_snd_assoc
-- Module: Mathlib.CategoryTheory.Subobject.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ Eq (α := Limits.pullback (a.arrow ≫ h) k ⟶ Z)
    (PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯ ≫ g)
    (pullback.snd (a.arrow ≫ h) k)

Tactic:
apply PullbackCone.IsLimit.lift_snd

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd