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 : MorphismProperty.{v_1, u_1} T
X Y : T
inst_1 : P.IsStableUnderComposition
f : X ⟶ Y
inst_2 : P.HasPullbacksAlong f
inst_3 : P.IsStableUnderBaseChangeAlong f
hPf : P f
⊢ Functor.IsRightAdjoint (C := P.Over ⊤ X) (Over.pullback P ⊤ f)

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

Premises used: trivial, CategoryTheory.MorphismProperty.Over.mapPullbackAdj, CategoryTheory.Adjunction.isRightAdjoint, Top.top
-- 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
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
h_obj :
  ∀ (X_1 : P.Under Q Z), Functor.obj (map (P := P) Q ⋯) X_1 = Functor.obj (map (P := P) Q hg ⋙ map (P := P) Q hf) X_1
h_map :
  autoParam
    (∀ (X_1 Y_1 : P.Under Q Z) (f_1 : X_1 ⟶ Y_1),
      Eq (α := Functor.obj (map (P := P) Q ⋯) X_1 ⟶ Functor.obj (map (P := P) Q ⋯) Y_1)
        (Functor.map (map (P := P) Q ⋯) f_1)
        (CategoryStruct.comp (Y := Functor.obj (map (P := P) Q hg ⋙ map (P := P) Q hf) X_1) (eqToHom ⋯)
          (Functor.map (map (P := P) Q hg ⋙ map (P := P) Q hf) f_1 ≫ eqToHom ⋯)))
    Functor.ext._auto_1
⊢ Eq (α := P.Under Q Z ⥤ P.Under Q X) (map (P := P) Q ⋯) (map (P := P) Q hg ⋙ map (P := P) Q hf)

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.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
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ ∀ (X_1 : P.Under Q Z), Functor.obj (map (P := P) Q ⋯) X_1 = Functor.obj (map (P := P) Q hg ⋙ map (P := P) Q hf) X_1

Tactic:
simp [map, Comma.mapLeft, CategoryTheory.Comma.mapLeft, Comma.lift]

Premises used: CategoryTheory.MorphismProperty.Under.map, CategoryTheory.MorphismProperty.Comma.mapLeft, CategoryTheory.Comma.mapLeft, CategoryTheory.MorphismProperty.Comma.lift
-- 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
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Under Q Z
k : U ⟶ V
h_map :
  Eq (α :=
    (Functor.obj (map (P := P) Q ⋯) U).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
      (Functor.obj (map (P := P) Q ⋯) V).toComma (P := P) (Q := ⊤) (W := Q).right)
    (CommaMorphism.right (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q) (Functor.map (map (P := P) Q ⋯) k)))
    (CommaMorphism.right
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
        (CategoryStruct.comp (Y := Functor.obj (map (P := P) Q hg ⋙ map (P := P) Q hf) U) (eqToHom ⋯)
          (Functor.map (map (P := P) Q hg ⋙ map (P := P) Q hf) k ≫ eqToHom ⋯))))
⊢ Eq (α := Functor.obj (map (P := P) Q ⋯) U ⟶ Functor.obj (map (P := P) Q ⋯) V) (Functor.map (map (P := P) Q ⋯) k)
    (CategoryStruct.comp (Y := Functor.obj (map (P := P) Q hg ⋙ map (P := P) Q hf) U) (eqToHom ⋯)
      (Functor.map (map (P := P) Q hg ⋙ map (P := P) Q hf) k ≫ eqToHom ⋯))

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
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Under Q Z
k : U ⟶ V
⊢ Eq (α :=
    (Functor.obj (map (P := P) Q ⋯) U).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
      (Functor.obj (map (P := P) Q ⋯) V).toComma (P := P) (Q := ⊤) (W := Q).right)
    (CommaMorphism.right (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q) (Functor.map (map (P := P) Q ⋯) k)))
    (CommaMorphism.right
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
        (CategoryStruct.comp (Y := Functor.obj (map (P := P) Q hg ⋙ map (P := P) Q hf) U) (eqToHom ⋯)
          (Functor.map (map (P := P) Q hg ⋙ map (P := P) Q hf) k ≫ eqToHom ⋯))))

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.HasPushoutsAlong f
A : P.Under Q X
⊢ HasPushout A.toComma (P := P) (Q := ⊤) (W := Q).hom f

Tactic:
HasPushoutsAlong.hasPushout A.hom A.prop

Premises used: CategoryTheory.Comma.hom, CategoryTheory.MorphismProperty.Comma.toComma, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.MorphismProperty.HasPushoutsAlong.hasPushout
-- 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 X Y Z : T
f : Y ⟶ X
g : Z ⟶ Y
inst_2 : P.HasPushoutsAlong f
inst_3 : P.HasPushoutsAlong g
inst_4 : P.IsStableUnderCobaseChangeAlong g
A : P.Under Q Z
⊢ HasPushout (Y := pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom g)
    (pushout.inr A.toComma (P := P) (Q := ⊤) (W := Q).hom g) f

Tactic:
HasPushoutsAlong.hasPushout (pushout.inr A.hom g)
  (IsStableUnderCobaseChangeAlong.of_isPushout (IsPushout.of_hasPushout A.hom g).flip A.prop)

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong.of_isPushout, CategoryTheory.Comma.hom, CategoryTheory.MorphismProperty.Comma.toComma, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.IsPushout.flip, CategoryTheory.MorphismProperty.HasPushoutsAlong.hasPushout, CategoryTheory.Limits.pushout.inr
-- 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.IsStableUnderCobaseChangeAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong g
inst_4 : P.HasPushoutsAlong f
inst_5 : P.HasPushoutsAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderCobaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pushoutComp._auto_1
subst : P.HasPushoutsAlong (f ≫ g)
⊢ P.HasPushoutsAlong 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.IsStableUnderCobaseChangeAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong g
inst_4 : P.HasPushoutsAlong f
inst_5 : P.HasPushoutsAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderCobaseChange
⊢ P.HasPushoutsAlong (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.IsStableUnderCobaseChangeAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong g
inst_4 : P.HasPushoutsAlong f
inst_5 : P.HasPushoutsAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderCobaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pushoutComp._auto_1
this : P.HasPushoutsAlong fg
subst : ∀ (this : P.HasPushoutsAlong (f ≫ g)), P.IsStableUnderCobaseChangeAlong (f ≫ g)
⊢ P.IsStableUnderCobaseChangeAlong 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.IsStableUnderCobaseChangeAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong g
inst_4 : P.HasPushoutsAlong f
inst_5 : P.HasPushoutsAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderCobaseChange
this : P.HasPushoutsAlong (f ≫ g)
⊢ P.IsStableUnderCobaseChangeAlong (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.IsStableUnderCobaseChangeAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong g
inst_4 : P.HasPushoutsAlong f
inst_5 : P.HasPushoutsAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderCobaseChange
fg : X ⟶ Z
hfg : fg = f ≫ g
subst : P.HasPushoutsAlong (f ≫ g)
⊢ P.HasPushoutsAlong 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.IsStableUnderCobaseChangeAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong g
inst_4 : P.HasPushoutsAlong f
inst_5 : P.HasPushoutsAlong g
inst_6 : Q.RespectsIso
inst_7 : Q.IsStableUnderCobaseChange
fg : X_1 ⟶ Z
hfg : fg = f ≫ g
this_1 : P.HasPushoutsAlong fg
X : P.Under Q X_1
this : HasPushout X.toComma (P := P) (Q := ⊤) (W := Q).hom fg
⊢ (Functor.obj (pushout P Q fg) X).toComma (P := P) (Q := ⊤) (W := Q).hom ≫
      Iso.hom
        (pushout.congrHom ⋯ hfg ≪≫ Iso.symm (pushoutLeftPushoutInrIso X.toComma (P := P) (Q := ⊤) (W := Q).hom f g)) =
    (Functor.obj (pushout P Q f ⋙ pushout P Q g) X).toComma (P := P) (Q := ⊤) (W := Q).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
inst_2 : P.HasPushoutsAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong f
inst_4 : Q.IsStableUnderCobaseChange
g : X ⟶ Y
h : f = g
subst : P.HasPushoutsAlong f
⊢ P.HasPushoutsAlong 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.HasPushoutsAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong f
inst_4 : Q.IsStableUnderCobaseChange
⊢ P.HasPushoutsAlong 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.HasPushoutsAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong f
inst_4 : Q.IsStableUnderCobaseChange
g : X ⟶ Y
h : f = g
this : P.HasPushoutsAlong g
subst : ∀ (this : P.HasPushoutsAlong f), P.IsStableUnderCobaseChangeAlong f
⊢ P.IsStableUnderCobaseChangeAlong 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.HasPushoutsAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong f
inst_4 : Q.IsStableUnderCobaseChange
this : P.HasPushoutsAlong f
⊢ P.IsStableUnderCobaseChangeAlong 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.HasPushoutsAlong f
g : X ⟶ Y
inst_3 : P.IsStableUnderCobaseChangeAlong f
inst_4 : Q.IsStableUnderCobaseChange
h : f = g
A : P.Under Q X
subst : P.HasPushoutsAlong f
⊢ P.HasPushoutsAlong 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.HasPushoutsAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong f
inst_4 : Q.IsStableUnderCobaseChange
A : P.Under Q X
⊢ P.HasPushoutsAlong 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.HasPushoutsAlong f
g : X ⟶ Y
inst_3 : P.IsStableUnderCobaseChangeAlong f
inst_4 : Q.IsStableUnderCobaseChange
h : f = g
A : P.Under Q X
subst :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
      (Functor.obj (pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (CategoryStruct.comp (Y := Limits.pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom f)
        (pushout.inl A.toComma (P := P) (Q := ⊤) (W := Q).hom f :
          Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
            Limits.pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom f)
        (CommaMorphism.right
            (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
              (NatTrans.app (Iso.hom (pushoutCongr (P := P) (Q := Q) ⋯)) A)) :
          (Functor.obj (pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
            (Functor.obj (pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
        (Functor.obj (pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (pushout.inl A.toComma (P := P) (Q := ⊤) (W := Q).hom f :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
        Limits.pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom f)
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
      (Functor.obj (pushout P Q g) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (CategoryStruct.comp (Y := Limits.pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom f)
        (pushout.inl A.toComma (P := P) (Q := ⊤) (W := Q).hom f :
          Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
            Limits.pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom f)
        (CommaMorphism.right
            (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
              (NatTrans.app (Iso.hom (pushoutCongr (P := P) (Q := Q) h)) A)) :
          (Functor.obj (pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
            (Functor.obj (pushout P Q g) A).toComma (P := P) (Q := ⊤) (W := Q).right) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
        (Functor.obj (pushout P Q g) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (pushout.inl A.toComma (P := P) (Q := ⊤) (W := Q).hom g :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
        Limits.pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom 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 : T
f : X ⟶ Y
inst_2 : P.HasPushoutsAlong f
inst_3 : P.IsStableUnderCobaseChangeAlong f
inst_4 : Q.IsStableUnderCobaseChange
A : P.Under Q X
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
      (Functor.obj (pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (CategoryStruct.comp (Y := Limits.pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom f)
        (pushout.inl A.toComma (P := P) (Q := ⊤) (W := Q).hom f :
          Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
            Limits.pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom f)
        (CommaMorphism.right
            (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q)
              (NatTrans.app (Iso.hom (pushoutCongr (P := P) (Q := Q) ⋯)) A)) :
          (Functor.obj (pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
            (Functor.obj (pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
        (Functor.obj (pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (pushout.inl A.toComma (P := P) (Q := ⊤) (W := Q).hom f :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 T) A.toComma (P := P) (Q := ⊤) (W := Q).right ⟶
        Limits.pushout A.toComma (P := P) (Q := ⊤) (W := Q).hom f)

Tactic:
simp [pushoutCongr]

Premises used: CategoryTheory.MorphismProperty.Under.pushoutCongr
-- 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 : P.Under Q Y
⊢ (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom ≫
      𝟙
        (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) =
    f ≫ A.toComma (P := P) (Q := ⊤) (W := Q).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.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 : P.Under Q Y
⊢ (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).hom ≫
      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.obj (𝟭 (P.Under Q Y)) A).toComma (P := P) (Q := ⊤) (W := Q).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.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 : P.Under Q Y
hf :
  Q (Y := (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (pushout.inl (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
hfg :
  Q
    (CategoryStruct.comp (Y :=
      (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
      (pushout.inl (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (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 ⋯))
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 ⟶
    (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right
apply : T
⊢ Q (X := (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (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 ⋯)

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

Premises used: CategoryTheory.MorphismProperty.of_precomp
-- 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 : P.Under Q Y
⊢ Q (Y := (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (pushout.inl (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)

Tactic:
Q.pushout_inl _ _ hQf

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.MorphismProperty.pushout_inl
-- 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 : P.Under Q Y
⊢ Q (Y := (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
    (pushout.inl (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)

Tactic:
exact Q.pushout_inl _ _ hQf

Premises used: CategoryTheory.MorphismProperty.pushout_inl
-- 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 : P.Under Q Y
⊢ Q
    (CategoryStruct.comp (Y :=
      (Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A).toComma (P := P) (Q := ⊤) (W := Q).right)
      (pushout.inl (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := ⊤) (W := Q).hom f)
      (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 ⋯))

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.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
h :
  Eq (α :=
    (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)
    (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 ⋯)
            ⋯ ⋯)))
    (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)))
⊢ Eq (α := Functor.obj (map (P := P) Q hPf ⋙ pushout P Q f) A ⟶ Functor.obj (𝟭 (P.Under Q Y)) B)
    (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 ⋯)
        ⋯ ⋯)
    (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)

Tactic:
ext