awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
inst_2 : P.IsStableUnderComposition
inst_3 : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst_4 : P.HasPushoutsAlong f
inst_5 : P.IsStableUnderCobaseChangeAlong f
inst_6 : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ CategoryStruct.comp (Y :=
      Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (pushout.inl (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f :
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
            (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (CommaMorphism.right
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
            (Functor.map (map (P := P) Q hPf ⋙ pushout P Q f) g ≫
              Under.homMk (P := P) (Q := Q)
                (pushout.desc
                  (𝟙
                    (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                      (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := ⊤) (W := Q).right))
                  B.toComma (P := P) (Q := ⊤) (W := Q).hom ⋯)
                ⋯ ⋯)) :
        (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          (Functor.obj (𝟭 (P.Under Q Y)) B).toComma (P := P) (Q := ⊤) (W := Q).right) =
    CategoryStruct.comp (Y :=
      Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (pushout.inl (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f :
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
            (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (CommaMorphism.right
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
            (Under.homMk (P := P) (Q := Q)
                (pushout.desc
                  (𝟙
                    (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                      (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).right))
                  A.toComma (P := P) (Q := ⊤) (W := Q).hom ⋯)
                ⋯ ⋯ ≫
              Functor.map (𝟭 (P.Under Q Y)) g)) :
        (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          (Functor.obj (𝟭 (P.Under Q Y)) B).toComma (P := P) (Q := ⊤) (W := Q).right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
inst_2 : P.IsStableUnderComposition
inst_3 : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst_4 : P.HasPushoutsAlong f
inst_5 : P.IsStableUnderCobaseChangeAlong f
inst_6 : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ CategoryStruct.comp (Y :=
      Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (pushout.inr (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f :
        Y ⟶ Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (CommaMorphism.right
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
            (Functor.map (map (P := P) Q hPf ⋙ pushout P Q f) g ≫
              Under.homMk (P := P) (Q := Q)
                (pushout.desc
                  (𝟙
                    (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                      (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := ⊤) (W := Q).right))
                  B.toComma (P := P) (Q := ⊤) (W := Q).hom ⋯)
                ⋯ ⋯)) :
        (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          (Functor.obj (𝟭 (P.Under Q Y)) B).toComma (P := P) (Q := ⊤) (W := Q).right) =
    CategoryStruct.comp (Y :=
      Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (pushout.inr (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f :
        Y ⟶ Limits.pushout (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (CommaMorphism.right
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
            (Under.homMk (P := P) (Q := Q)
                (pushout.desc
                  (𝟙
                    (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
                      (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).right))
                  A.toComma (P := P) (Q := ⊤) (W := Q).hom ⋯)
                ⋯ ⋯ ≫
              Functor.map (𝟭 (P.Under Q Y)) g)) :
        (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
          (Functor.obj (𝟭 (P.Under Q Y)) B).toComma (P := P) (Q := ⊤) (W := Q).right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
X Y Z : T
inst_2 : P.IsStableUnderComposition
inst_3 : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst_4 : P.HasPushoutsAlong f
inst_5 : P.IsStableUnderCobaseChangeAlong f
hPf : P f
⊢ Functor.IsRightAdjoint (C := P.Under ⊤ X) (Under.map (P := P) ⊤ hPf)

Tactic:
(Under.mapPushoutAdj P ⊤ f hPf trivial).isRightAdjoint

Premises used: CategoryTheory.MorphismProperty.Under.mapPushoutAdj, trivial, CategoryTheory.Adjunction.isRightAdjoint, Top.top
-- Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X Y : T
inst_1 : P.IsStableUnderComposition
f : X ⟶ Y
inst_2 : P.HasPushoutsAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong f
hPf : P f
⊢ Functor.IsLeftAdjoint (C := P.Under ⊤ X) (Under.pushout P ⊤ f)

Tactic:
(Under.mapPushoutAdj P ⊤ f hPf trivial).isLeftAdjoint

Premises used: CategoryTheory.MorphismProperty.Under.mapPushoutAdj, trivial, CategoryTheory.Adjunction.isLeftAdjoint, Top.top
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f g x y : X ⟶ Y
h : homRel x y
⊢ W x ↔ W y

Tactic:
iff W h

Premises used: CategoryTheory.MorphismProperty.HasQuotient.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f g x y : X ⟶ Y
h : homRel x y
⊢ W x ↔ W y

Tactic:
exact iff W h

Premises used: CategoryTheory.MorphismProperty.HasQuotient.iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f g x : X ⟶ Y
⊢ W x ↔ W x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f g x y : X ⟶ Y
h_1 : Relation.EqvGen homRel x y
h : W x ↔ W y
⊢ W y ↔ W x

Tactic:
h.symm

Premises used: Iff.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f g x y : X ⟶ Y
h_1 : Relation.EqvGen homRel x y
h : W x ↔ W y
⊢ W y ↔ W x

Tactic:
exact h.symm

Premises used: Iff.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f g x y z : X ⟶ Y
h : Relation.EqvGen homRel x y
h_1 : Relation.EqvGen homRel y z
h₁ : W x ↔ W y
h₂ : W y ↔ W z
⊢ W x ↔ W z

Tactic:
h₁.trans h₂

Premises used: Iff.trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f g x y z : X ⟶ Y
h : Relation.EqvGen homRel x y
h_1 : Relation.EqvGen homRel y z
h₁ : W x ↔ W y
h₂ : W y ↔ W z
⊢ W x ↔ W z

Tactic:
exact h₁.trans h₂

Premises used: Iff.trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f g : X ⟶ Y
h : Relation.EqvGen homRel f g
rel : ∀ (x y : X ⟶ Y) (h : homRel x y), W x ↔ W y
refl : ∀ (x : X ⟶ Y), W x ↔ W x
symm : ∀ (x y : X ⟶ Y), Relation.EqvGen homRel x y → ∀ (h : W x ↔ W y), W y ↔ W x
trans :
  ∀ (x y z : X ⟶ Y),
    Relation.EqvGen homRel x y → Relation.EqvGen homRel y z → ∀ (h₁ : W x ↔ W y) (h₂ : W y ↔ W z), W x ↔ W z
⊢ W f ↔ W g

Tactic:
induction h with
  | rel _ _ h => exact iff W h
  | refl => rfl
  | symm _ _ _ h => exact h.symm
  | trans _ _ _ _ _ h₁ h₂ => exact h₁.trans h₂

Premises used: CategoryTheory.MorphismProperty.HasQuotient.iff, symm, Relation.EqvGen.symm, refl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
⊢ W.quotient homRel ((Quotient.functor homRel).map f) ↔ W f

Tactic:
⟨fun ⟨f', hf', h⟩ ↦ ?_, fun hf ↦ ⟨f, hf, rfl⟩⟩

Premises used: _private.0.CategoryTheory.MorphismProperty.quotient_iff.match_1, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
refine :
  W.quotient homRel ((Quotient.functor homRel).map f) →
    ∀
      (f' :
        Quiver.Hom.{v_1, u_1} (V := C) (Quotient.as (r := homRel) ((Quotient.functor homRel).1 X))
          (Quotient.as (r := homRel) ((Quotient.functor homRel).1 Y)))
      (hf' : W f') (h : (Quotient.functor homRel).map f = (Quotient.functor homRel).map f'), W f
⊢ W.quotient homRel ((Quotient.functor homRel).map f) ↔ W f

Tactic:
refine ⟨fun ⟨f', hf', h⟩ ↦ ?_, fun hf ↦ ⟨f, hf, rfl⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
h_1 : W.quotient homRel ((Quotient.functor homRel).map f)
f' :
  Quiver.Hom.{v_1, u_1} (V := C) (Quotient.as (r := homRel) ((Quotient.functor homRel).1 X))
    (Quotient.as (r := homRel) ((Quotient.functor homRel).1 Y))
hf' : W f'
h : (Quotient.functor homRel).map f = (Quotient.functor homRel).map f'
⊢ Relation.EqvGen homRel f f'

Tactic:
rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self homRel] at h

Premises used: CategoryTheory.Functor.homRel_iff, CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen, CategoryTheory.HomRel.compClosure_eq_self
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
h_1 : W.quotient homRel ((Quotient.functor homRel).map f)
f' :
  Quiver.Hom.{v_1, u_1} (V := C) (Quotient.as (r := homRel) ((Quotient.functor homRel).1 X))
    (Quotient.as (r := homRel) ((Quotient.functor homRel).1 Y))
hf' : W f'
h : Relation.EqvGen homRel f f'
rwa rwa₁ rwa₂ rwa₃ : W f'
⊢ W f

Tactic:
rwa [HasQuotient.iff_of_eqvGen W h]

Premises used: CategoryTheory.MorphismProperty.HasQuotient.iff_of_eqvGen
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ (W.quotient homRel).inverseImage (Quotient.functor homRel) f
⊢ W = (W.quotient homRel).inverseImage (Quotient.functor homRel)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
⊢ W f ↔ (W.quotient homRel).inverseImage (Quotient.functor homRel) f

Tactic:
(quotient_iff _ _ _).symm

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.MorphismProperty.quotient, Iff.symm, CategoryTheory.MorphismProperty.quotient_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
⊢ W f ↔ (W.quotient homRel).inverseImage (Quotient.functor homRel) f

Tactic:
exact (quotient_iff _ _ _).symm

Premises used: Iff.symm, CategoryTheory.MorphismProperty.quotient_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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
inst_2 : F.Full
⊢ F.map (hf'.fst' g) = hf'.fst g

Tactic:
F.map_preimage _

Premises used: CategoryTheory.Functor.map_preimage
-- 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
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
⊢ IsPullback (hf.fst g) (F.map (hf.snd g)) f g

Tactic:
(hf g).choose_spec.choose_spec.choose_spec

Premises used: Exists.choose_spec, 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
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
⊢ hf.fst g ≫ f = F.map (hf.snd g) ≫ g

Tactic:
(hf.isPullback g).w

Premises used: CategoryTheory.Functor.relativelyRepresentable.isPullback, 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 : Functor.{v₁, v₂, u₁, u₂} C D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
inst_2 : F.Full
⊢ IsPullback (F.map (hf'.fst' g)) (F.map (hf'.snd g)) f' g

Tactic:
(hf'.map_fst' _) ▸ hf'.isPullback g

Premises used: Eq.rec, CategoryTheory.Functor.relativelyRepresentable.map_fst', CategoryTheory.Functor.relativelyRepresentable.isPullback, Eq.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 : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Z
hf : F.relativelyRepresentable (F.map f)
g : Y ⟶ Z
inst_2 : F.Full
inst_3 : F.Faithful
⊢ F.map (hf.fst' (F.map g) ≫ f) = F.map (hf.snd (F.map g) ≫ g)

Tactic:
simp [(hf.w (F.map g))]

Premises used: CategoryTheory.Functor.map, 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 Z : C
f : X ⟶ Z
hf : F.relativelyRepresentable (F.map f)
g : Y ⟶ Z
inst_2 : F.Full
inst_3 : F.Faithful
⊢ IsPullback (hf.fst' (F.map g)) (hf.snd (F.map g)) f g

Tactic:
IsPullback.of_map F (hf.w' g) (hf.isPullback' (F.map g))

Premises used: CategoryTheory.IsPullback.of_map, CategoryTheory.Functor.map, CategoryTheory.Functor.relativelyRepresentable.w', CategoryTheory.Functor.relativelyRepresentable.isPullback'
-- 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
hf : F.relativelyRepresentable f
a_1 : C
g : F.obj a_1 ⟶ Y
inst_2 : F.Faithful
c : C
a b : c ⟶ hf.pullback g
h₁ : F.map a ≫ hf.fst g = F.map b ≫ hf.fst g
h₂ : a ≫ hf.snd g = b ≫ hf.snd g
⊢ F.map a ≫ ⋯.cone.snd = F.map b ≫ ⋯.cone.snd

Tactic:
simpa using F.congr_map h₂

Premises used: CategoryTheory.Functor.congr_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
Y : D
b_1 : C
f' : F.obj b_1 ⟶ Y
hf' : F.relativelyRepresentable f'
a_1 : C
g : F.obj a_1 ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
c : C
a b : c ⟶ hf'.pullback g
h₁ : a ≫ hf'.fst' g = b ≫ hf'.fst' g
h₂ : a ≫ hf'.snd g = b ≫ hf'.snd g
⊢ F.map a ≫ hf'.fst g = F.map b ≫ hf'.fst g

Tactic:
simpa [map_fst'] using F.congr_map h₁

Premises used: CategoryTheory.Functor.relativelyRepresentable.map_fst', CategoryTheory.Functor.congr_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
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
c : C
i : F.obj c ⟶ X
h : c ⟶ a
hi : i ≫ f = F.map h ≫ g
inst_2 : F.Full
⊢ F.map (hf.lift i h hi) ≫ hf.fst g = i

Tactic:
simpa [lift] using PullbackCone.IsLimit.lift_fst _ _ _ _

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst, 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
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
c : C
i : F.obj c ⟶ X
h : c ⟶ a
hi : i ≫ f = F.map h ≫ g
inst_2 : F.Full
inst_3 : F.Faithful
⊢ F.map (hf.lift i h hi ≫ hf.snd g) = F.map h

Tactic:
simpa [lift] using PullbackCone.IsLimit.lift_snd _ _ _ _

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd, 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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
c : C
i : c ⟶ b
h : c ⟶ a
hi : F.map i ≫ f' = F.map h ≫ g
inst_2 : F.Full
inst_3 : F.Faithful
⊢ F.map (hf'.lift' i h hi ≫ hf'.fst' g) = F.map i

Tactic:
simp [lift']

Premises used: 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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
c : C
i : c ⟶ b
h : c ⟶ a
hi : F.map i ≫ f' = F.map h ≫ g
inst_2 : F.Full
inst_3 : F.Faithful
⊢ hf'.lift' i h hi ≫ hf'.snd g = h

Tactic:
simp [lift']

Premises used: 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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst_2 : F.Full
inst_3 : F.Faithful
⊢ hf'.symmetry hg ≫ hg.fst' f' = hf'.snd g

Tactic:
simp [symmetry]

Premises used: CategoryTheory.Functor.relativelyRepresentable.symmetry
-- 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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst_2 : F.Full
inst_3 : F.Faithful
⊢ hf'.symmetry hg ≫ hg.snd f' = hf'.fst' g

Tactic:
simp [symmetry]

Premises used: CategoryTheory.Functor.relativelyRepresentable.symmetry
-- 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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst_2 : F.Full
inst_3 : F.Faithful
⊢ (hf'.symmetry hg ≫ hg.symmetry hf') ≫ hf'.fst' g = 𝟙 (hf'.pullback g) ≫ hf'.fst' 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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst_2 : F.Full
inst_3 : F.Faithful
⊢ (hf'.symmetry hg ≫ hg.symmetry hf') ≫ hf'.snd g = 𝟙 (hf'.pullback g) ≫ hf'.snd 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
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst_2 : F.Full
inst_3 : F.Faithful
⊢ IsIso (hf'.symmetry hg)

Tactic:
(hf'.symmetryIso hg).isIso_hom

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Functor.relativelyRepresentable.lift', CategoryTheory.Functor.relativelyRepresentable.symmetryIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.Functor.relativelyRepresentable.lift, Classical.choose, CategoryTheory.Functor.relativelyRepresentable.symmetry
-- 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 : F.obj c ⟶ F.obj b
obtain :
  ∀ (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)
⊢ ∃ (b_1 : C) (snd : b_1 ⟶ c) (fst : F.obj b_1 ⟶ F.obj a), IsPullback fst (F.map snd) (F.map f) g

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

Premises used: rfl, CategoryTheory.Functor.map_surjective