awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
h :
  Presheaf.IsSheaf J P →
    Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) P
h₁ :
  Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) P →
    Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf J P ↔
    Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) P

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
⊢ Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) P

Tactic:
⟨⟨P, hP⟩, rfl⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
⊢ Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) P

Tactic:
exact ⟨⟨P, hP⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
F : Sheaf.{v_1, v_2, u_1, u_2} J A
⊢ Presheaf.IsSheaf J (Functor.obj (sheafToPresheaf J A) F)

Tactic:
F.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
F : Sheaf.{v_1, v_2, u_1, u_2} J A
⊢ Presheaf.IsSheaf J (Functor.obj (sheafToPresheaf J A) F)

Tactic:
exact F.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
F₁ F₂ : Sheaf.{v_1, v_2, u_1, u_2} J A
φ : F₁ ⟶ F₂
rw :
  ObjectProperty.isLocal fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) x
      (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔
    IsIso φ
rw₁ : IsIso (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔ IsIso φ
rw₂ rw₃ : IsIso φ ↔ IsIso φ
⊢ J.W (X := Functor.obj (sheafToPresheaf J A) F₁) (Functor.map (sheafToPresheaf J A) φ) ↔ IsIso φ

Tactic:
rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩, isIso_iff_of_reflects_iso]

Premises used: CategoryTheory.ObjectProperty.isLocal_iff_isIso, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
rw :
  ObjectProperty.isLocal
    (fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) x)
    (adj.unit.app P)
⊢ J.W (adj.unit.app P)

Tactic:
rw [W_eq_isLocal_range_sheafToPresheaf_obj]

Premises used: CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
⊢ ObjectProperty.isLocal
    (fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) x)
    (adj.unit.app P)

Tactic:
ObjectProperty.isLocal_adj_unit_app adj P

Premises used: Set.Mem, CategoryTheory.ObjectProperty.isLocal_adj_unit_app
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
⊢ ObjectProperty.isLocal
    (fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A))) x)
    (adj.unit.app P)

Tactic:
exact ObjectProperty.isLocal_adj_unit_app adj P

Premises used: CategoryTheory.ObjectProperty.isLocal_adj_unit_app
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
f : P₁ ⟶ P₂
rw :
  ObjectProperty.isLocal
      (fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A)))
          x)
      f ↔
    IsIso (G.map f)
⊢ J.W f ↔ IsIso (G.map f)

Tactic:
rw [W_eq_isLocal_range_sheafToPresheaf_obj]

Premises used: CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
f : P₁ ⟶ P₂
⊢ ObjectProperty.isLocal
      (fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A)))
          x)
      f ↔
    IsIso (G.map f)

Tactic:
ObjectProperty.isLocal_iff_isIso_map adj f

Premises used: Set.Mem, CategoryTheory.ObjectProperty.isLocal_iff_isIso_map
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
f : P₁ ⟶ P₂
⊢ ObjectProperty.isLocal
      (fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A)))
          x)
      f ↔
    IsIso (G.map f)

Tactic:
exact ObjectProperty.isLocal_iff_isIso_map adj f

Premises used: CategoryTheory.ObjectProperty.isLocal_iff_isIso_map
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A ⥤ Sheaf.{v_1, v_2, u_1, u_2} J A
adj : G ⊣ sheafToPresheaf J A
rw :
  (ObjectProperty.isLocal fun (x : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) (Set.range (Functor.obj (sheafToPresheaf J A)))
        x) =
    MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G
rw₁ rw₂ :
  MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G =
    MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G
⊢ J.W = MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A)) G

Tactic:
rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_eq_inverseImage_isomorphisms adj]

Premises used: CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj, CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J A
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
⊢ J.W (Y := sheafify J P) (toSheafify J P)

Tactic:
J.W_adj_unit_app (sheafificationAdjunction J A) P

Premises used: CategoryTheory.GrothendieckTopology.W_adj_unit_app, CategoryTheory.sheafificationAdjunction
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J A
P₁ P₂ : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
f : P₁ ⟶ P₂
⊢ J.W f ↔ IsIso (X := Functor.obj (presheafToSheaf J A) P₁) (Functor.map (presheafToSheaf J A) f)

Tactic:
J.W_iff_isIso_map_of_adjunction (sheafificationAdjunction J A) f

Premises used: CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction, CategoryTheory.sheafificationAdjunction
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J A
⊢ Eq (α := MorphismProperty (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A)) J.W
    (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A))
      (presheafToSheaf J A))

Tactic:
J.W_eq_inverseImage_isomorphisms_of_adjunction (sheafificationAdjunction J A)

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms_of_adjunction
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J A
rw :
  Functor.IsLocalization (C := Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) (presheafToSheaf J A)
    (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A))
      (presheafToSheaf J A))
⊢ Functor.IsLocalization (C := Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) (presheafToSheaf J A) J.W

Tactic:
rw [W_eq_inverseImage_isomorphisms]

Premises used: CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J A
⊢ Functor.IsLocalization (C := Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) (presheafToSheaf J A)
    (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A))
      (presheafToSheaf J A))

Tactic:
(sheafificationAdjunction J A).isLocalization

Premises used: CategoryTheory.Adjunction.isLocalization, CategoryTheory.sheafificationAdjunction
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J A
⊢ Functor.IsLocalization (C := Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A) (presheafToSheaf J A)
    (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (Sheaf.{v_1, v_2, u_1, u_2} J A))
      (presheafToSheaf J A))

Tactic:
exact (sheafificationAdjunction J A).isLocalization

Premises used: CategoryTheory.Adjunction.isLocalization, CategoryTheory.sheafificationAdjunction
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
Z : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hZ : Presheaf.IsSheaf J Z
⊢ Presieve.IsSheaf J Z

Tactic:
rw [isSheaf_iff_isSheaf_of_type] at hZ

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
Z : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hZ : Presieve.IsSheaf J Z
rw : Presieve.IsSheafFor Z S.arrows
⊢ Function.Bijective (β :=
    Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v_1, u_1} X) (shrinkFunctor.{w, v_1, u_1} S) ⟶ Z)
    fun (g : Functor.obj shrinkYoneda.{w, v_1, u_1} X ⟶ Z) ↦ Subfunctor.ι (shrinkFunctor.{w, v_1, u_1} S) ≫ g

Tactic:
rw [← Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
Z : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hZ : Presieve.IsSheaf J Z
⊢ Presieve.IsSheafFor Z S.arrows

Tactic:
hZ _ hS
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
Z : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hZ : Presieve.IsSheaf J Z
⊢ Presieve.IsSheafFor Z S.arrows

Tactic:
exact hZ _ hS
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_3
inst_1 : Category.{v_3, u_3} D
K : GrothendieckTopology.{v_3, u_3} D
inst_2 : LocallySmall.{w, v_1, u_1} C
F : Functor.{v_1, v_3, u_1, u_3} C D
H : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w) ⥤ Functor.{v_3, w, u_3, w + 1} Dᵒᵖ (Type w)
adj : H ⊣ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)) F.op
h :
  ∀ ⦃X : C⦄ ⦃S : Sieve.{v_1, u_1} X⦄,
    S ∈ (J : (a : C) → Set (Sieve a)) X →
      K.W (X :=
        H.obj
          (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v_1, u_1} X) (Sieve.shrinkFunctor.{w, v_1, u_1} S)))
        (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{w, v_1, u_1} S)))
G : Functor.{v_3, w, u_3, w + 1} Dᵒᵖ (Type w)
hG : IsSheaf K G
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
rw :
  Function.Bijective (β :=
    H.obj (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v_1, u_1} X) (Sieve.shrinkFunctor.{w, v_1, u_1} S)) ⟶
      G)
    fun (g : H.obj (Functor.obj shrinkYoneda.{w, v_1, u_1} X) ⟶ G) ↦
    H.map (Subfunctor.ι (Sieve.shrinkFunctor.{w, v_1, u_1} S)) ≫ g
⊢ IsSheafFor (F.op ⋙ G) S.arrows

Tactic:
rw [Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp, ← Functor.whiskeringLeft_obj_obj,
    ← adj.map_comp_bijective_iff]

Premises used: CategoryTheory.Adjunction.map_comp_bijective_iff, CategoryTheory.Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp, CategoryTheory.Functor.whiskeringLeft_obj_obj
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_3
inst_1 : Category.{v_3, u_3} D
K : GrothendieckTopology.{v_3, u_3} D
inst_2 : LocallySmall.{w, v_1, u_1} C
F : Functor.{v_1, v_3, u_1, u_3} C D
H : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w) ⥤ Functor.{v_3, w, u_3, w + 1} Dᵒᵖ (Type w)
adj : H ⊣ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)) F.op
h :
  ∀ ⦃X : C⦄ ⦃S : Sieve.{v_1, u_1} X⦄,
    S ∈ (J : (a : C) → Set (Sieve a)) X →
      K.W (X :=
        H.obj
          (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v_1, u_1} X) (Sieve.shrinkFunctor.{w, v_1, u_1} S)))
        (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{w, v_1, u_1} S)))
G : Functor.{v_3, w, u_3, w + 1} Dᵒᵖ (Type w)
hG : IsSheaf K G
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Function.Bijective (β :=
    H.obj (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v_1, u_1} X) (Sieve.shrinkFunctor.{w, v_1, u_1} S)) ⟶
      G)
    fun (g : H.obj (Functor.obj shrinkYoneda.{w, v_1, u_1} X) ⟶ G) ↦
    H.map (Subfunctor.ι (Sieve.shrinkFunctor.{w, v_1, u_1} S)) ≫ g

Tactic:
h hS _ ?_
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_3
inst_1 : Category.{v_3, u_3} D
K : GrothendieckTopology.{v_3, u_3} D
inst_2 : LocallySmall.{w, v_1, u_1} C
F : Functor.{v_1, v_3, u_1, u_3} C D
H : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w) ⥤ Functor.{v_3, w, u_3, w + 1} Dᵒᵖ (Type w)
adj : H ⊣ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)) F.op
h :
  ∀ ⦃X : C⦄ ⦃S : Sieve.{v_1, u_1} X⦄,
    S ∈ (J : (a : C) → Set (Sieve a)) X →
      K.W (X :=
        H.obj
          (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v_1, u_1} X) (Sieve.shrinkFunctor.{w, v_1, u_1} S)))
        (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{w, v_1, u_1} S)))
G : Functor.{v_3, w, u_3, w + 1} Dᵒᵖ (Type w)
hG : IsSheaf K G
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
refine : Presheaf.IsSheaf K G
⊢ Function.Bijective (β :=
    H.obj (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v_1, u_1} X) (Sieve.shrinkFunctor.{w, v_1, u_1} S)) ⟶
      G)
    fun (g : H.obj (Functor.obj shrinkYoneda.{w, v_1, u_1} X) ⟶ G) ↦
    H.map (Subfunctor.ι (Sieve.shrinkFunctor.{w, v_1, u_1} S)) ≫ g

Tactic:
refine h hS _ ?_
-- Module: Mathlib.CategoryTheory.Sites.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_3
inst_1 : Category.{v_3, u_3} D
K : GrothendieckTopology.{v_3, u_3} D
inst_2 : LocallySmall.{w, v_1, u_1} C
F : Functor.{v_1, v_3, u_1, u_3} C D
H : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w) ⥤ Functor.{v_3, w, u_3, w + 1} Dᵒᵖ (Type w)
adj : H ⊣ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)) F.op
h :
  ∀ ⦃X : C⦄ ⦃S : Sieve.{v_1, u_1} X⦄,
    S ∈ (J : (a : C) → Set (Sieve a)) X →
      K.W (X :=
        H.obj
          (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v_1, u_1} X) (Sieve.shrinkFunctor.{w, v_1, u_1} S)))
        (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{w, v_1, u_1} S)))
G : Functor.{v_3, w, u_3, w + 1} Dᵒᵖ (Type w)
hG : IsSheaf K G
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
rwa rwa₁ rwa₂ rwa₃ : IsSheaf K G
⊢ Presheaf.IsSheaf K G

Tactic:
rwa [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
mp : IsLocallyInjective (FD := TypeCat.Fun) f ∧ IsLocallySurjective (FA := TypeCat.Fun) f → IsIso f
mpr : IsIso f → IsLocallyInjective (FD := TypeCat.Fun) f ∧ IsLocallySurjective (FA := TypeCat.Fun) f
⊢ IsLocallyInjective (FD := TypeCat.Fun) f ∧ IsLocallySurjective (FA := TypeCat.Fun) f ↔ IsIso f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : IsLocallyInjective (FD := TypeCat.Fun) f
right : IsLocallySurjective (FA := TypeCat.Fun) f
⊢ ∀ (X : Cᵒᵖ),
    Function.Injective (α := F.obj (P := Presheaf.IsSheaf J).obj X) (β := G.obj (P := Presheaf.IsSheaf J).obj X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)) : (a : F.obj.obj X) → G.obj.obj X)

Tactic:
rw [isLocallyInjective_iff_injective] at h₁

Premises used: CategoryTheory.Sheaf.isLocallyInjective_iff_injective
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : IsLocallyInjective (FD := TypeCat.Fun) f
right : IsLocallySurjective (FA := TypeCat.Fun) f
h₂ :
  ∀ (X : Cᵒᵖ),
    Function.Injective (α := F.obj (P := Presheaf.IsSheaf J).obj X) (β := G.obj (P := Presheaf.IsSheaf J).obj X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)) : (a : F.obj.obj X) → G.obj.obj X)
⊢ IsLocallySurjective (FA := TypeCat.Fun) f

Tactic:
rw [isLocallyInjective_iff_injective] at h₁

Premises used: CategoryTheory.Sheaf.isLocallyInjective_iff_injective
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ :
  ∀ (X : Cᵒᵖ),
    Function.Injective (α := F.obj (P := Presheaf.IsSheaf J).obj X) (β := G.obj (P := Presheaf.IsSheaf J).obj X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)) : (a : F.obj.obj X) → G.obj.obj X)
right : IsLocallySurjective (FA := TypeCat.Fun) f
this :
  ∀ (X : Cᵒᵖ),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj X)) (β :=
      (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj X))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)) :
        (a : (fun (X : Type w) ↦ X) (F.obj.obj X)) → (fun (X : Type w) ↦ X) (G.obj.obj X))
rw :
  ∀ (X : Cᵒᵖ),
    IsIso (X := (Functor.obj (sheafToPresheaf J (Type w)) F).obj X)
      (NatTrans.app (Functor.map (sheafToPresheaf J (Type w)) f) X)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _), NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ :
  ∀ (X : Cᵒᵖ),
    Function.Injective (α := F.obj (P := Presheaf.IsSheaf J).obj X) (β := G.obj (P := Presheaf.IsSheaf J).obj X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)) : (a : F.obj.obj X) → G.obj.obj X)
right : IsLocallySurjective (FA := TypeCat.Fun) f
this :
  ∀ (X : Cᵒᵖ),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj X)) (β :=
      (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj X))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)) :
        (a : (fun (X : Type w) ↦ X) (F.obj.obj X)) → (fun (X : Type w) ↦ X) (G.obj.obj X))
X : Cᵒᵖ
rw :
  Function.Bijective (α := (fun (X : Type w) ↦ X) ((Functor.obj (sheafToPresheaf J (Type w)) F).obj X)) (β :=
    (fun (X : Type w) ↦ X) ((Functor.obj (sheafToPresheaf J (Type w)) G).obj X))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map (sheafToPresheaf J (Type w)) f) X)) :
      (a : (fun (X : Type w) ↦ X) (((sheafToPresheaf J (Type w)).obj F).obj X)) →
        (fun (X : Type w) ↦ X) (((sheafToPresheaf J (Type w)).obj G).obj X))
⊢ IsIso (X := (Functor.obj (sheafToPresheaf J (Type w)) F).obj X)
    (NatTrans.app (Functor.map (sheafToPresheaf J (Type w)) f) X)

Tactic:
rw [isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective