awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
data : FunctorialSurjectiveInjectiveFactorizationData.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_6 : HasWeakSheafify.{v, v', u, u'} J A
f : Arrow (Sheaf.{v, v', u, u'} J A)
⊢ IsLocallyInjective (FD := FA) (CD := CA)
    ((functorialLocallySurjectiveInjectiveFactorization J (FA := FA) (CA := CA) data).p (W₁ :=
          locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)).app
      f)

Tactic:
apply (functorialLocallySurjectiveInjectiveFactorization J data).hp

Premises used: CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization, CategoryTheory.MorphismProperty.FunctorialFactorizationData.hp
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
data : FunctorialSurjectiveInjectiveFactorizationData.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_6 : HasWeakSheafify.{v, v', u, u'} J A
f : Arrow (Sheaf.{v, v', u, u'} J A)
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
⊢ Epi
    ((functorialLocallySurjectiveInjectiveFactorization J (FA := FA) (CA := CA) data).i (W₁ :=
          locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)).app
      f)

Tactic:
apply epi_of_isLocallySurjective

Premises used: CategoryTheory.Sheaf.epi_of_isLocallySurjective
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
data : FunctorialSurjectiveInjectiveFactorizationData.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_6 : HasWeakSheafify.{v, v', u, u'} J A
f : Arrow (Sheaf.{v, v', u, u'} J A)
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
⊢ Mono
    ((functorialLocallySurjectiveInjectiveFactorization J (FA := FA) (CA := CA) data).p (W₁ :=
          locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)).app
      f)

Tactic:
apply mono_of_isLocallyInjective

Premises used: CategoryTheory.Sheaf.mono_of_isLocallyInjective
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
mp : IsLocallySurjective (FA := FA) (CA := CA) φ → Epi φ
mpr : Epi φ → IsLocallySurjective (FA := FA) (CA := CA) φ
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ ↔ Epi φ

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : IsLocallySurjective (FA := FA) (CA := CA) φ
⊢ Epi φ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : Epi φ
data : MorphismProperty.MapFactorizationData (locallySurjective J A (FA := FA) (CA := CA))
  (locallyInjective J A (FA := FA) (CA := CA)) φ :=
  MorphismProperty.factorizationData (locallySurjective J A (FA := FA) (CA := CA))
    (locallyInjective J A (FA := FA) (CA := CA)) φ
⊢ IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))

Tactic:
have : IsLocallySurjective data.i := data.hi
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : Epi φ
data : MorphismProperty.MapFactorizationData (locallySurjective J A (FA := FA) (CA := CA))
  (locallyInjective J A (FA := FA) (CA := CA)) φ :=
  MorphismProperty.factorizationData (locallySurjective J A (FA := FA) (CA := CA))
    (locallyInjective J A (FA := FA) (CA := CA)) φ
this :
  IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
⊢ IsLocallyInjective (FD := FA) (CD := CA)
    (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))

Tactic:
have : IsLocallyInjective data.p := data.hp
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : Epi φ
data : MorphismProperty.MapFactorizationData (locallySurjective J A (FA := FA) (CA := CA))
  (locallyInjective J A (FA := FA) (CA := CA)) φ :=
  MorphismProperty.factorizationData (locallySurjective J A (FA := FA) (CA := CA))
    (locallyInjective J A (FA := FA) (CA := CA)) φ
this_1 :
  IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this :
  IsLocallyInjective (FD := FA) (CD := CA)
    (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
⊢ Epi (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))

Tactic:
have : Epi data.p := epi_of_epi_fac data.fac
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : Epi φ
data : MorphismProperty.MapFactorizationData (locallySurjective J A (FA := FA) (CA := CA))
  (locallyInjective J A (FA := FA) (CA := CA)) φ :=
  MorphismProperty.factorizationData (locallySurjective J A (FA := FA) (CA := CA))
    (locallyInjective J A (FA := FA) (CA := CA)) φ
this_1 :
  IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this_2 :
  IsLocallyInjective (FD := FA) (CD := CA)
    (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this :
  Epi (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
⊢ Mono (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))

Tactic:
have := mono_of_isLocallyInjective data.p
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : Epi φ
data : MorphismProperty.MapFactorizationData (locallySurjective J A (FA := FA) (CA := CA))
  (locallyInjective J A (FA := FA) (CA := CA)) φ :=
  MorphismProperty.factorizationData (locallySurjective J A (FA := FA) (CA := CA))
    (locallyInjective J A (FA := FA) (CA := CA)) φ
this_1 :
  IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this_2 :
  IsLocallyInjective (FD := FA) (CD := CA)
    (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this_3 :
  Epi (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this :
  Mono (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
⊢ IsIso (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))

Tactic:
have := isIso_of_mono_of_epi data.p
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : Epi φ
data : MorphismProperty.MapFactorizationData (locallySurjective J A (FA := FA) (CA := CA))
  (locallyInjective J A (FA := FA) (CA := CA)) φ :=
  MorphismProperty.factorizationData (locallySurjective J A (FA := FA) (CA := CA))
    (locallyInjective J A (FA := FA) (CA := CA)) φ
this_1 :
  IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this_2 :
  IsLocallyInjective (FD := FA) (CD := CA)
    (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this_3 :
  Epi (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this_4 :
  Mono (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this :
  IsIso (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
mpr :
  IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)) ≫
      data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ

Tactic:
rw [← data.fac]

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.fac
-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
inst_6 : HasSheafify.{v, v', u, u'} J A
inst_7 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FA) (CC := CA))
inst_8 : Balanced (Sheaf.{v, v', u, u'} J A)
F G : Sheaf.{v, v', u, u'} J A
φ : F ⟶ G
h : Epi φ
data : MorphismProperty.MapFactorizationData (locallySurjective J A (FA := FA) (CA := CA))
  (locallyInjective J A (FA := FA) (CA := CA)) φ :=
  MorphismProperty.factorizationData (locallySurjective J A (FA := FA) (CA := CA))
    (locallyInjective J A (FA := FA) (CA := CA)) φ
this_1 :
  IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this_2 :
  IsLocallyInjective (FD := FA) (CD := CA)
    (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this_3 :
  Epi (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this_4 :
  Mono (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
this :
  IsIso (data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))
⊢ IsLocallySurjective (FA := FA) (CA := CA)
    (data.i (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)) ≫
      data.p (W₁ := locallySurjective J A (FA := FA) (CA := CA)) (W₂ := locallyInjective J A (FA := FA) (CA := CA)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
b : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }
x : P.obj (op X)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((forkMap P S.arrows ≫ firstMap P S) ≫
            Pi.π
              (fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ↦
                P.obj
                  (op
                    (f.snd (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }).fst (β :=
                      fun (Z : C) ↦
                      (_ : Z ⟶ f.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })) ×
                        { f' : f.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ⟶ X //
                          S.arrows f' }))))
              b)).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((forkMap P S.arrows ≫ secondMap P S) ≫
            Pi.π
              (fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ↦
                P.obj
                  (op
                    (f.snd (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }).fst (β :=
                      fun (Z : C) ↦
                      (_ : Z ⟶ f.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })) ×
                        { f' : f.fst (β := fun (Y : C) ↦ (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) ⟶ X //
                          S.arrows f' }))))
              b)).toFun
      x

Tactic:
simp [firstMap, secondMap, forkMap]

Premises used: CategoryTheory.Equalizer.forkMap, CategoryTheory.Equalizer.Sieve.secondMap, CategoryTheory.Equalizer.Sieve.firstMap
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
x : FirstObj P S.arrows
rw :
  Presieve.FamilyOfElements.SieveCompatible (C := C) (P := P) (X := X) (S := S)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
        x) ↔
    Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
⊢ Presieve.FamilyOfElements.Compatible (P := P) (R := S.arrows)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
        x) ↔
    Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S))

Tactic:
rw [Presieve.compatible_iff_sieveCompatible]

Premises used: CategoryTheory.Presieve.compatible_iff_sieveCompatible
-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
x : FirstObj P S.arrows
mp :
  Presieve.FamilyOfElements.SieveCompatible (C := C) (P := P) (X := X) (S := S)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
        x) →
    Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
mpr :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S)) →
    Presieve.FamilyOfElements.SieveCompatible (C := C) (P := P) (X := X) (S := S)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
        x)
⊢ Presieve.FamilyOfElements.SieveCompatible (C := C) (P := P) (X := X) (S := S)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
        x) ↔
    Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P S) :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
          x :
        (fun (X : Type (max u v)) ↦ X) (SecondObj P S))

Tactic:
constructor