awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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 H₁ H₂ H₃ :
  P (X := pullback f g) (Y := pullback.diagonalObj (X := pullback f g) (pullback.fst f g))
    (pullback.diagonal (pullback.fst f g))
⊢ 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)

Tactic:
rwa [cancel_right_of_respectsIso (P := P)]

Premises used: CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q W : MorphismProperty.{v_1, u_1} C
A X_1 Y_1 Z : C
fst : A ⟶ X_1
snd : A ⟶ Y_1
f_1 : X_1 ⟶ Z
g_1 : Y_1 ⟶ Z
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
⊢ s ≫ 𝟙 S = f ≫ t

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q W : MorphismProperty.{v_1, u_1} C
A X_1 Y_1 Z : C
fst : A ⟶ X_1
snd : A ⟶ Y_1
f_1 : X_1 ⟶ Z
g_1 : Y_1 ⟶ Z
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
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q W : MorphismProperty.{v_1, u_1} C
A X_1 Y_1 Z : C
fst : A ⟶ X_1
snd : A ⟶ Y_1
f_1 : X_1 ⟶ Z
g_1 : Y_1 ⟶ Z
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
⊢ s ≫ 𝟙 S = g ≫ t

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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) ⋯ ⋯)
suffices : IsIso (X := equalizer f g) (equalizer.ι f g)
⊢ f = g

Tactic:
suffices IsIso (equalizer.ι f g) from Limits.eq_of_epi_equalizer
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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) ⋯ ⋯)
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))
⊢ isomorphisms C (X := equalizer f g) (equalizer.ι f g)

Tactic:
apply (MorphismProperty.isomorphisms C).of_isPullback_of_descendsAlong
    (IsPullback.of_hasPullback _ _).flip (P.pullback_fst s v hv)

Premises used: CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong, CategoryTheory.MorphismProperty.pullback_fst, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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) ⟶ 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) ⋯ ⋯)
              (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)
        (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:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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) ⟶ T)
    (pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.snd s v :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)
    (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) ⋯ ⋯)
              (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)
        (pullback.snd s v : pullback s v ⟶ T) :
      pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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)

Tactic:
have : pullback.snd (equalizer.ι f g) (pullback.fst s v) =
      (equalizerPullbackMapIso hf hg _).inv ≫ equalizer.ι _ _ := by
    ext <;> simp [pullback.condition]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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) ⋯ ⋯)
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) ⋯ ⋯)
          (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)
⊢ 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:
simpa [this] using equalizer.ι_of_eq H

Premises used: CategoryTheory.Limits.equalizer.ι_of_eq
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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

Tactic:
⟨fun {X} Y a b hab ↦ ?_⟩

Premises used: CategoryTheory.Functor.Faithful.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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
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
⊢ (Over.pullback f).Faithful

Tactic:
refine ⟨fun {X} Y a b hab ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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 : Over.Hom.left a = Over.Hom.left b
⊢ a = b

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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 :
  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) ⋯ ⋯)
⊢ Over.Hom.left a = Over.Hom.left b

Tactic:
apply P.eq_of_isomorphisms_descendsAlong (Over.w a) (Over.w b) f hf

Premises used: CategoryTheory.Over.w, CategoryTheory.MorphismProperty.eq_of_isomorphisms_descendsAlong
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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 ((Over.pullback f).map a) = Over.Hom.left ((Over.pullback f).map b)

Tactic:
congr($(hab).left)

Premises used: congrArg, CategoryTheory.Over.Hom.left, id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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)
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) ⋯ ⋯ = Over.Hom.left ((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) ⋯ ⋯)

Tactic:
convert! congr($(hab).left)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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
h₁ :
  CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯)
      (pullback.snd Y.hom f) =
    Over.Hom.left ((Over.pullback f).map a) ≫ pullback.snd 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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
h₁ :
  CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯)
      (pullback.snd Y.hom f) =
    Over.Hom.left ((Over.pullback f).map b) ≫ pullback.snd 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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)
⊢ 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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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)
⊢ CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯)
      (pullback.snd Y.hom f) =
    Over.Hom.left ((Over.pullback f).map a) ≫ pullback.snd Y.hom f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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)
⊢ 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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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)
⊢ CategoryStruct.comp (Y := pullback Y.hom f) (pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯)
      (pullback.snd Y.hom f) =
    Over.Hom.left ((Over.pullback f).map b) ≫ pullback.snd Y.hom f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
Z X Y A : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ A
inr : Y ⟶ A
inst_1 : P.CodescendsAlong Q
h : IsPushout f g inl inr
hf : Q f
hinl : P inl
⊢ P g

Tactic:
CodescendsAlong.of_isPushout h hf hinl

Premises used: CategoryTheory.MorphismProperty.CodescendsAlong.of_isPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
Z X Y A : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ A
inr : Y ⟶ A
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.CodescendsAlong Q
h : IsPushout f g inl inr
hg : Q f
⊢ P inl ↔ P g

Tactic:
⟨fun hinl ↦ of_isPushout_of_codescendsAlong h hg hinl, fun hf ↦ P.of_isPushout h hf⟩

Premises used: CategoryTheory.MorphismProperty.of_isPushout_of_codescendsAlong, CategoryTheory.MorphismProperty.of_isPushout, Iff.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
inst_1 : P.CodescendsAlong Q
inst_2 : HasPushout f g
hf : Q f
hinl : P (Y := pushout f g) (pushout.inl f g)
⊢ P g

Tactic:
of_isPushout_of_codescendsAlong (.of_hasPushout f g) hf hinl

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout_of_codescendsAlong