awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q_1 W : MorphismProperty.{v_1, u_1} C
A X_1 Y_1 Z_1 : C
fst : A ⟶ X_1
snd : A ⟶ Y_1
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.DescendsAlong Q
inst_3 : P.RespectsIso
inst_4 : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_5 : HasPullback f g
hf : Q f
hfst : P.diagonal (X := pullback f g) (pullback.fst f g)
heq :
  Eq (α :=
    pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
        (pullback.diagonal g) ⟶
      pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (Iso.hom (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)) ≫
        Iso.hom (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)) ≫
          CategoryStruct.comp (Y := pullback g f) (Iso.hom (pullback.congrHom ⋯ ⋯))
            (Iso.hom (pullbackSymmetry g f) ≫
              CategoryStruct.comp (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (pullback.diagonal (pullback.fst f g) :
                  pullback f g ⟶ pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (Iso.hom (diagonalObjPullbackFstIso f g) :
                  pullback.diagonalObj (X := pullback f g) (pullback.fst f g) ⟶
                    pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)
⊢ P (Y := pullback.diagonalObj g) (pullback.diagonal g)
have H : Q (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
Tactic: apply MorphismProperty.of_pullback_fst_of_descendsAlong (P := P) (Q := Q)
      (f := pullback.fst (pullback.snd g g ≫ g) f)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q_1 W : MorphismProperty.{v_1, u_1} C
A X_1 Y_1 Z_1 : C
fst : A ⟶ X_1
snd : A ⟶ Y_1
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.DescendsAlong Q
inst_3 : P.RespectsIso
inst_4 : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_5 : HasPullback f g
hf : Q f
hfst : P.diagonal (X := pullback f g) (pullback.fst f g)
heq :
  Eq (α :=
    pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
        (pullback.diagonal g) ⟶
      pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (Iso.hom (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)) ≫
        Iso.hom (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)) ≫
          CategoryStruct.comp (Y := pullback g f) (Iso.hom (pullback.congrHom ⋯ ⋯))
            (Iso.hom (pullbackSymmetry g f) ≫
              CategoryStruct.comp (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (pullback.diagonal (pullback.fst f g) :
                  pullback f g ⟶ pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (Iso.hom (diagonalObjPullbackFstIso f g) :
                  pullback.diagonalObj (X := pullback f g) (pullback.fst f g) ⟶
                    pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)
H : Q (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
⊢ P (Y := pullback.diagonalObj g) (pullback.diagonal g)
have H₁ : P (X :=
  pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
    (pullback.diagonal g))
  (pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g))
Tactic: apply MorphismProperty.of_pullback_fst_of_descendsAlong (P := P) (Q := Q)
      (f := pullback.fst (pullback.snd g g ≫ g) f)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q_1 W : MorphismProperty.{v_1, u_1} C
A X_1 Y_1 Z_1 : C
fst : A ⟶ X_1
snd : A ⟶ Y_1
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.DescendsAlong Q
inst_3 : P.RespectsIso
inst_4 : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_5 : HasPullback f g
hf : Q f
hfst : P.diagonal (X := pullback f g) (pullback.fst f g)
heq :
  Eq (α :=
    pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
        (pullback.diagonal g) ⟶
      pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (Iso.hom (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)) ≫
        Iso.hom (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)) ≫
          CategoryStruct.comp (Y := pullback g f) (Iso.hom (pullback.congrHom ⋯ ⋯))
            (Iso.hom (pullbackSymmetry g f) ≫
              CategoryStruct.comp (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (pullback.diagonal (pullback.fst f g) :
                  pullback f g ⟶ pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
                (Iso.hom (diagonalObjPullbackFstIso f g) :
                  pullback.diagonalObj (X := pullback f g) (pullback.fst f g) ⟶
                    pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)) :
      pullback (X := pullback (X := pullback g g) (pullback.snd g g ≫ g) f) (pullback.fst (pullback.snd g g ≫ g) f)
          (pullback.diagonal g) ⟶
        pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)
⊢ P (X := pullback f g) (Y := pullback (X := pullback g g) (pullback.snd g g ≫ g) f)
    (CategoryStruct.comp (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
        (pullback.diagonal (pullback.fst f g) :
          pullback f g ⟶ pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
        (Iso.hom (diagonalObjPullbackFstIso f g) :
          pullback.diagonalObj (X := pullback f g) (pullback.fst f g) ⟶
            pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f) :
      pullback f g ⟶ pullback (X := pullback.diagonalObj g) (pullback.snd g g ≫ g) f)
have H : P (X := pullback f g) (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
  (pullback.diagonal (pullback.fst f g))
Tactic: rwa [cancel_right_of_respectsIso (P := P)]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasEqualizers.{v_1, u_1} C
inst_4 : HasPullbacks.{v_1, u_1} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H :
  Eq (α := pullback s v ⟶ pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
    (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)
⊢ f = g
have suffices : IsIso (X := equalizer f g) (equalizer.ι f g)
Tactic: suffices IsIso (equalizer.ι f g) from Limits.eq_of_epi_equalizer
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasEqualizers.{v_1, u_1} C
inst_4 : HasPullbacks.{v_1, u_1} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H :
  Eq (α := pullback s v ⟶ pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
    (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)
⊢ isomorphisms C (X := equalizer f g) (equalizer.ι f g)
have apply : isomorphisms C (X := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
  (pullback.snd (equalizer.ι f g) (pullback.fst s v))
Tactic: apply (MorphismProperty.isomorphisms C).of_isPullback_of_descendsAlong
    (IsPullback.of_hasPullback _ _).flip (P.pullback_fst s v hv)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasEqualizers.{v_1, u_1} C
inst_4 : HasPullbacks.{v_1, u_1} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H :
  Eq (α := pullback s v ⟶ pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
    (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
    (pullback.snd (equalizer.ι f g) (pullback.fst s v) :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
    (CategoryStruct.comp (Y :=
        equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
          (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
        (Iso.inv (equalizerPullbackMapIso hf hg v) :
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶
            equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯))
        (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) :
          equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
              (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ⟶
            pullback s v) :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
have h₀ : Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X)
  (pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.fst s v :
    pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X)
  (CategoryStruct.comp (Y := pullback s v)
      (CategoryStruct.comp (Y :=
          equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry)
            (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry))
          (Iso.inv (equalizerPullbackMapIso hf hg v) :
            pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶
              equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry)
                (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry))
          (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry) (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry) :
            equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry)
                (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry) ⟶
              pullback s v) :
        pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
      (pullback.fst s v : pullback s v ⟶ X) :
    pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ X)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasEqualizers.{v_1, u_1} C
inst_4 : HasPullbacks.{v_1, u_1} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H :
  Eq (α := pullback s v ⟶ pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯)
    (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)
⊢ isomorphisms C (X := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
    (pullback.snd (equalizer.ι f g) (pullback.fst s v))
have this : Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
  (pullback.snd (equalizer.ι f g) (pullback.fst s v) :
    pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
  (CategoryStruct.comp (Y :=
      equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry)
        (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry))
      (Iso.inv (equalizerPullbackMapIso hf hg v) :
        pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶
          equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry)
            (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry))
      (equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry) (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry) :
        equalizer (X := pullback s v) (Y := pullback t v) (pullback.map s v t v f (𝟙 T) (𝟙 S) sorry sorry)
            (pullback.map s v t v g (𝟙 T) (𝟙 S) sorry sorry) ⟶
          pullback s v) :
    pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback s v)
Tactic: have : pullback.snd (equalizer.ι f g) (pullback.fst s v) =
      (equalizerPullbackMapIso hf hg _).inv ≫ equalizer.ι _ _ := by
    ext <;> simp [pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasPullbacks.{v_1, u_1} C
inst_4 : HasEqualizers.{v_1, u_1} C
S T : C
f : T ⟶ S
hf : P f
⊢ (Over.pullback f).Faithful
have refine : ∀ {X : Over.{v_1, u_1} S} (Y : Over.{v_1, u_1} S) (a b : X ⟶ Y)
  (hab : (Over.pullback f).map a = (Over.pullback f).map b), a = b
Tactic: refine ⟨fun {X} Y a b hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasPullbacks.{v_1, u_1} C
inst_4 : HasEqualizers.{v_1, u_1} C
S T : C
f : T ⟶ S
hf : P f
X Y : Over.{v_1, u_1} S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
⊢ a = b
have h : Over.Hom.left a = Over.Hom.left b
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasPullbacks.{v_1, u_1} C
inst_4 : HasEqualizers.{v_1, u_1} C
S T : C
f : T ⟶ S
hf : P f
X Y : Over.{v_1, u_1} S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
⊢ Over.Hom.left a = Over.Hom.left b
have h : Eq (α := pullback X.hom f ⟶ pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) sorry sorry)
  (pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) sorry sorry)
Tactic: apply P.eq_of_isomorphisms_descendsAlong (Over.w a) (Over.w b) f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasPullbacks.{v_1, u_1} C
inst_4 : HasEqualizers.{v_1, u_1} C
S T : C
f : T ⟶ S
hf : P f
X Y : Over.{v_1, u_1} S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
⊢ Eq (α := pullback X.hom f ⟶ pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯)
    (pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯)
have h : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left) →
  pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) sorry sorry = Over.Hom.left ((Over.pullback f).map a)
Tactic: convert! congr($(hab).left)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasPullbacks.{v_1, u_1} C
inst_4 : HasEqualizers.{v_1, u_1} C
S T : C
f : T ⟶ S
hf : P f
X Y : Over.{v_1, u_1} S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
h :
  (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left) →
    pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯ = Over.Hom.left ((Over.pullback f).map a)
⊢ Eq (α := pullback X.hom f ⟶ pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯)
    (pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯)
have h₁ : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left) →
  pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) sorry sorry = Over.Hom.left ((Over.pullback f).map b)
Tactic: convert! congr($(hab).left)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasPullbacks.{v_1, u_1} C
inst_4 : HasEqualizers.{v_1, u_1} C
S T : C
f : T ⟶ S
hf : P f
X Y : Over.{v_1, u_1} S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1 : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯ = Over.Hom.left ((Over.pullback f).map a)
have h : CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) sorry sorry)
    (pullback.fst Y.hom f) =
  Over.Hom.left ((Over.pullback f).map a) ≫ pullback.fst Y.hom f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasPullbacks.{v_1, u_1} C
inst_4 : HasEqualizers.{v_1, u_1} C
S T : C
f : T ⟶ S
hf : P f
X Y : Over.{v_1, u_1} S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1 : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
h :
  CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯)
      (pullback.fst Y.hom f) =
    Over.Hom.left ((Over.pullback f).map a) ≫ pullback.fst Y.hom f
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯ = Over.Hom.left ((Over.pullback f).map a)
have h₁ : CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) sorry sorry)
    (pullback.snd Y.hom f) =
  Over.Hom.left ((Over.pullback f).map a) ≫ pullback.snd Y.hom f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasPullbacks.{v_1, u_1} C
inst_4 : HasEqualizers.{v_1, u_1} C
S T : C
f : T ⟶ S
hf : P f
X Y : Over.{v_1, u_1} S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1 : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯ = Over.Hom.left ((Over.pullback f).map b)
have h : CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) sorry sorry)
    (pullback.fst Y.hom f) =
  Over.Hom.left ((Over.pullback f).map b) ≫ pullback.fst Y.hom f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : DescendsAlong (isomorphisms C) P
inst_2 : P.IsStableUnderBaseChange
inst_3 : HasPullbacks.{v_1, u_1} C
inst_4 : HasEqualizers.{v_1, u_1} C
S T : C
f : T ⟶ S
hf : P f
X Y : Over.{v_1, u_1} S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1 : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
h :
  CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯)
      (pullback.fst Y.hom f) =
    Over.Hom.left ((Over.pullback f).map b) ≫ pullback.fst Y.hom f
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯ = Over.Hom.left ((Over.pullback f).map b)
have h₁ : CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) sorry sorry)
    (pullback.snd Y.hom f) =
  Over.Hom.left ((Over.pullback f).map b) ≫ pullback.snd Y.hom f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst_2 : HasPushout f g], Q f → P (Y := pushout f g) (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
⊢ P g
have have : ∀ (this : HasPushout f g), P g
Tactic: have : HasPushout f g := h.hasPushout
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst_2 : HasPushout f g], Q f → P (Y := pushout f g) (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
this : HasPushout f g
⊢ P g
have apply : P (Y := pushout f g) (pushout.inl f g)
Tactic: apply H hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst_2 : HasPushout f g], Q f → P (Y := pushout f g) (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
this : HasPushout f g
⊢ P (Y := pushout f g) (pushout.inl f g)
have rwa : P (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (Iso.inv h.isoPushout))
Tactic: rwa [← P.cancel_right_of_respectsIso _ h.isoPushout.inv, h.inl_isoPushout_inv]