awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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₁ : Sieve.pullback lift (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b)) ∈ (K : (a : D) → Set (Sieve a)) Y
⊢ Sieve.pullback g (equalizerSieve (FD := FA) (CD := CA) a b) ∈ (K : (a : D) → Set (Sieve a)) Y

Tactic:
rw [← fac, Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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₁ :
  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))
⊢ Sieve.pullback lift (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b)) ∈ (K : (a : D) → Set (Sieve a)) Y

Tactic:
apply K.pullback_stable

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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))

Tactic:
K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Sieve.functorPullback_pushforward_le
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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₁ :
  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))))
⊢ 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:
refine K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Sieve.functorPullback_pushforward_le
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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))))

Tactic:
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) ?_)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Functor.op, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Sieve.functorPushforward_monotone, CategoryTheory.Functor.map, CategoryTheory.Presheaf.equalizerSieve_mem, CategoryTheory.CoverPreserving.cover_preserve, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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
W : C
q : W ⟶ Z
hq :
  Sieve.arrows
    (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))
    q
⊢ (Sieve.functorPullback H (Sieve.pullback m (equalizerSieve (FD := FA) (CD := CA) a b))).arrows q

Tactic:
simpa using hq
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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₁ :
  Eq (α := CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
          (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
              (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
            a :
          CA (F.obj (Opposite.op (H.obj Z)))) :
      CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
          (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
              (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
            b :
          CA (F.obj (Opposite.op (H.obj Z)))) :
      CA (G.obj (Opposite.op (H.obj Z))))
⊢ 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:
simp only [comp_obj, op_obj, whiskerLeft_app, Opposite.op_unop]

Premises used: CategoryTheory.Functor.comp_obj, Opposite.op_unop, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.op_obj
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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.IsCocontinuous J K
inst_6 : H.IsCoverDense K
⊢ IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f) ↔ IsLocallyInjective (FD := FA) (CD := CA) K f

Tactic:
⟨fun _ ↦ isLocallyInjective_of_whisker J K H f hH,
    fun _ ↦ isLocallyInjective_whisker J K H f⟩

Premises used: CategoryTheory.Presheaf.isLocallyInjective_of_whisker, CategoryTheory.Presheaf.isLocallyInjective_whisker, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
h :
  ∀ ⦃Y : D⦄ ⦃f_1 : Y ⟶ X⦄,
    (Sieve.coverByImage H X).arrows f_1 →
      Sieve.pullback f_1 (imageSieve (FA := FA) (CA := CA) f a) ∈ (K : (a : D) → Set (Sieve a)) Y
⊢ imageSieve (FA := FA) (CA := CA) f a ∈ (K : (a : D) → Set (Sieve a)) X

Tactic:
apply K.transitive (H.is_cover_of_isCoverDense K X)

Premises used: CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.Functor.is_cover_of_isCoverDense
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
h :
  ∀ (Z : C) (lift : Y ⟶ H.obj Z) (m : H.obj Z ⟶ X) (fac : lift ≫ m = g),
    Sieve.pullback g (imageSieve (FA := FA) (CA := CA) f a) ∈ (K : (a : D) → Set (Sieve a)) Y
⊢ (Sieve.coverByImage H X).arrows g →
    Sieve.pullback g (imageSieve (FA := FA) (CA := CA) f a) ∈ (K : (a : D) → Set (Sieve a)) Y

Tactic:
⟨⟨Z, lift, m, fac⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
h : Sieve.pullback lift (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a)) ∈ (K : (a : D) → Set (Sieve a)) Y
⊢ Sieve.pullback g (imageSieve (FA := FA) (CA := CA) f a) ∈ (K : (a : D) → Set (Sieve a)) Y

Tactic:
rw [← fac, Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
h :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
    (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))
⊢ Sieve.pullback lift (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a)) ∈ (K : (a : D) → Set (Sieve a)) Y

Tactic:
apply K.pullback_stable

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj (Opposite.unop (Opposite.op Z)))))
    ((K : (a : D) → Set (Sieve a)) (H.obj (Opposite.unop (Opposite.op Z))))
    (Sieve.functorPushforward H
      (imageSieve (FA := FA) (CA := CA) (H.op.whiskerLeft f)
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
            (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
          a)))

Tactic:
have hh := hH.cover_preserve <| imageSieve_mem J (whiskerLeft H.op f) (G.map m.op a)
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj (Opposite.unop (Opposite.op Z)))))
    ((K : (a : D) → Set (Sieve a)) (H.obj (Opposite.unop (Opposite.op Z))))
    (Sieve.functorPushforward H
      (imageSieve (FA := FA) (CA := CA) (H.op.whiskerLeft f)
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
            (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
          a)))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
    (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))

Tactic:
K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Sieve.functorPullback_pushforward_le
-- Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
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 : IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f)
X : D
a : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj (Opposite.unop (Opposite.op Z)))))
    ((K : (a : D) → Set (Sieve a)) (H.obj (Opposite.unop (Opposite.op Z))))
    (Sieve.functorPushforward H
      (imageSieve (FA := FA) (CA := CA) (H.op.whiskerLeft f)
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) :
            (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj Z))))
          a)))
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 (imageSieve (FA := FA) (CA := CA) f a))))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (H.obj Z))) ((K : (a : D) → Set (Sieve a)) (H.obj Z))
    (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))

Tactic:
refine K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Sieve.functorPullback_pushforward_le