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 : 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.functorPushforward H (Sieve.functorPullback H (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))))

Tactic:
K.superset_covering (Sieve.functorPushforward_monotone H _ ?_) hh

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Sieve.functorPushforward_monotone
-- 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 :
  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) ≤
    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.functorPushforward H (Sieve.functorPullback H (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))))

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

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Sieve.functorPushforward_monotone
-- 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)))
W : C
q : W ⟶ Z
h :
  ∀ (x : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) ((H.op ⋙ F).obj (Opposite.op W)))
    (h :
      Eq (α := CA ((H.op ⋙ G).obj (Opposite.op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op.whiskerLeft f).app (Opposite.op W)) :
              (a : CA ((H.op ⋙ F).obj (Opposite.op W))) → CA ((H.op ⋙ G).obj (Opposite.op W)))
            x :
          CA ((H.op ⋙ G).obj (Opposite.op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op ⋙ G).map q.op) :
              (a : CA ((H.op ⋙ G).obj (Opposite.op (Opposite.unop (Opposite.op Z))))) →
                CA ((H.op ⋙ G).obj (Opposite.op W)))
            ((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 :
              CA (G.obj (Opposite.op (H.obj Z)))) :
          CA ((H.op ⋙ G).obj (Opposite.op W)))),
    (Sieve.functorPullback H (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))).arrows q
⊢ Sieve.arrows
      (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))
      q →
    (Sieve.functorPullback H (Sieve.pullback m (imageSieve (FA := FA) (CA := CA) f a))).arrows q

Tactic:
⟨x, h⟩
-- 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)))
W : C
q : W ⟶ Z
x : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) ((H.op ⋙ F).obj (Opposite.op W))
h :
  Eq (α := CA ((H.op ⋙ G).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op.whiskerLeft f).app (Opposite.op W)) :
          (a : CA ((H.op ⋙ F).obj (Opposite.op W))) → CA ((H.op ⋙ G).obj (Opposite.op W)))
        x :
      CA ((H.op ⋙ G).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op ⋙ G).map q.op) :
          (a : CA ((H.op ⋙ G).obj (Opposite.op (Opposite.unop (Opposite.op Z))))) → CA ((H.op ⋙ G).obj (Opposite.op W)))
        ((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 :
          CA (G.obj (Opposite.op (H.obj Z)))) :
      CA ((H.op ⋙ G).obj (Opposite.op W)))
⊢ Eq (α := CA (G.obj (Opposite.op (H.obj W))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj W))) :
          (a : CA (F.obj (Opposite.op (H.obj W)))) → CA (G.obj (Opposite.op (H.obj W))))
        x :
      CA (G.obj (Opposite.op (H.obj W))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (H.map q ≫ m).op) :
          (a : CA (G.obj (Opposite.op X))) → CA (G.obj (Opposite.op (H.obj W))))
        a :
      CA (G.obj (Opposite.op (H.obj W))))

Tactic:
simpa using h
-- 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)))
W : C
q : W ⟶ Z
x : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) ((H.op ⋙ F).obj (Opposite.op W))
h :
  Eq (α := CA ((H.op ⋙ G).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op.whiskerLeft f).app (Opposite.op W)) :
          (a : CA ((H.op ⋙ F).obj (Opposite.op W))) → CA ((H.op ⋙ G).obj (Opposite.op W)))
        x :
      CA ((H.op ⋙ G).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((H.op ⋙ G).map q.op) :
          (a : CA ((H.op ⋙ G).obj (Opposite.op (Opposite.unop (Opposite.op Z))))) → CA ((H.op ⋙ G).obj (Opposite.op W)))
        ((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 :
          CA (G.obj (Opposite.op (H.obj Z)))) :
      CA ((H.op ⋙ G).obj (Opposite.op W)))
⊢ (imageSieve (FA := FA) (CA := CA) f a).arrows (H.map q ≫ m)

Tactic:
exact ⟨x, by simpa using h⟩
-- 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
⊢ IsLocallySurjective J (FA := FA) (CA := CA) (H.op.whiskerLeft f) ↔ IsLocallySurjective K (FA := FA) (CA := CA) f

Tactic:
⟨fun _ ↦ isLocallySurjective_of_whisker J K H f hH,
    fun _ ↦ isLocallySurjective_whisker J K H f⟩

Premises used: CategoryTheory.Presheaf.isLocallySurjective_whisker, CategoryTheory.Presheaf.isLocallySurjective_of_whisker, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : J.PreservesSheafification F
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ J.W (whiskerRight f F)

Tactic:
PreservesSheafification.le _ hf

Premises used: CategoryTheory.ObjectProperty.isLocal, CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.Functor.comp, CategoryTheory.GrothendieckTopology.PreservesSheafification.le, CategoryTheory.Functor.whiskerRight
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : J.PreservesSheafification F
inst_4 : HasWeakSheafify.{v, v_2, u, u_2} J B
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
rw : J.W (whiskerRight f F)
⊢ IsIso (X := obj (presheafToSheaf J B) (P₁ ⋙ F)) (map (presheafToSheaf J B) (whiskerRight f F))

Tactic:
rw [← W_iff]

Premises used: CategoryTheory.GrothendieckTopology.W_iff
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : J.PreservesSheafification F
inst_4 : HasWeakSheafify.{v, v_2, u, u_2} J B
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ J.W (whiskerRight f F)

Tactic:
J.W_of_preservesSheafification F _ hf

Premises used: CategoryTheory.GrothendieckTopology.W_of_preservesSheafification
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : J.PreservesSheafification F
inst_4 : HasWeakSheafify.{v, v_2, u, u_2} J B
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ J.W (whiskerRight f F)

Tactic:
exact J.W_of_preservesSheafification F _ hf

Premises used: CategoryTheory.GrothendieckTopology.W_of_preservesSheafification
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : HasWeakSheafify.{v, v_2, u, u_2} J B
inst_4 : HasWeakSheafify.{v, v_1, u, u_1} J A
inst_5 : J.PreservesSheafification F
rw :
  ∀ (X : Functor.{v, v_1, u, u_1} Cᵒᵖ A),
    IsIso (X := (obj (whiskeringRight Cᵒᵖ A B) F ⋙ presheafToSheaf J B).obj X) (Y :=
      (presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F).obj X)
      (NatTrans.app (toPresheafToSheafCompComposeAndSheafify J F) X)
⊢ IsIso (X := obj (whiskeringRight Cᵒᵖ A B) F ⋙ presheafToSheaf J B) (Y :=
    presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F) (toPresheafToSheafCompComposeAndSheafify J F)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : HasWeakSheafify.{v, v_2, u, u_2} J B
inst_4 : HasWeakSheafify.{v, v_1, u, u_1} J A
inst_5 : J.PreservesSheafification F
X : Functor.{v, v_1, u, u_1} Cᵒᵖ A
dsimp :
  IsIso (X := obj (presheafToSheaf J B) (X ⋙ F)) (Y :=
    obj (presheafToSheaf J B) ((obj (presheafToSheaf J A) X).obj (P := Presheaf.IsSheaf J) ⋙ F))
    (map (presheafToSheaf J B) (whiskerRight (toSheafify J X) F))
⊢ IsIso (X := (obj (whiskeringRight Cᵒᵖ A B) F ⋙ presheafToSheaf J B).obj X) (Y :=
    (presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F).obj X)
    (NatTrans.app (toPresheafToSheafCompComposeAndSheafify J F) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : HasWeakSheafify.{v, v_2, u, u_2} J B
inst_4 : HasWeakSheafify.{v, v_1, u, u_1} J A
inst_5 : J.PreservesSheafification F
X : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ IsIso (X := obj (presheafToSheaf J B) (X ⋙ F)) (Y :=
    obj (presheafToSheaf J B) ((obj (presheafToSheaf J A) X).obj (P := Presheaf.IsSheaf J) ⋙ F))
    (map (presheafToSheaf J B) (whiskerRight (toSheafify J X) F))

Tactic:
simpa only [← J.W_iff] using J.W_of_preservesSheafification F _ (J.W_toSheafify X)

Premises used: CategoryTheory.GrothendieckTopology.W_of_preservesSheafification, CategoryTheory.GrothendieckTopology.W_iff, CategoryTheory.GrothendieckTopology.W_toSheafify
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
simp : J.PreservesSheafification F ↔ ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
⊢ J.PreservesSheafification F ↔
    ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))

Tactic:
simp only [← J.W_iff_isIso_map_of_adjunction adj₂]

Premises used: CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
mp : J.PreservesSheafification F → ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
mpr : (∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)) → J.PreservesSheafification F
⊢ J.PreservesSheafification F ↔ ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : J.PreservesSheafification F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
mp : J.W (adj₁.unit.app P)
⊢ J.W (whiskerRight (adj₁.unit.app P) F)

Tactic:
apply W_of_preservesSheafification

Premises used: CategoryTheory.GrothendieckTopology.W_of_preservesSheafification
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : J.PreservesSheafification F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
mp : IsIso (G₁.map (adj₁.unit.app P))
⊢ J.W (adj₁.unit.app P)

Tactic:
rw [J.W_iff_isIso_map_of_adjunction adj₁]

Premises used: CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : J.PreservesSheafification F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ IsIso (G₁.map (adj₁.unit.app P))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
mpr : J.W ≤ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F)
⊢ J.PreservesSheafification F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ IsIso (G₁.map f)

Tactic:
rw [J.W_iff_isIso_map_of_adjunction adj₁] at hf

Premises used: CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
mpr : J.W (whiskerRight (f ≫ adj₁.unit.app P₂) F)
⊢ J.W (whiskerRight f F)

Tactic:
rw [← (W _).postcomp_iff _ _ (h P₂), ← whiskerRight_comp]

Premises used: CategoryTheory.MorphismProperty.postcomp_iff, CategoryTheory.GrothendieckTopology.W, CategoryTheory.Functor.whiskerRight_comp
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
mpr : J.W (whiskerRight (adj₁.unit.app P₁ ≫ (G₁ ⋙ sheafToPresheaf J A).map f) F)
⊢ J.W (whiskerRight (f ≫ adj₁.unit.app P₂) F)

Tactic:
erw [adj₁.unit.naturality f]

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.NatTrans.naturality