awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F_1.map snd) (f ≫ g) p
refine_1 : IsPullback fst (F_1.map (⋯.lift (fst ≫ f) snd ⋯) ≫ F_1.map (⋯.snd p)) (f ≫ g) p
refine_2 : fst ≫ f = F_1.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p
⊢ P (⋯.lift (fst ≫ f) snd ⋯ ≫ ⋯.snd p)

Tactic:
refine comp_mem _ _ _ (hf.property (hg.1.fst p) fst _
      (IsPullback.of_bot ?_ ?_ (hg.1.isPullback p))) (hg.property_snd p)

Premises used: CategoryTheory.Functor.relativelyRepresentable.fst, CategoryTheory.MorphismProperty.relative.property_snd, CategoryTheory.MorphismProperty.relative.property, CategoryTheory.Functor.relativelyRepresentable.isPullback, CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.IsPullback.of_bot, And.left
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h refine_1 : IsPullback fst (F_1.map snd) (f ≫ g) p
⊢ IsPullback fst (F_1.map (⋯.lift (fst ≫ f) snd ⋯) ≫ F_1.map (⋯.snd p)) (f ≫ g) p

Tactic:
rw [← Functor.map_comp, lift_snd]

Premises used: CategoryTheory.Functor.relativelyRepresentable.lift_snd, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F_1.map snd) (f ≫ g) p
⊢ IsPullback fst (F_1.map snd) (f ≫ g) p

Tactic:
h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F_1.map snd) (f ≫ g) p
⊢ IsPullback fst (F_1.map snd) (f ≫ g) p

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F_1.map snd) (f ≫ g) p
refine_2 : F_1.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p = fst ≫ f
⊢ fst ≫ f = F_1.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p

Tactic:
symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F_1.map snd) (f ≫ g) p
⊢ F_1.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p = fst ≫ f

Tactic:
apply hg.1.lift_fst

Premises used: CategoryTheory.Functor.relativelyRepresentable.lift_fst, And.left
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : D
P : MorphismProperty.{v₁, u₁} C
⊢ (relative F P).RespectsIso

Tactic:
(relative_isStableUnderBaseChange P).respectsIso

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.IsMultiplicative
inst_5 : P.RespectsIso
X : D
Y : C
g : F.obj Y ⟶ X
⊢ IsPullback g (F.map (𝟙 Y)) (𝟙 X) g

Tactic:
simpa using IsPullback.of_id_snd

Premises used: CategoryTheory.IsPullback.of_id_snd
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
this : ∀ {X : C} {a b : Functor.obj yoneda X ⟶ F}, a ≫ f = b ≫ f → a = b
Z : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
x x_1 : Z ⟶ F
h : x ≫ f = x_1 ≫ f
x_2 : C
x_3 : Functor.obj yoneda x_2 ⟶ Z
⊢ (x_3 ≫ x) ≫ f = (x_3 ≫ x_1) ≫ f

Tactic:
simp only [assoc, h]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
suffices : ∀ {X : C} {a b : Functor.obj yoneda X ⟶ F}, a ≫ f = b ≫ f → a = b
⊢ monomorphisms (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) f

Tactic:
suffices ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b from
    ⟨fun _ _ h ↦ hom_ext_yoneda (fun _ _ ↦ this (by simp only [assoc, h]))⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
X : C
a b : Functor.obj yoneda X ⟶ F
h : a ≫ f = b ≫ f
⊢ a ≫ f = Functor.map yoneda (𝟙 X) ≫ a ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
X : C
a b : Functor.obj yoneda X ⟶ F
h : a ≫ f = b ≫ f
⊢ b ≫ f = Functor.map yoneda (𝟙 X) ≫ a ≫ f

Tactic:
simp [← h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
X : C
a b : Functor.obj yoneda X ⟶ F
h : a ≫ f = b ≫ f
this : ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯
⊢ a = b

Tactic:
simpa using yoneda.congr_map this =≫ (hf.rep.fst (a ≫ f))

Premises used: CategoryTheory.Functor.relativelyRepresentable.fst, CategoryTheory.yoneda, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.congr_map, CategoryTheory.MorphismProperty.relative.rep
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
X : C
a b : Functor.obj yoneda X ⟶ F
h : a ≫ f = b ≫ f
suffices : ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯
⊢ a = b

Tactic:
suffices hf.rep.lift (g := a ≫ f) a (𝟙 X) (by simp) =
      hf.rep.lift b (𝟙 X) (by simp [← h]) by
    simpa using yoneda.congr_map this =≫ (hf.rep.fst (a ≫ f))
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
X : C
a b : Functor.obj yoneda X ⟶ F
h : a ≫ f = b ≫ f
⊢ Mono (⋯.snd (a ≫ f))

Tactic:
have : Mono (hf.rep.snd (a ≫ f)) := hf.property_snd (a ≫ f)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
X : C
a b : Functor.obj yoneda X ⟶ F
h : a ≫ f = b ≫ f
this : Mono (⋯.snd (a ≫ f))
⊢ ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯

Tactic:
simp only [← cancel_mono (hf.rep.snd (a ≫ f)), lift_snd]

Premises used: CategoryTheory.Functor.relativelyRepresentable.lift_snd, CategoryTheory.cancel_mono, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.relativelyRepresentable.snd, CategoryTheory.MorphismProperty.relative.rep
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hP : P ≤ monomorphisms C
X : C
f : Functor.obj yoneda X ⟶ G
hf : P.presheaf f
⊢ Mono f

Tactic:
MorphismProperty.presheaf_monomorphisms_le_monomorphisms _
    (MorphismProperty.relative_monotone hP _ hf)

Premises used: CategoryTheory.MorphismProperty.relative_monotone, CategoryTheory.MorphismProperty.presheaf_monomorphisms_le_monomorphisms
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hP : P ≤ monomorphisms C
X : C
f : Functor.obj yoneda X ⟶ G
hf : P.presheaf f
⊢ Mono f

Tactic:
have := P.presheaf_mono_of_le hP hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hP : P ≤ monomorphisms C
X : C
f : Functor.obj yoneda X ⟶ G
hf : P.presheaf f
this : Mono f
a :
  Eq (α :=
    Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Functor.obj yoneda (⋯.pullback f))
      (Functor.obj yoneda X))
    (Functor.map yoneda (⋯.fst' f)) (Functor.map yoneda (⋯.snd f))
⊢ ⋯.fst' f = ⋯.snd f

Tactic:
apply yoneda.map_injective

Premises used: CategoryTheory.yoneda, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hP : P ≤ monomorphisms C
X : C
f : Functor.obj yoneda X ⟶ G
hf : P.presheaf f
this : Mono f
a : Functor.map yoneda (⋯.fst' f) ≫ f = Functor.map yoneda (⋯.snd f) ≫ f
a₁ a₂ : Functor.map yoneda (⋯.snd f) ≫ f = Functor.map yoneda (⋯.snd f) ≫ f
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Functor.obj yoneda (⋯.pullback f))
      (Functor.obj yoneda X))
    (Functor.map yoneda (⋯.fst' f)) (Functor.map yoneda (⋯.snd f))

Tactic:
rw [← cancel_mono f, (hf.rep.isPullback' f).w]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, CategoryTheory.Functor.relativelyRepresentable.isPullback', CategoryTheory.MorphismProperty.relative.rep
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hP : P ≤ monomorphisms C
X : C
f : Functor.obj yoneda X ⟶ G
hf : P.presheaf f
⊢ IsIso (⋯.fst' f)

Tactic:
have := P.presheaf_mono_of_le hP hf
  have := (hf.rep.isPullback' f).isIso_fst_of_mono
  Yoneda.fullyFaithful.isIso_of_isIso_map _

Premises used: CategoryTheory.Yoneda.fullyFaithful, CategoryTheory.MorphismProperty.presheaf_mono_of_le, CategoryTheory.Functor.relativelyRepresentable.fst', CategoryTheory.IsPullback.isIso_fst_of_mono, CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map, CategoryTheory.Functor.relativelyRepresentable.isPullback', CategoryTheory.MorphismProperty.relative.rep
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ Eq (α := F.obj (hf₁.pullback₃ f₂ f₃) ⟶ X) (F.map (p₁ hf₁ f₂ f₃) ≫ f₁) (π hf₁ f₂ f₃)

Tactic:
rfl

Premises used: CategoryTheory.Functor.relativelyRepresentable.pullback₃.π, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ Eq (α := F.obj (hf₁.pullback₃ f₂ f₃) ⟶ X) (F.map (p₂ hf₁ f₂ f₃) ≫ f₂) (π hf₁ f₂ f₃)

Tactic:
simp [π, p₁, p₂, ← hf₁.w f₂]

Premises used: CategoryTheory.Functor.relativelyRepresentable.w, CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁, CategoryTheory.Functor.relativelyRepresentable.pullback₃.π, CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ Eq (α := F.obj (hf₁.pullback₃ f₂ f₃) ⟶ X) (F.map (p₃ hf₁ f₂ f₃) ≫ f₃) (π hf₁ f₂ f₃)

Tactic:
simp [π, p₁, p₃, ← hf₁.w f₃, pullback.condition]

Premises used: CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃, CategoryTheory.Functor.relativelyRepresentable.w, CategoryTheory.Limits.pullback.condition, CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁, CategoryTheory.Functor.relativelyRepresentable.pullback₃.π
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
x₁ : Z ⟶ A₁
x₂ : Z ⟶ A₂
x₃ : Z ⟶ A₃
h₁₂ : F.map x₁ ≫ f₁ = F.map x₂ ≫ f₂
h₁₃ : F.map x₁ ≫ f₁ = F.map x₃ ≫ f₃
⊢ hf₁.lift' x₁ x₂ h₁₂ ≫ hf₁.fst' f₂ = hf₁.lift' x₁ x₃ h₁₃ ≫ hf₁.fst' f₃

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
x₁ : Z ⟶ A₁
x₂ : Z ⟶ A₂
x₃ : Z ⟶ A₃
h₁₂ : F.map x₁ ≫ f₁ = F.map x₂ ≫ f₂
h₁₃ : F.map x₁ ≫ f₁ = F.map x₃ ≫ f₃
⊢ CategoryStruct.comp (Y := hf₁.pullback₃ f₂ f₃) (hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃) (pullback₃.p₁ hf₁ f₂ f₃) = x₁

Tactic:
simp [lift₃, pullback₃.p₁]

Premises used: CategoryTheory.Functor.relativelyRepresentable.lift₃, CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
x₁ : Z ⟶ A₁
x₂ : Z ⟶ A₂
x₃ : Z ⟶ A₃
h₁₂ : F.map x₁ ≫ f₁ = F.map x₂ ≫ f₂
h₁₃ : F.map x₁ ≫ f₁ = F.map x₃ ≫ f₃
⊢ CategoryStruct.comp (Y := hf₁.pullback₃ f₂ f₃) (hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃) (pullback₃.p₂ hf₁ f₂ f₃) = x₂

Tactic:
simp [lift₃, pullback₃.p₂]

Premises used: CategoryTheory.Functor.relativelyRepresentable.lift₃, CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
x₁ : Z ⟶ A₁
x₂ : Z ⟶ A₂
x₃ : Z ⟶ A₃
h₁₂ : F.map x₁ ≫ f₁ = F.map x₂ ≫ f₂
h₁₃ : F.map x₁ ≫ f₁ = F.map x₃ ≫ f₃
⊢ CategoryStruct.comp (Y := hf₁.pullback₃ f₂ f₃) (hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃) (pullback₃.p₃ hf₁ f₂ f₃) = x₃

Tactic:
simp [lift₃, pullback₃.p₃]

Premises used: CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃, CategoryTheory.Functor.relativelyRepresentable.lift₃
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ Eq (α := Limits.pullback (hf₁.fst' f₂) (hf₁.fst' f₃) ⟶ A₁) (pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) ≫ hf₁.fst' f₂)
    (p₁ hf₁ f₂ f₃)

Tactic:
rfl

Premises used: CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁, CategoryTheory.Functor.relativelyRepresentable.pullback₃, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ Eq (α := Limits.pullback (hf₁.fst' f₂) (hf₁.fst' f₃) ⟶ A₂) (pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) ≫ hf₁.snd f₂)
    (p₂ hf₁ f₂ f₃)

Tactic:
rfl

Premises used: CategoryTheory.Functor.relativelyRepresentable.pullback₃, rfl, CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ Eq (α := Limits.pullback (hf₁.fst' f₂) (hf₁.fst' f₃) ⟶ A₃) (pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃) ≫ hf₁.snd f₃)
    (p₃ hf₁ f₂ f₃)

Tactic:
rfl

Premises used: CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃, CategoryTheory.Functor.relativelyRepresentable.pullback₃, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ Eq (α := Limits.pullback (hf₁.fst' f₂) (hf₁.fst' f₃) ⟶ A₁) (pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃) ≫ hf₁.fst' f₃)
    (p₁ hf₁ f₂ f₃)

Tactic:
pullback.condition.symm

Premises used: CategoryTheory.Limits.pullback.condition, CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁, Eq.symm, CategoryTheory.Functor.relativelyRepresentable.pullback₃
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
h₀ : φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)
h₄ : φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ φ = φ'

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
h₀ :
  (φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₂ =
    (φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₂
h₄ :
  (φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₂ =
    (φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₂
⊢ φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
h₄ :
  (φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₃ =
    (φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₃
h₅ :
  (φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₃ =
    (φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₃
⊢ φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ (φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₂ =
    (φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₂

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ (φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₂ =
    (φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₂

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ (φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₃ =
    (φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₃

Tactic:
simpa