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 : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : HasPullbacks.{v₁, u₁} C
a b : C
f : a ⟶ b
inst_4 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : c ⟶ b
⊢ ∃ (b_1 : C) (snd : b_1 ⟶ c) (fst : F.obj b_1 ⟶ F.obj a), IsPullback fst (F.map snd) (F.map f) (F.map g)

Tactic:
⟨Limits.pullback f g, Limits.pullback.snd f g, F.map (Limits.pullback.fst f g), ?_⟩

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Limits.pullback.snd, CategoryTheory.Functor.map, CategoryTheory.Limits.pullback.fst, Exists.intro
-- 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
inst_3 : HasPullbacks.{v₁, u₁} C
a b : C
f : a ⟶ b
inst_4 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : c ⟶ b
refine :
  IsPullback (P := F.obj (Limits.pullback f g)) (F.map (pullback.fst f g)) (F.map (pullback.snd f g)) (F.map f)
    (F.map g)
⊢ ∃ (b_1 : C) (snd : b_1 ⟶ c) (fst : F.obj b_1 ⟶ F.obj a), IsPullback fst (F.map snd) (F.map f) (F.map g)

Tactic:
refine ⟨Limits.pullback f g, Limits.pullback.snd f g, F.map (Limits.pullback.fst f g), ?_⟩
-- 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
inst_3 : HasPullbacks.{v₁, u₁} C
a b : C
f : a ⟶ b
inst_4 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : c ⟶ b
⊢ IsPullback (P := F.obj (Limits.pullback f g)) (F.map (pullback.fst f g)) (F.map (pullback.snd f g)) (F.map f)
    (F.map g)

Tactic:
apply F.map_isPullback <| IsPullback.of_hasPullback f g

Premises used: CategoryTheory.Functor.map_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- 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
f : X ⟶ Y
inst_2 : IsIso f
a : C
g : F.obj a ⟶ Y
⊢ (g ≫ CategoryTheory.inv f) ≫ f = F.map (𝟙 a) ≫ g

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
⊢ isomorphisms D ≤ F.relativelyRepresentable

Tactic:
fun _ _ f hf ↦ letI : IsIso f := hf; of_isIso F f

Premises used: CategoryTheory.Functor.relativelyRepresentable.of_isIso
-- 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
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : F_1.relativelyRepresentable f
hg : F_1.relativelyRepresentable g
X : C
h : F_1.obj X ⟶ H
⊢ IsPullback (hf.fst (hg.fst h)) (F_1.map (hf.snd (hg.fst h) ≫ hg.snd h)) (f ≫ g) h

Tactic:
simpa using IsPullback.paste_vert (hf.isPullback (hg.fst h)) (hg.isPullback h)

Premises used: CategoryTheory.Functor.relativelyRepresentable.fst, CategoryTheory.Functor.relativelyRepresentable.isPullback, CategoryTheory.IsPullback.paste_vert
-- 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 Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ Y'), IsPullback fst (F.map snd) g' h

Tactic:
⟨hg.pullback (h ≫ f), hg.snd (h ≫ f), ?_, ?_⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.relativelyRepresentable.pullback, CategoryTheory.Functor.relativelyRepresentable.snd
-- 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 Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
refine_1 : F.obj (hg.pullback (h ≫ f)) ⟶ Y'
refine_2 : IsPullback (P₁.lift (hg.fst (h ≫ f)) (F.map (hg.snd (h ≫ f)) ≫ h) ⋯) (F.map (hg.snd (h ≫ f))) g' h
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ Y'), IsPullback fst (F.map snd) g' h

Tactic:
refine ⟨hg.pullback (h ≫ f), hg.snd (h ≫ f), ?_, ?_⟩
-- 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 Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ hg.fst (h ≫ f) ≫ g = (F.map (hg.snd (h ≫ f)) ≫ h) ≫ f

Tactic:
simpa using hg.w (h ≫ f)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.relativelyRepresentable.w
-- 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 Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ F.obj (hg.pullback (h ≫ f)) ⟶ Y'

Tactic:
apply P₁.lift (hg.fst (h ≫ f)) (F.map (hg.snd (h ≫ f)) ≫ h) (by simpa using hg.w (h ≫ f))

Premises used: CategoryTheory.Functor.relativelyRepresentable.fst, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.relativelyRepresentable.snd, CategoryTheory.IsPullback.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
X Y Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ IsPullback (P₁.lift (hg.fst (h ≫ f)) (F.map (hg.snd (h ≫ f)) ≫ h) ⋯) (F.map (hg.snd (h ≫ f))) g' h

Tactic:
apply IsPullback.of_right' (hg.isPullback (h ≫ f)) P₁

Premises used: CategoryTheory.IsPullback.of_right', CategoryTheory.Functor.relativelyRepresentable.isPullback, CategoryTheory.CategoryStruct.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 : Functor.{v₁, v₂, u₁, u₂} C D
⊢ F.relativelyRepresentable.RespectsIso

Tactic:
(isStableUnderBaseChange F).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 Y : D
P : MorphismProperty.{v₁, u₁} C
f : X ⟶ Y
hf : relative F P f
⊢ F.relativelyRepresentable f

Tactic:
hf.1

Premises used: 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
f : X ⟶ Y
hf : relative F P f
⊢ ∀ ⦃a b : C⦄ (g : F.obj a ⟶ Y) (fst : F.obj b ⟶ X) (snd : b ⟶ a), IsPullback fst (F.map snd) f g → P snd

Tactic:
hf.2

Premises used: And.right
-- 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
f : X ⟶ Y
hf : relative F P f
a : C
g : F.obj a ⟶ Y
⊢ P (⋯.snd g)

Tactic:
hf.property g _ _ (hf.rep.isPullback g)

Premises used: CategoryTheory.MorphismProperty.relative.property, 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
X Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
⊢ relative F P f

Tactic:
⟨fun a g ↦ ?_, fun a b g fst snd h ↦ ?_⟩

Premises used: CategoryTheory.MorphismProperty.relative, And.intro
-- 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
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
refine_1 : ∀ (a : C) (g : F.obj a ⟶ Y), ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) f g
refine_2 : ∀ (a b : C) (g : F.obj a ⟶ Y) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (h : IsPullback fst (F.map snd) f g), P snd
⊢ relative F P f

Tactic:
refine ⟨fun a g ↦ ?_, fun a b g fst snd 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 : Functor.{v₁, v₂, u₁, u₂} C D
X Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a : C
g : F.obj a ⟶ Y
refine_1 :
  ∀ (c : C) (g_fst : F.obj c ⟶ X) (g_snd : c ⟶ a) (BC : IsPullback g_fst (F.map g_snd) f g) (H : P g_snd),
    ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) f g
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) f g

Tactic:
obtain ⟨c, g_fst, g_snd, BC, H⟩ := h₀ g
-- 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
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
refine_2 :
  ∀ (c : C) (g_fst : F.obj c ⟶ X) (g_snd : c ⟶ a) (BC : IsPullback g_fst (F.map g_snd) f g) (H : P g_snd), P snd
⊢ P snd

Tactic:
obtain ⟨c, g_fst, g_snd, BC, H⟩ := h₀ g
-- 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
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a : C
g : F.obj a ⟶ Y
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) f g

Tactic:
⟨c, g_snd, g_fst, BC⟩

Premises used: Exists.intro
-- 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
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a : C
g : F.obj a ⟶ Y
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) f g

Tactic:
refine ⟨c, g_snd, g_fst, BC⟩
-- 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
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ P snd

Tactic:
(P.arrow_mk_iso_iff ?_).2 H

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- 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
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
refine_2 : Arrow.mk snd ≅ Arrow.mk g_snd
⊢ P snd

Tactic:
refine (P.arrow_mk_iso_iff ?_).2 H

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- 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
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ F.map ((F.preimageIso (IsPullback.isoIsPullback X (F.obj a) h BC)).hom ≫ (Arrow.mk g_snd).hom) =
    F.map ((Arrow.mk snd).hom ≫ Iso.hom (Iso.refl (Arrow.mk snd).right))

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
X Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ Arrow.mk snd ≅ Arrow.mk g_snd

Tactic:
exact Arrow.isoMk (F.preimageIso (h.isoIsPullback X (F.obj a) BC)) (Iso.refl _)
      (F.map_injective (by simp))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.preimageIso, CategoryTheory.Functor.map_injective, CategoryTheory.Arrow.isoMk
-- 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
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
hf : F.relativelyRepresentable f
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), P (hf.snd g)
⊢ relative F P f

Tactic:
relative.of_exists (fun _ g ↦ ⟨hf.pullback g, hf.fst g, hf.snd g, hf.isPullback g, h g⟩)

Premises used: CategoryTheory.Functor.relativelyRepresentable.fst, CategoryTheory.Functor.relativelyRepresentable.isPullback, Exists.intro, CategoryTheory.Functor.relativelyRepresentable.pullback, CategoryTheory.Functor.relativelyRepresentable.snd, CategoryTheory.MorphismProperty.relative.of_exists
-- 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
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : HasPullbacks.{v₁, u₁} C
inst_5 : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst_6 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
h₀ :
  ∀ ⦃a_1 : C⦄ (g : F.obj a_1 ⟶ F.obj b),
    ∃ (b_1 : C) (fst : F.obj b_1 ⟶ F.obj a) (snd : b_1 ⟶ a_1) (_ : IsPullback fst (F.map snd) (F.map f) g), P snd
⊢ relative F P (F.map f)

Tactic:
apply relative.of_exists

Premises used: CategoryTheory.MorphismProperty.relative.of_exists
-- 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
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : HasPullbacks.{v₁, u₁} C
inst_5 : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst_6 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
Y' : C
g : F.obj Y' ⟶ F.obj b
h₀ :
  ∀ (g : Y' ⟶ b),
    ∃ (b_1 : C) (fst : F.obj b_1 ⟶ F.obj a) (snd : b_1 ⟶ Y') (_ : IsPullback fst (F.map snd) (F.map f) (F.map g)), P snd
⊢ ∃ (b_1 : C) (fst : F.obj b_1 ⟶ F.obj a) (snd : b_1 ⟶ Y') (_ : IsPullback fst (F.map snd) (F.map f) g), P snd

Tactic:
obtain ⟨g, rfl⟩ := F.map_surjective g

Premises used: rfl, CategoryTheory.Functor.map_surjective
-- 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
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : HasPullbacks.{v₁, u₁} C
inst_5 : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst_6 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
Y' : C
g : Y' ⟶ b
⊢ ∃ (b_1 : C) (fst : F.obj b_1 ⟶ F.obj a) (snd : b_1 ⟶ Y') (_ : IsPullback fst (F.map snd) (F.map f) (F.map g)), P snd

Tactic:
⟨_, _, _, (IsPullback.of_hasPullback f g).map F, P.pullback_snd _ _ hf⟩

Premises used: Exists.intro, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.MorphismProperty.pullback_snd, CategoryTheory.IsPullback.map
-- 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
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : HasPullbacks.{v₁, u₁} C
inst_5 : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst_6 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
Y' : C
g : Y' ⟶ b
⊢ ∃ (b_1 : C) (fst : F.obj b_1 ⟶ F.obj a) (snd : b_1 ⟶ Y') (_ : IsPullback fst (F.map snd) (F.map f) (F.map g)), P snd

Tactic:
exact ⟨_, _, _, (IsPullback.of_hasPullback f g).map F, P.pullback_snd _ _ hf⟩
-- 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
P : MorphismProperty.{v₁, u₁} C
a b : C
f : a ⟶ b
hf : relative F P (F.map f)
⊢ P f

Tactic:
hf.property (𝟙 _) (𝟙 _) f (IsPullback.id_horiz (F.map f))

Premises used: CategoryTheory.IsPullback.id_horiz, CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.relative.property, CategoryTheory.Functor.map
-- 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
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : PreservesLimitsOfShape WalkingCospan F
inst_5 : HasPullbacks.{v₁, u₁} C
inst_6 : P.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
⊢ relative F P (F.map f) ↔ P f

Tactic:
⟨fun hf ↦ of_relative_map hf, fun hf ↦ relative_map hf⟩

Premises used: CategoryTheory.MorphismProperty.relative_map, Iff.intro, CategoryTheory.MorphismProperty.of_relative_map
-- 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
P P' : MorphismProperty.{v₁, u₁} C
h : P ≤ P'
⊢ relative F P ≤ relative F P'

Tactic:
fun _ _ _ hf ↦
  ⟨hf.rep, fun _ _ g fst snd BC ↦ h _ (hf.property g fst snd BC)⟩

Premises used: CategoryTheory.MorphismProperty.relative.property, CategoryTheory.MorphismProperty.relative, And.intro, 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_1 : Functor.{v₁, v₂, u₁, u₂} C D
X 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
⊢ relative F_1 P (f ≫ g)

Tactic:
⟨comp_mem _ _ _ hf.1 hg.1, fun Z X p fst snd h ↦ ?_⟩

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.relative, And.left, And.intro
-- 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 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
refine :
  ∀ (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),
    P snd
⊢ relative F_1 P (f ≫ g)

Tactic:
refine ⟨comp_mem _ _ _ hf.1 hg.1, fun Z X p fst snd 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
⊢ (fst ≫ f) ≫ g = F_1.map snd ≫ p

Tactic:
simpa using h.w

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- 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
rw : P (⋯.lift (fst ≫ f) snd ⋯ ≫ ⋯.snd p)
⊢ P snd

Tactic:
rw [← hg.1.lift_snd (fst ≫ f) snd (by simpa using h.w)]

Premises used: CategoryTheory.Functor.relativelyRepresentable.lift_snd, And.left, CategoryTheory.CategoryStruct.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
⊢ P (⋯.lift (fst ≫ f) snd ⋯ ≫ ⋯.snd p)

Tactic:
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