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
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : P.IsStableUnderBaseChangeAlong f
inst_3 : P.IsStableUnderBaseChangeAlong g
inst_4 : P.HasPullbacksAlong f
inst_5 : P.HasPullbacksAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderBaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pullbackComp._auto_1
this : P.HasPullbacksAlong fg
subst : ∀ (this : P.HasPullbacksAlong (f ≫ g)), P.IsStableUnderBaseChangeAlong (f ≫ g)
⊢ P.IsStableUnderBaseChangeAlong fg

Tactic:
subst hfg
-- 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
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : P.IsStableUnderBaseChangeAlong f
inst_3 : P.IsStableUnderBaseChangeAlong g
inst_4 : P.HasPullbacksAlong f
inst_5 : P.HasPullbacksAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderBaseChange
this : P.HasPullbacksAlong (f ≫ g)
⊢ P.IsStableUnderBaseChangeAlong (f ≫ g)

Tactic:
infer_instance
-- 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
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : P.IsStableUnderBaseChangeAlong f
inst_3 : P.IsStableUnderBaseChangeAlong g
inst_4 : P.HasPullbacksAlong f
inst_5 : P.HasPullbacksAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderBaseChange
fg : X ⟶ Z
hfg : fg = f ≫ g
subst : P.HasPullbacksAlong (f ≫ g)
⊢ P.HasPullbacksAlong fg

Tactic:
subst hfg
-- 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_1 Y Z : T
f : X_1 ⟶ Y
g : Y ⟶ Z
inst_2 : P.IsStableUnderBaseChangeAlong f
inst_3 : P.IsStableUnderBaseChangeAlong g
inst_4 : P.HasPullbacksAlong f
inst_5 : P.HasPullbacksAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderBaseChange
fg : X_1 ⟶ Z
hfg : fg = f ≫ g
this_1 : P.HasPullbacksAlong fg
X : P.Over Q Z
this : HasPullback X.toComma (P := P) (Q := Q) (W := ⊤).hom fg
⊢ Iso.hom
        (pullback.congrHom ⋯ hfg ≪≫
          Iso.symm (pullbackLeftPullbackSndIso X.toComma (P := P) (Q := Q) (W := ⊤).hom g f)) ≫
      (Functor.obj (pullback P Q g ⋙ pullback P Q f) X).toComma (P := P) (Q := Q) (W := ⊤).hom =
    (Functor.obj (pullback P Q fg) X).toComma (P := P) (Q := Q) (W := ⊤).hom

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
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : P.IsStableUnderBaseChangeAlong f
inst_3 : P.IsStableUnderBaseChangeAlong g
inst_4 : P.HasPullbacksAlong f
inst_5 : P.HasPullbacksAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderBaseChange
A : P.Over Q Z
⊢ Eq (α :=
    (Functor.obj (pullback P Q (f ≫ g)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := Q) (W := ⊤).left)
    (CategoryStruct.comp (Y :=
        (Functor.obj (pullback P Q g ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left)
        (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
            (NatTrans.app (Iso.hom (pullbackComp (P := P) (Q := Q) f g (f ≫ g) ⋯)) A)))
        (pullback.fst (pullback.snd A.toComma (P := P) (Q := Q) (W := ⊤).hom g) f ≫
          pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom g) :
      (Functor.obj (pullback P Q (f ≫ g)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := Q) (W := ⊤).left)
    (pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom (f ≫ g) :
      Limits.pullback A.toComma (P := P) (Q := Q) (W := ⊤).hom (f ≫ g) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := Q) (W := ⊤).left)

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
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
g : X ⟶ Y
h : f = g
subst : P.HasPullbacksAlong f
⊢ P.HasPullbacksAlong g

Tactic:
subst h
-- 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
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
⊢ P.HasPullbacksAlong f

Tactic:
infer_instance
-- 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
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
g : X ⟶ Y
h : f = g
this : P.HasPullbacksAlong g
subst : ∀ (this : P.HasPullbacksAlong f), P.IsStableUnderBaseChangeAlong f
⊢ P.IsStableUnderBaseChangeAlong g

Tactic:
subst h
-- 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
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
this : P.HasPullbacksAlong f
⊢ P.IsStableUnderBaseChangeAlong f

Tactic:
infer_instance
-- 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
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
g : X ⟶ Y
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
h : f = g
A : P.Over Q Y
subst : P.HasPullbacksAlong f
⊢ P.HasPullbacksAlong g

Tactic:
subst h
-- 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
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
A : P.Over Q Y
⊢ P.HasPullbacksAlong f

Tactic:
infer_instance
-- 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 : T
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
g : X ⟶ Y
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
h : f = g
A : P.Over Q Y
subst :
  Eq (α :=
    (Functor.obj (pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := Q) (W := ⊤).left)
    (CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
          (NatTrans.app (Iso.hom (pullbackCongr (P := P) (Q := Q) ⋯)) A)) ≫
      pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f)
    (pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f)
⊢ Eq (α :=
    (Functor.obj (pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := Q) (W := ⊤).left)
    (CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
          (NatTrans.app (Iso.hom (pullbackCongr (P := P) (Q := Q) h)) A)) ≫
      pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom g)
    (pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f)

Tactic:
subst h
-- 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 : T
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : Q.IsStableUnderBaseChange
A : P.Over Q Y
⊢ Eq (α :=
    (Functor.obj (pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := Q) (W := ⊤).left)
    (CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
          (NatTrans.app (Iso.hom (pullbackCongr (P := P) (Q := Q) ⋯)) A)) ≫
      pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f)
    (pullback.fst A.toComma (P := P) (Q := Q) (W := ⊤).hom f)

Tactic:
simp [pullbackCongr]

Premises used: CategoryTheory.MorphismProperty.Over.pullbackCongr
-- 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_1 Y_1 Z_1 : T
inst_2 : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : P.IsStableUnderBaseChangeAlong g
inst_5 : Q.IsStableUnderBaseChange
inst_6 : HasPullbacks.{v_1, u_1} T
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (f ≫ g = fg) pullbackMapHomPullback._auto_1
subst : P.IsStableUnderBaseChangeAlong (f ≫ g)
⊢ P.IsStableUnderBaseChangeAlong fg

Tactic:
subst hfg
-- 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_1 Y_1 Z_1 : T
inst_2 : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : P.IsStableUnderBaseChangeAlong g
inst_5 : Q.IsStableUnderBaseChange
inst_6 : HasPullbacks.{v_1, u_1} T
⊢ P.IsStableUnderBaseChangeAlong (f ≫ g)

Tactic:
infer_instance
-- 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_1 Y_1 Z_1 : T
inst_2 : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : P.IsStableUnderBaseChangeAlong g
inst_5 : Q.IsStableUnderBaseChange
inst_6 : HasPullbacks.{v_1, u_1} T
fg : X ⟶ Z
hfg : f ≫ g = fg
A : P.Over Q Z
⊢ A.toComma (P := P) (Q := Q) (W := ⊤).hom ≫ 𝟙 Z =
    𝟙 A.toComma (P := P) (Q := Q) (W := ⊤).left ≫ A.toComma (P := P) (Q := Q) (W := ⊤).hom

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_1 Y_1 Z_1 : T
inst_2 : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : P.IsStableUnderBaseChangeAlong g
inst_5 : Q.IsStableUnderBaseChange
inst_6 : HasPullbacks.{v_1, u_1} T
fg : X ⟶ Z
hfg : f ≫ g = fg
A : P.Over Q Z
⊢ pullback.map A.toComma (P := P) (Q := Q) (W := ⊤).hom fg A.toComma (P := P) (Q := Q) (W := ⊤).hom g
        (𝟙 A.toComma (P := P) (Q := Q) (W := ⊤).left) f (𝟙 Z) ⋯ ⋯ ≫
      (Functor.obj (pullback P Q g) A).toComma (P := P) (Q := Q) (W := ⊤).hom =
    (Functor.obj (pullback P Q fg ⋙ map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).hom

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_1 Y_1 Z_1 : T
inst_2 : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst_3 : P.IsStableUnderBaseChangeAlong f
inst_4 : P.IsStableUnderBaseChangeAlong g
inst_5 : Q.IsStableUnderBaseChange
inst_6 : HasPullbacks.{v_1, u_1} T
fg : X ⟶ Z
hfg : f ≫ g = fg
A : P.Over Q Z
⊢ A.toComma (P := P) (Q := Q) (W := ⊤).hom =
    𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := Q) (W := ⊤).left) ≫
      A.toComma (P := P) (Q := Q) (W := ⊤).hom

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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ 𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ≫
      (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).hom =
    A.toComma (P := P) (Q := Q) (W := ⊤).hom ≫ f

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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
        A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯ ≫
      (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).hom =
    (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).hom

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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
hg :
  Q (X := (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left)
    (pullback.fst (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).hom f)
hfg :
  Q
    (CategoryStruct.comp (Y :=
      (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left)
      (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
        A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
      (pullback.fst (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).hom f))
g :
  (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).left
apply : T
⊢ Q (Y := (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left)
    (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
      A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)

Tactic:
apply Q.of_postcomp (W' := Q)

Premises used: CategoryTheory.MorphismProperty.of_postcomp
-- 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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q (X := (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left)
    (pullback.fst (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).hom f)

Tactic:
Q.pullback_fst _ _ hQf

Premises used: CategoryTheory.MorphismProperty.pullback_fst, CategoryTheory.Limits.limit
-- 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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q (X := (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left)
    (pullback.fst (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).hom f)

Tactic:
exact Q.pullback_fst _ _ hQf

Premises used: CategoryTheory.MorphismProperty.pullback_fst
-- 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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q
    (CategoryStruct.comp (Y :=
      (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) A).toComma (P := P) (Q := Q) (W := ⊤).left)
      (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
        A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
      (pullback.fst (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).hom f))

Tactic:
simpa using Q.of_isIso _

Premises used: CategoryTheory.MorphismProperty.of_isIso
-- 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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
h :
  Eq (α :=
    (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
        (Functor.map (𝟭 (P.Over Q X)) g ≫
          Over.homMk (P := P) (Q := Q)
            (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) B).toComma (P := P) (Q := Q) (W := ⊤).left)
              B.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
            ⋯ ⋯)))
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
        (Over.homMk (P := P) (Q := Q)
            (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
              A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
            ⋯ ⋯ ≫
          Functor.map (map (P := P) Q hPf ⋙ pullback P Q f) g)))
⊢ Eq (α := Functor.obj (𝟭 (P.Over Q X)) A ⟶ Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B)
    (Functor.map (𝟭 (P.Over Q X)) g ≫
      Over.homMk (P := P) (Q := Q)
        (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) B).toComma (P := P) (Q := Q) (W := ⊤).left)
          B.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
        ⋯ ⋯)
    (Over.homMk (P := P) (Q := Q)
        (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
          A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
        ⋯ ⋯ ≫
      Functor.map (map (P := P) Q hPf ⋙ pullback P Q f) g)

Tactic:
ext
-- 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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
⊢ Eq (α :=
    (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T)
        (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).left)
    (CategoryStruct.comp (Y :=
      Limits.pullback (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f)
      (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
            (Functor.map (𝟭 (P.Over Q X)) g ≫
              Over.homMk (P := P) (Q := Q)
                (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) B).toComma (P := P) (Q := Q) (W := ⊤).left)
                  B.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
                ⋯ ⋯)) :
        (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
          (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
      (pullback.fst (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f))
    (CategoryStruct.comp (Y :=
      Limits.pullback (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f)
      (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
            (Over.homMk (P := P) (Q := Q)
                (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
                  A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
                ⋯ ⋯ ≫
              Functor.map (map (P := P) Q hPf ⋙ pullback P Q f) g)) :
        (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
          (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
      (pullback.fst (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f))

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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
inst_6 : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
⊢ Eq (α := (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶ X)
    (CategoryStruct.comp (Y :=
      Limits.pullback (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f)
      (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
            (Functor.map (𝟭 (P.Over Q X)) g ≫
              Over.homMk (P := P) (Q := Q)
                (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) B).toComma (P := P) (Q := Q) (W := ⊤).left)
                  B.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
                ⋯ ⋯)) :
        (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
          (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
      (pullback.snd (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f))
    (CategoryStruct.comp (Y :=
      Limits.pullback (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f)
      (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := Q) (W := ⊤)
            (Over.homMk (P := P) (Q := Q)
                (pullback.lift (𝟙 (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left)
                  A.toComma (P := P) (Q := Q) (W := ⊤).hom ⋯)
                ⋯ ⋯ ≫
              Functor.map (map (P := P) Q hPf ⋙ pullback P Q f) g)) :
        (Functor.obj (𝟭 (P.Over Q X)) A).toComma (P := P) (Q := Q) (W := ⊤).left ⟶
          (Functor.obj (map (P := P) Q hPf ⋙ pullback P Q f) B).toComma (P := P) (Q := Q) (W := ⊤).left)
      (pullback.snd (Functor.obj (map (P := P) Q hPf) B).toComma (P := P) (Q := Q) (W := ⊤).hom f))

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.IsStableUnderBaseChange
f : X ⟶ Y
inst_4 : P.HasPullbacksAlong f
inst_5 : P.IsStableUnderBaseChangeAlong f
hPf : P f
⊢ Functor.IsLeftAdjoint (C := P.Over ⊤ X) (Over.map (P := P) ⊤ hPf)

Tactic:
(Over.mapPullbackAdj P ⊤ f hPf trivial).isLeftAdjoint

Premises used: trivial, CategoryTheory.MorphismProperty.Over.mapPullbackAdj, CategoryTheory.Adjunction.isLeftAdjoint, Top.top