awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EpiMono (hypothesis)
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)))
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ
have this₁ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EpiMono (hypothesis)
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)))
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ
have this₁ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EpiMono (hypothesis)
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)))
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ
have this₁ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EpiMono (goal)
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) φ
have 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)))
Tactic: rw [← data.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
⊢ 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))
have 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))
Tactic: rw [Presieve.compatible_iff_sieveCompatible]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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
⊢ 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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))
⊢ 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))
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
⊢ Presieve.IsSheafFor P S.arrows ↔ Nonempty (IsLimit (Fork.ofι (forkMap P S.arrows) ⋯))
have rw : Presieve.IsSheafFor P S.arrows ↔
  ∀ (a : Presieve.FamilyOfElements P S.arrows),
    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))
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
              a) :
          (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))
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
              a) :
          (fun (X : Type (max u v)) ↦ X) (SecondObj P S)) →
      ∃! x : P.obj (op X),
        Eq (α := (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) :
                (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op X))) →
                  (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
              x :
            (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
          (((firstObjEqFamily P S.arrows).toEquiv.symm :
                (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
              a :
            FirstObj P S.arrows)
Tactic: rw [Types.type_equalizer_iff_unique,
    ← Equiv.forall_congr_right (firstObjEqFamily P (S : Presieve X)).toEquiv.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      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))
              (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a) :
            (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))
              (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a) :
            (fun (X : Type (max u v)) ↦ X) (SecondObj P S)) →
        ∃! x : P.obj (op X),
          Eq (α := (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) :
                  (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op X))) →
                    (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
                x :
              (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a :
              FirstObj P S.arrows)
have simp_rw : Presieve.IsSheafFor P S.arrows ↔
  ∀ (a : Presieve.FamilyOfElements P S.arrows),
    Presieve.FamilyOfElements.Compatible (P := P) (R := S.arrows)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
              (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
              a) :
          Presieve.FamilyOfElements P S.arrows) →
      ∃! x : P.obj (op X),
        Eq (α := FirstObj P S.arrows)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
              x :
            FirstObj P S.arrows)
          (((firstObjEqFamily P S.arrows).toEquiv.symm :
                (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
              a :
            FirstObj P S.arrows)
Tactic: simp_rw [← compatible_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
| Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible (P := P) (R := S.arrows)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
                (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
              (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a) :
            Presieve.FamilyOfElements P S.arrows) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P S.arrows)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
                x :
              FirstObj P S.arrows)
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a :
              FirstObj P S.arrows)
have enter : ∀ (a : Presieve.FamilyOfElements P S.arrows),
  (((firstObjEqFamily P S.arrows).toEquiv.symm : (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows) a :
    FirstObj P S.arrows)
Tactic: enter [2, a, 1, 1, 2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
| Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible (P := P) (R := S.arrows)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
                (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
              (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a) :
            Presieve.FamilyOfElements P S.arrows) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P S.arrows)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
                x :
              FirstObj P S.arrows)
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a :
              FirstObj P S.arrows)
have enter : ∀ (a : Presieve.FamilyOfElements P S.arrows),
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).inv :
        (a : (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows)) →
          (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
      a :
    (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
Tactic: enter [2, a, 1, 1, 2]; rw [(firstObjEqFamily P S.arrows).toEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve.{v, u} X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible (P := P) (R := S.arrows)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
                (a : FirstObj P S.arrows) → Presieve.FamilyOfElements P S.arrows)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).inv :
                  (a : (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows)) →
                    (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows))
                a) :
            Presieve.FamilyOfElements P S.arrows) →
        ∃! x : P.obj (op X),
          Eq (α := FirstObj P S.arrows)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
                x :
              FirstObj P S.arrows)
            (((firstObjEqFamily P S.arrows).toEquiv.symm :
                  (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
                a :
              FirstObj P S.arrows)
have simp : Presieve.IsSheafFor P S.arrows ↔
  ∀ (a : Presieve.FamilyOfElements P S.arrows),
    a.Compatible (R := S.arrows) →
      ∃! x : P.obj (op X),
        Eq (α := FirstObj P S.arrows)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P S.arrows) : (a : P.obj (op X)) → FirstObj P S.arrows)
              x :
            FirstObj P S.arrows)
          (((firstObjEqFamily P S.arrows).toEquiv.symm :
                (a : Presieve.FamilyOfElements P S.arrows) → FirstObj P S.arrows)
              a :
            FirstObj P S.arrows)
Tactic: simp only [Iso.inv_hom_id_apply]