awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_2 : (ofArrows X c.inj).HasPairwisePullbacks
inst_3 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct.{u_1, v, u} X
⊢ IsIso (X := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (Y :=
    ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))
    (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj :
      F.obj
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (X x))
            (Fan.mk (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) (Pi.π fun (x : α) ↦ op (X x)))) ⟶
        Equalizer.Presieve.Arrows.FirstObj F X)
have refine : IsIso (Y := ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))
  (Equalizer.Presieve.Arrows.forkMap F X c.inj : F.obj (op c.pt) ⟶ Equalizer.Presieve.Arrows.FirstObj F X)
Tactic: refine IsIso.comp_isIso' inferInstance ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_2 : (ofArrows X c.inj).HasPairwisePullbacks
inst_3 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct.{u_1, v, u} X
⊢ IsIso (Y := ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))
    (Equalizer.Presieve.Arrows.forkMap F X c.inj : F.obj (op c.pt) ⟶ Equalizer.Presieve.Arrows.FirstObj F X)
have rw : ∀ (b : (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))),
  ∃! a : (fun (X : Type w) ↦ X) (F.obj (op c.pt)),
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Equalizer.Presieve.Arrows.forkMap F X c.inj) :
            TypeCat.Fun (F.obj (op c.pt)) (∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op c.pt))) →
            (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b)))
        a =
      b
Tactic: rw [isIso_iff_bijective, Function.bijective_iff_existsUnique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Preserves (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_2 : (ofArrows X c.inj).HasPairwisePullbacks
inst_3 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct.{u_1, v, u} X
⊢ ∀ (b : (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))),
    ∃! a : (fun (X : Type w) ↦ X) (F.obj (op c.pt)),
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Equalizer.Presieve.Arrows.forkMap F X c.inj) :
              TypeCat.Fun (F.obj (op c.pt)) (∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op c.pt))) →
              (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b)))
          a =
        b
have hF'₁ : ∀ (y : Equalizer.Presieve.Arrows.FirstObj F X),
  Eq (α := (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Equalizer.Presieve.Arrows.firstMap F X c.inj) :
            (a : (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.FirstObj F X)) →
              (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj))
          y :
        (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Equalizer.Presieve.Arrows.secondMap F X c.inj) :
            (a : (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.FirstObj F X)) →
              (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj))
          y :
        (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj)) →
    ∃! x : F.obj (op c.pt),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Equalizer.Presieve.Arrows.forkMap F X c.inj) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op c.pt))) →
              (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.FirstObj F X))
          x =
        y
Tactic: rw [Equalizer.Presieve.Arrows.sheaf_condition, Limits.Types.type_equalizer_iff_unique] at hF'
Cleared hypotheses: hF', this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
K : Type u_1
inst_2 : Category.{v_1, u_1} K
F : CategoryTheory.Functor.{v_1, v, u_1, u} K C
inst_3 : ∀ (X : Sheaf J (Type v)), PreservesLimit F.op (X.obj (P := Presheaf.IsSheaf J))
c : Cocone F
hc : IsColimit c
⊢ IsColimit (J.yoneda.mapCocone c)
have suffices : IsLimit (F := (F ⋙ J.yoneda).op ⋙ coyoneda) (mapCone coyoneda (J.yoneda.mapCocone c).op)
Tactic: suffices IsLimit (coyoneda.mapCone (J.yoneda.mapCocone c).op) from
      isColimitOfOp (isLimitOfReflects _ this)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
K : Type u_1
inst_2 : Category.{v_1, u_1} K
F : CategoryTheory.Functor.{v_1, v, u_1, u} K C
inst_3 : ∀ (X : Sheaf J (Type v)), PreservesLimit F.op (X.obj (P := Presheaf.IsSheaf J))
c : Cocone F
hc : IsColimit c
⊢ IsLimit (F := (F ⋙ J.yoneda).op ⋙ coyoneda) (mapCone coyoneda (J.yoneda.mapCocone c).op)
have t : (k : Sheaf J (Type v)) →
  IsLimit (F := ((F ⋙ J.yoneda).op ⋙ coyoneda) ⋙ obj (evaluation (Sheaf J (Type v)) (Type (max u v))) k)
    (mapCone (obj (evaluation (Sheaf J (Type v)) (Type (max u v))) k) (mapCone coyoneda (J.yoneda.mapCocone c).op))
Tactic: apply evaluationJointlyReflectsLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
K : Type u_1
inst_2 : Category.{v_1, u_1} K
F : CategoryTheory.Functor.{v_1, v, u_1, u} K C
inst_3 : ∀ (X : Sheaf J (Type v)), PreservesLimit F.op (X.obj (P := Presheaf.IsSheaf J))
c : Cocone F
hc : IsColimit c
X : Sheaf J (Type v)
⊢ IsLimit (F := ((F ⋙ J.yoneda).op ⋙ coyoneda) ⋙ obj (evaluation (Sheaf J (Type v)) (Type (max u v))) X)
    (mapCone (obj (evaluation (Sheaf J (Type v)) (Type (max u v))) X) (mapCone coyoneda (J.yoneda.mapCocone c).op))
have t : IsLimit ((X.obj (P := Presheaf.IsSheaf J) ⋙ uliftFunctor.{u, v}).mapCone c.op)
Tactic: suffices IsLimit ((X.obj ⋙ uliftFunctor).mapCone c.op) from IsLimit.mapConeEquiv
      (isoWhiskerRight (J.yonedaOpCompCoyoneda) ((evaluation _ _ ).obj X)).symm this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
K : Type u_1
inst_2 : Category.{v_1, u_1} K
F : CategoryTheory.Functor.{v_1, v, u_1, u} K C
inst_3 : ∀ (X : Sheaf J (Type (max v v'))), PreservesLimit F.op (X.obj (P := Presheaf.IsSheaf J))
c : Cocone F
hc : IsColimit c
⊢ IsColimit ((GrothendieckTopology.uliftYoneda.{v', v, u} J).mapCocone c)
have suffices : IsLimit (F := (F ⋙ GrothendieckTopology.uliftYoneda.{v', v, u} J).op ⋙ coyoneda)
  (mapCone coyoneda ((GrothendieckTopology.uliftYoneda.{v', v, u} J).mapCocone c).op)
Tactic: suffices IsLimit (coyoneda.mapCone (J.uliftYoneda.mapCocone c).op) from
      isColimitOfOp (isLimitOfReflects _ this)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
K : Type u_1
inst_2 : Category.{v_1, u_1} K
F : CategoryTheory.Functor.{v_1, v, u_1, u} K C
inst_3 : ∀ (X : Sheaf J (Type (max v v'))), PreservesLimit F.op (X.obj (P := Presheaf.IsSheaf J))
c : Cocone F
hc : IsColimit c
⊢ IsLimit (F := (F ⋙ GrothendieckTopology.uliftYoneda.{v', v, u} J).op ⋙ coyoneda)
    (mapCone coyoneda ((GrothendieckTopology.uliftYoneda.{v', v, u} J).mapCocone c).op)
have t : (k : Sheaf J (Type (max v v'))) →
  IsLimit (F :=
    ((F ⋙ GrothendieckTopology.uliftYoneda.{v', v, u} J).op ⋙ coyoneda) ⋙
      obj (evaluation (Sheaf J (Type (max v v'))) (Type (max (max u v) v'))) k)
    (mapCone (obj (evaluation (Sheaf J (Type (max v v'))) (Type (max (max u v) v'))) k)
      (mapCone coyoneda ((GrothendieckTopology.uliftYoneda.{v', v, u} J).mapCocone c).op))
Tactic: apply evaluationJointlyReflectsLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
K : Type u_1
inst_2 : Category.{v_1, u_1} K
F : CategoryTheory.Functor.{v_1, v, u_1, u} K C
inst_3 : ∀ (X : Sheaf J (Type (max v v'))), PreservesLimit F.op (X.obj (P := Presheaf.IsSheaf J))
c : Cocone F
hc : IsColimit c
X : Sheaf J (Type (max v v'))
⊢ IsLimit (F :=
    ((F ⋙ GrothendieckTopology.uliftYoneda.{v', v, u} J).op ⋙ coyoneda) ⋙
      obj (evaluation (Sheaf J (Type (max v v'))) (Type (max (max u v) v'))) X)
    (mapCone (obj (evaluation (Sheaf J (Type (max v v'))) (Type (max (max u v) v'))) X)
      (mapCone coyoneda ((GrothendieckTopology.uliftYoneda.{v', v, u} J).mapCocone c).op))
have t : IsLimit ((X.obj (P := Presheaf.IsSheaf J) ⋙ uliftFunctor.{u, max v v'}).mapCone c.op)
Tactic: suffices IsLimit ((X.obj ⋙ uliftFunctor).mapCone c.op) from IsLimit.mapConeEquiv
      (isoWhiskerRight (J.uliftYonedaOpCompCoyoneda) ((evaluation _ _ ).obj X)).symm this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
K : Type u_1
inst_2 : Category.{v_1, u_1} K
F : CategoryTheory.Functor.{v_1, v, u_1, u} K C
⊢ PreservesLimit F J.yoneda
have this : PreservesLimitsOfShape K (J.yoneda ⋙ sheafToPresheaf J (Type v))
Tactic: have : PreservesLimitsOfShape K (J.yoneda ⋙ sheafToPresheaf J (Type v)) :=
      preservesLimitsOfShape_of_natIso (yonedaCompSheafToPresheaf J).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
K : Type u_1
inst_2 : Category.{v_1, u_1} K
F : CategoryTheory.Functor.{v_1, v, u_1, u} K C
⊢ PreservesLimit F (GrothendieckTopology.uliftYoneda.{v', v, u} J)
have this : PreservesLimitsOfShape K (GrothendieckTopology.uliftYoneda.{v', v, u} J ⋙ sheafToPresheaf J (Type (max v v')))
Tactic: have : PreservesLimitsOfShape K (uliftYoneda J ⋙ sheafToPresheaf J (Type max v v')) :=
      preservesLimitsOfShape_of_natIso (uliftYonedaCompSheafToPresheaf J).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (Opposite.unop X))) ((K : (a : D) → Set (Sieve a)) (Opposite.unop X))
    (equalizerSieve (FD := FA) (CD := CA) a b)
have h₁ : ∀ ⦃Y : D⦄ ⦃f : Y ⟶ Opposite.unop X⦄,
  Sieve.arrows (Sieve.coverByImage H (Opposite.unop X)) f →
    Sieve.pullback f (equalizerSieve (FD := FA) (CD := CA) a b) ∈ (K : (a : D) → Set (Sieve a)) Y
Tactic: apply K.transitive (H.is_cover_of_isCoverDense K X.unop)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
Y : D
g : Y ⟶ Opposite.unop X
⊢ Sieve.arrows (Sieve.coverByImage H (Opposite.unop X)) g →
    Sieve.pullback g (equalizerSieve (FD := FA) (CD := CA) a b) ∈ (K : (a : D) → Set (Sieve a)) Y
have h₁ : ∀ (Z : C) (lift : Y ⟶ H.obj Z) (m : H.obj Z ⟶ Opposite.unop X) (fac : lift ≫ m = g),
  Sieve.pullback g (equalizerSieve (FD := FA) (CD := CA) a b) ∈ (K : (a : D) → Set (Sieve a)) Y
Tactic: ⟨⟨Z, lift, m, fac⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Sieve.pullback g (equalizerSieve (FD := FA) (CD := CA) a b) ∈ (K : (a : D) → Set (Sieve a)) Y
have h₁ : Sieve.pullback lift (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b)) ∈ (K : (a : D) → Set (Sieve a)) Y
Tactic: rw [← fac, Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Sieve.pullback lift (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b)) ∈ (K : (a : D) → Set (Sieve a)) Y
have h₁ : Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
  (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b))
Tactic: apply K.pullback_stable
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
    (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b))
have h₁ : Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
  (Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b))))
Tactic: refine K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
    (Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b))))
have h₁ : equalizerSieve.{u_5, v_3, v_1, u_3, u_1, u_4} (FD := FA) (CD := CA) (F := H.op ⋙ F)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
        (a : CA (F.obj (Opposite.op (Opposite.unop X)))) → CA (F.obj (Opposite.op (H.obj Z))))
      a)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
        (a : CA (F.obj (Opposite.op (Opposite.unop X)))) → CA (F.obj (Opposite.op (H.obj Z))))
      b) ≤
  Sieve.functorPullback H (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b))
Tactic: refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_)
      (hH.cover_preserve <| equalizerSieve_mem J (whiskerLeft H.op f)
        (F.map m.op a) (F.map m.op b) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
h₁ :
  equalizerSieve.{u_5, v_3, v_1, u_3, u_1, u_4} (FD := FA) (CD := CA) (F := H.op ⋙ F)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
          (a : CA (F.obj (Opposite.op (Opposite.unop X)))) → CA (F.obj (Opposite.op (H.obj Z))))
        a)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
          (a : CA (F.obj (Opposite.op (Opposite.unop X)))) → CA (F.obj (Opposite.op (H.obj Z))))
        b) ≤
    Sieve.functorPullback H (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
    (Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b))))
have h₂ : Eq (α := CA ((H.op ⋙ G).obj (Opposite.op Z)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op.whiskerLeft f).app (Opposite.op Z)) :
        (a : CA ((H.op ⋙ F).obj (Opposite.op Z))) → CA ((H.op ⋙ G).obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
            (a : CA (F.obj (Opposite.op (Opposite.unop X)))) → CA (F.obj (Opposite.op (H.obj Z))))
          a :
        CA (F.obj (Opposite.op (H.obj Z)))) :
    CA ((H.op ⋙ G).obj (Opposite.op Z)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op.whiskerLeft f).app (Opposite.op Z)) :
        (a : CA ((H.op ⋙ F).obj (Opposite.op Z))) → CA ((H.op ⋙ G).obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
            (a : CA (F.obj (Opposite.op (Opposite.unop X)))) → CA (F.obj (Opposite.op (H.obj Z))))
          b :
        CA (F.obj (Opposite.op (H.obj Z)))) :
    CA ((H.op ⋙ G).obj (Opposite.op Z)))
Tactic: refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_)
      (hH.cover_preserve <| equalizerSieve_mem J (whiskerLeft H.op f)
        (F.map m.op a) (F.map m.op b) ?_)