awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H_1 : IsPullback f' i₁ i₂ (f ≫ g)
H :
  IsPullback (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g)) i₁ i₂ (f ≫ g)
this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g) = f'
⊢ P (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯)

Tactic:
hf _ _ _ (H.of_right (pullback.lift_snd _ _ _) (IsPullback.of_hasPullback i₂ g))

Premises used: CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.of_right
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H_1 : IsPullback f' i₁ i₂ (f ≫ g)
H :
  IsPullback (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g)) i₁ i₂ (f ≫ g)
this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g) = f'
⊢ P (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯)

Tactic:
exact hf _ _ _ (H.of_right (pullback.lift_snd _ _ _) (IsPullback.of_hasPullback i₂ g))

Premises used: CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.of_right
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P.universally f
rw : f = 𝟙 X ≫ f
rw₁ rw₂ : f = f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
rw [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P.universally f
⊢ P f

Tactic:
exact hf (𝟙 _) (𝟙 _) _ (IsPullback.of_vert_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩)

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.CategoryStruct.id, CategoryTheory.CommSq.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (P ⊓ Q).universally f ↔ (P.universally ⊓ Q.universally) f
⊢ (P ⊓ Q).universally = P.universally ⊓ Q.universally

Tactic:
ext X Y f
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
h :
  (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → (P ⊓ Q) f') ↔
    ∀ (x x_1 : C) (x_2 : x ⟶ X) (x_3 : x_1 ⟶ Y) (x_4 : x ⟶ x_1) (x_5 : IsPullback x_4 x_2 x_3 f), P x_4 ∧ Q x_4
⊢ (P ⊓ Q).universally f ↔ P.universally f ∧ Q.universally f

Tactic:
simp_rw [universally, ← forall_and]

Premises used: CategoryTheory.MorphismProperty.universally, forall_and
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → (P ⊓ Q) f') ↔
    ∀ (x x_1 : C) (x_2 : x ⟶ X) (x_3 : x_1 ⟶ Y) (x_4 : x ⟶ x_1) (x_5 : IsPullback x_4 x_2 x_3 f), P x_4 ∧ Q x_4

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.universally = P ↔ P.IsStableUnderBaseChange

Tactic:
⟨(· ▸ P.universally_isStableUnderBaseChange),
    fun hP ↦ P.universally_le.antisymm fun _ _ _ hf _ _ _ _ _ H => hP.of_isPullback H.flip hf⟩

Premises used: CategoryTheory.MorphismProperty.universally_le, LE.le.antisymm, Eq.rec, CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange, CategoryTheory.IsPullback.flip, Iff.intro, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.IsStableUnderBaseChange
⊢ P.universally = P

Tactic:
universally_eq_iff.mpr hP

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.universally_eq_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Monotone (α := MorphismProperty.{v, u} C) universally

Tactic:
fun _ _ h _ _ _ h₁ _ _ _ _ _ H => h _ (h₁ _ _ _ H)

Premises used: Monotone, CategoryTheory.MorphismProperty.universally
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst_2 : HasPullback f g], P (X := pullback f g) (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
have : ∀ (this : HasPullback i₂ g), P f'
⊢ P f'

Tactic:
have := h.hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst_2 : HasPullback f g], P (X := pullback f g) (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
rw : P (X := pullback i₂ g) (pullback.fst i₂ g)
⊢ P f'

Tactic:
rw [← h.isoPullback_hom_fst, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.IsPullback.isoPullback_hom_fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst_2 : HasPullback f g], P (X := pullback f g) (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
⊢ P (X := pullback i₂ g) (pullback.fst i₂ g)

Tactic:
H ..
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst_2 : HasPullback f g], P (X := pullback f g) (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
⊢ P (X := pullback i₂ g) (pullback.fst i₂ g)

Tactic:
exact H ..
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderBaseChangeAgainst ⊤
x x_1 x_2 x_3 : C
x_4 : x ⟶ x_3
x_5 : x_1 ⟶ x_3
x_6 : x_2 ⟶ x_1
x_7 : x_2 ⟶ x
h' : IsPullback x_6 x_7 x_5 x_4
h'' : P x_5
⊢ ⊤ x_4

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.HasPullbacksAgainst ⊤
X Y S : C
f : X ⟶ S
x : Y ⟶ S
h' : P f
⊢ ⊤ x

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P P' : MorphismProperty.{v, u} C
c c' c'' : C
f : c ⟶ c'
g : c'' ⟶ c'
inst_1 : P.HasPullbacksAgainst P'
hf : P f
hg : P' g
⊢ HasPullback f g

Tactic:
letI : P.HasPullbacksAlong g :=
    MorphismProperty.HasPullbacksAgainst.hasPullbacksAlong g hg
  MorphismProperty.HasPullbacksAlong.hasPullback f hf

Premises used: CategoryTheory.MorphismProperty.HasPullbacksAlong.hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderCobaseChangeAgainst ⊤
x x_1 x_2 x_3 : C
x_4 : x ⟶ x_1
x_5 : x ⟶ x_2
x_6 : x_2 ⟶ x_3
x_7 : x_1 ⟶ x_3
h' : IsPushout x_5 x_4 x_6 x_7
h'' : P x_4
⊢ ⊤ x_5

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.HasPushoutsAgainst ⊤
X Y S : C
f : S ⟶ X
x : S ⟶ Y
h' : P f
⊢ ⊤ x

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P P' : MorphismProperty.{v, u} C
c c' c'' : C
f : c ⟶ c'
g : c ⟶ c''
inst_1 : P.HasPushoutsAgainst P'
hf : P f
hg : P' g
⊢ HasPushout f g

Tactic:
letI : P.HasPushoutsAlong g :=
    MorphismProperty.HasPushoutsAgainst.hasPushoutsAlong g hg
  MorphismProperty.HasPushoutsAlong.hasPushout f hf

Premises used: CategoryTheory.MorphismProperty.HasPushoutsAlong.hasPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
K_1 : Precoverage.{v, u} C
P : MorphismProperty.{v, u} C
K L : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
⊢ ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) (i : 𝒰.I₀) (hf : ⊤ f),
    ⊤ (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
K_1 : Precoverage.{v, u} C
P : MorphismProperty.{v, u} C
K L : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
⊢ ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y)
    (h : ∀ (i : 𝒰.I₀), ⊤ (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))), ⊤ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
X' : C
i : 𝒰.I₀
fst : X' ⟶ X
snd : X' ⟶ 𝒰.X i
h : IsPullback fst snd f (𝒰.f i)
hf : P f
rw : P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ P snd

Tactic:
rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]

Premises used: CategoryTheory.IsPullback.isoPullback_inv_snd, CategoryTheory.IsPullback.isoPullback, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
X' : C
i : 𝒰.I₀
fst : X' ⟶ X
snd : X' ⟶ 𝒰.X i
h : IsPullback fst snd f (𝒰.f i)
hf : P f
⊢ P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))

Tactic:
pullbackSnd _ _ hf

Premises used: CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
X' : C
i : 𝒰.I₀
fst : X' ⟶ X
snd : X' ⟶ 𝒰.X i
h : IsPullback fst snd f (𝒰.f i)
hf : P f
⊢ P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))

Tactic:
exact pullbackSnd _ _ hf

Premises used: CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
⊢ P f ↔ ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))

Tactic:
⟨fun hf _ ↦ pullbackSnd _ _ hf, fun h ↦ of_zeroHypercover _ h⟩

Premises used: CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover, CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd, Iff.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : Precoverage.ZeroHypercover.{w, v, u} K Y
inst_3 : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
rw :
  ∀ (i : 𝒰.restrictIndexOfSmall.I₀),
    P (X := pullback f (𝒰.restrictIndexOfSmall.f i)) (pullback.snd f (𝒰.restrictIndexOfSmall.f i))
⊢ P f

Tactic:
rw [IsLocalAtTarget.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]

Premises used: CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover, CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : Precoverage.ZeroHypercover.{w, v, u} K Y
inst_3 : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ ∀ (i : 𝒰.restrictIndexOfSmall.I₀),
    P (X := pullback f (𝒰.restrictIndexOfSmall.f i)) (pullback.snd f (𝒰.restrictIndexOfSmall.f i))

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
K_1 : Precoverage.{v, u} C
P : MorphismProperty.{v, u} C
K L : Precoverage.{v, u} C
⊢ ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) (i : 𝒰.I₀) (hf : ⊤ f), ⊤ (𝒰.f i ≫ f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
K_1 : Precoverage.{v, u} C
P : MorphismProperty.{v, u} C
K L : Precoverage.{v, u} C
⊢ ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X), (∀ (i : 𝒰.I₀), ⊤ (𝒰.f i ≫ f)) → ⊤ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
⊢ P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)

Tactic:
⟨fun hf i ↦ comp _ i hf, fun h ↦ of_zeroHypercover _ h⟩

Premises used: CategoryTheory.MorphismProperty.IsLocalAtSource.comp, CategoryTheory.MorphismProperty.IsLocalAtSource.of_zeroHypercover, Iff.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : Precoverage.ZeroHypercover.{w, v, u} K X
inst_2 : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
rw : ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (𝒰.restrictIndexOfSmall.f i ≫ f)
⊢ P f

Tactic:
rw [IsLocalAtSource.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall, CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : Precoverage.ZeroHypercover.{w, v, u} K X
inst_2 : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (𝒰.restrictIndexOfSmall.f i ≫ f)

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
i : 𝒰.I₀
⊢ s ≫ 𝟙 S = f ≫ t

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
i : 𝒰.I₀
⊢ 𝒰.f i ≫ 𝟙 S = 𝟙 (𝒰.X i) ≫ 𝒰.f i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
i : 𝒰.I₀
⊢ s ≫ 𝟙 S = g ≫ t

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
H :
  ∀ (i : 𝒰.I₀),
    Eq (α := pullback s (𝒰.f i) ⟶ pullback t (𝒰.f i)) (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
      (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 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.Local
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
H :
  ∀ (i : 𝒰.I₀),
    Eq (α := pullback s (𝒰.f i) ⟶ pullback t (𝒰.f i)) (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
      (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
rw :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀),
    MorphismProperty.isomorphisms C (X :=
      pullback (X := equalizer f g) (equalizer.ι f g) ((Precoverage.ZeroHypercover.pullback₁ s 𝒰).f i))
      (pullback.snd (equalizer.ι f g) ((Precoverage.ZeroHypercover.pullback₁ s 𝒰).f i))
⊢ MorphismProperty.isomorphisms C (X := equalizer f g) (equalizer.ι f g)

Tactic:
rw [(MorphismProperty.isomorphisms C).iff_of_zeroHypercover_target (𝒰.pullback₁ s)]

Premises used: CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target, CategoryTheory.Precoverage.ZeroHypercover.pullback₁
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
H :
  ∀ (i : 𝒰.I₀),
    Eq (α := pullback s (𝒰.f i) ⟶ pullback t (𝒰.f i)) (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
      (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶ X)
    (pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ≫ pullback.fst s (𝒰.f i) :
      pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶ X)
    (CategoryStruct.comp (Y := pullback s (𝒰.f i))
        (CategoryStruct.comp (Y :=
            equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
              (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
              (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
            (Iso.inv (equalizerPullbackMapIso hf hg (𝒰.f i)) :
              pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
                equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
                  (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
                  (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
            (equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
                (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯) :
              equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
                  (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
                  (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯) ⟶
                pullback s (𝒰.f i)) :
          pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
            pullback s (𝒰.f i))
        (pullback.fst s (𝒰.f i) : pullback s (𝒰.f i) ⟶ X) :
      pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶ X)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.MorphismProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage.{v, u} C
𝒰 : J.ZeroHypercover S
inst_3 : J.IsStableUnderBaseChange
inst_4 : MorphismProperty.IsLocalAtTarget (MorphismProperty.isomorphisms C) J
H :
  ∀ (i : 𝒰.I₀),
    Eq (α := pullback s (𝒰.f i) ⟶ pullback t (𝒰.f i)) (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
      (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
i : (Precoverage.ZeroHypercover.pullback₁ s 𝒰).I₀
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶ 𝒰.X i)
    (pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ≫ pullback.snd s (𝒰.f i) :
      pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶ 𝒰.X i)
    (CategoryStruct.comp (Y := pullback s (𝒰.f i))
        (CategoryStruct.comp (Y :=
            equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
              (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
              (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
            (Iso.inv (equalizerPullbackMapIso hf hg (𝒰.f i)) :
              pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
                equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
                  (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
                  (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯))
            (equalizer.ι (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
                (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯) :
              equalizer (X := pullback s (𝒰.f i)) (Y := pullback t (𝒰.f i))
                  (pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯)
                  (pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯) ⟶
                pullback s (𝒰.f i)) :
          pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶
            pullback s (𝒰.f i))
        (pullback.snd s (𝒰.f i) : pullback s (𝒰.f i) ⟶ 𝒰.X i) :
      pullback (X := equalizer f g) (Y := pullback s (𝒰.f i)) (equalizer.ι f g) (pullback.fst s (𝒰.f i)) ⟶ 𝒰.X i)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition