awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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)
⊢ 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 ⋯)
have 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 sorry)
    (pullback.fst (Functor.obj (map (P := P) Q hPf) A).toComma (P := P) (Q := Q) (W := ⊤).hom f))
Tactic: apply Q.of_postcomp (W' := Q)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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))
⊢ 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 ⋯)
have 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
Tactic: apply Q.of_postcomp (W' := Q)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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 ⟶ 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)
have 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 sorry)
          sorry sorry)))
  (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 sorry)
          sorry sorry ≫
        Functor.map (map (P := P) Q hPf ⋙ pullback P Q f) g)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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 (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)))
have h : 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 sorry)
              sorry sorry)) :
      (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 sorry)
              sorry sorry ≫
            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: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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
⊢ Eq (α := P.Under Q Z ⥤ P.Under Q X) (map (P := P) Q ⋯) (map (P := P) Q hg ⋙ map (P := P) Q hf)
have h_obj : ∀ (X_1 : P.Under Q Z), Functor.obj (map (P := P) Q sorry) X_1 = Functor.obj (map (P := P) Q hg ⋙ map (P := P) Q hf) X_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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
⊢ Eq (α := P.Under Q Z ⥤ P.Under Q X) (map (P := P) Q ⋯) (map (P := P) Q hg ⋙ map (P := P) Q hf)
have h_map : autoParam
  (∀ (X_1 Y_1 : P.Under Q Z) (f_1 : X_1 ⟶ Y_1),
    Eq (α := Functor.obj (map (P := P) Q sorry) X_1 ⟶ Functor.obj (map (P := P) Q sorry) Y_1)
      (Functor.map (map (P := P) Q sorry) f_1)
      (CategoryStruct.comp (Y := Functor.obj (map (P := P) Q hg ⋙ map (P := P) Q hf) X_1) (eqToHom sorry)
        (Functor.map (map (P := P) Q hg ⋙ map (P := P) Q hf) f_1 ≫ eqToHom sorry)))
  Functor.ext._auto_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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 ⟶ 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 ⋯))
have h_map : Eq (α :=
  (Functor.obj (map (P := P) Q sorry) U).toComma (P := P) (Q := ⊤) (W := Q).right ⟶
    (Functor.obj (map (P := P) Q sorry) V).toComma (P := P) (Q := ⊤) (W := Q).right)
  (CommaMorphism.right (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := Q) (Functor.map (map (P := P) Q sorry) 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 sorry)
        (Functor.map (map (P := P) Q hg ⋙ map (P := P) Q hf) k ≫ eqToHom sorry))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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
⊢ P.HasPushoutsAlong fg
have subst : P.HasPushoutsAlong (f ≫ g)
Tactic: subst hfg
Cleared hypotheses: fg, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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
⊢ P.IsStableUnderCobaseChangeAlong fg
have subst : ∀ (this : P.HasPushoutsAlong (f ≫ g)), P.IsStableUnderCobaseChangeAlong (f ≫ g)
Tactic: subst hfg
Cleared hypotheses: fg, hfg, this
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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
⊢ P.HasPushoutsAlong fg
have subst : P.HasPushoutsAlong (f ≫ g)
Tactic: subst hfg
Cleared hypotheses: fg, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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
⊢ P.IsStableUnderCobaseChangeAlong g
have subst : ∀ (this : P.HasPushoutsAlong f), P.IsStableUnderCobaseChangeAlong f
Tactic: subst h
Cleared hypotheses: g, h, this
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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
⊢ 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)
have 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) sorry)) 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: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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 (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 ⋯)
have 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)
Tactic: apply Q.of_precomp (W' := Q)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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)
⊢ 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 ⋯)
have 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 sorry))
Tactic: apply Q.of_precomp (W' := Q)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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 ⋯))
⊢ 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 ⋯)
have 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
Tactic: apply Q.of_precomp (W' := Q)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.OverAdjunction (goal)
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
⊢ 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)
have 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 sorry)
          sorry sorry)))
  (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 sorry)
          sorry sorry ≫
        Functor.map (𝟭 (P.Under Q Y)) g)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Quotient (goal)
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
⊢ W f ↔ W g
have rel : ∀ (x y : X ⟶ Y) (h : homRel x y), W x ↔ W y
Tactic: induction h with
  | rel _ _ h => exact iff W h
  | refl => rfl
  | symm _ _ _ h => exact h.symm
  | trans _ _ _ _ _ h₁ h₂ => exact h₁.trans h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Quotient (goal)
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
⊢ W f ↔ W g
have refl : ∀ (x : X ⟶ Y), W x ↔ W x
Tactic: induction h with
  | rel _ _ h => exact iff W h
  | refl => rfl
  | symm _ _ _ h => exact h.symm
  | trans _ _ _ _ _ h₁ h₂ => exact h₁.trans h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Quotient (goal)
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
⊢ W f ↔ W g
have symm : ∀ (x y : X ⟶ Y), Relation.EqvGen homRel x y → ∀ (h : W x ↔ W y), W y ↔ W x
Tactic: induction h with
  | rel _ _ h => exact iff W h
  | refl => rfl
  | symm _ _ _ h => exact h.symm
  | trans _ _ _ _ _ h₁ h₂ => exact h₁.trans h₂
Cleared hypotheses: h