awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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ᵒᵖ
⊢ 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))

Tactic:
⟨h₁ X, this X⟩

Premises used: And.intro, Function.Bijective
-- 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ᵒᵖ
⊢ 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))

Tactic:
exact ⟨h₁ X, this X⟩
-- 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
mp :
  ∀ (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))
⊢ IsIso f

Tactic:
suffices ∀ (X : Cᵒᵖ), Function.Surjective (f.hom.app X) by
      rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _), NatTrans.isIso_iff_isIso_app]
      intro X
      rw [isIso_iff_bijective]
      exact ⟨h₁ X, this X⟩
-- 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
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
⊢ Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows

Tactic:
have H := (isSheaf_iff_isSheaf_of_type J F.obj).1 F.property _
      (Presheaf.imageSieve_mem J f.hom s)
-- 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
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
a :
  Eq (α := G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op W)) :
          (a : F.obj.obj (Opposite.op W)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₁.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op Y₁))) →
                (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op W)))
            (t f₁ hf₁) :
          (fun (X : Type w) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op W)) :
          (a : F.obj.obj (Opposite.op W)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₂.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op Y₂))) →
                (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op W)))
            (t f₂ hf₂) :
          (fun (X : Type w) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op Y₁))) →
            (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op W)))
        (t f₁ hf₁) :
      (fun (X : Type w) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op Y₂))) →
            (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op W)))
        (t f₂ hf₂) :
      (fun (X : Type w) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)))

Tactic:
apply h₁
-- 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
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op W)) :
          (a : F.obj.obj (Opposite.op W)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₁.op) :
              (a : F.obj.obj (Opposite.op Y₁)) → F.obj.obj (Opposite.op W))
            (t f₁ hf₁) :
          F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g₁.op) :
          (a : G.obj.obj (Opposite.op Y₁)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op Y₁)) :
              (a : F.obj.obj (Opposite.op Y₁)) → G.obj.obj (Opposite.op Y₁))
            (t f₁ hf₁) :
          G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y₁)) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))

Tactic:
have eq₁ := NatTrans.naturality_apply f.hom g₁.op (t f₁ hf₁)
-- 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
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
⊢ t.Compatible (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows)

Tactic:
have ht : t.Compatible := by
      intro Y₁ Y₂ W g₁ g₂ f₁ f₂ hf₁ hf₂ w
      apply h₁
      have eq₁ := NatTrans.naturality_apply f.hom g₁.op (t f₁ hf₁)
      have eq₂ := NatTrans.naturality_apply f.hom g₂.op (t f₂ hf₂)
      have eq₃ := congr_arg (G.obj.map g₁.op) (Presheaf.app_localPreimage f.hom s _ hf₁)
      have eq₄ := congr_arg (G.obj.map g₂.op) (Presheaf.app_localPreimage f.hom s _ hf₂)
      refine eq₁.trans (eq₃.trans (Eq.trans ?_ (eq₄.symm.trans eq₂.symm)))
      rw [← Functor.map_comp_apply, ← Functor.map_comp_apply]
      simp only [← op_comp, w]
-- 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
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
ht : t.Compatible (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows)
⊢ ∃ (a : (fun (X : Type w) ↦ X) (F.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))
        a =
      s

Tactic:
⟨H.amalgamate t ht, ?_⟩

Premises used: CategoryTheory.Presieve.IsSheafFor.amalgamate, Exists.intro
-- 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
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
ht : t.Compatible (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows)
mp :
  (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))
      (H.amalgamate (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows) t ht) =
    s
⊢ ∃ (a : (fun (X : Type w) ↦ X) (F.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))
        a =
      s

Tactic:
refine ⟨H.amalgamate t ht, ?_⟩
-- 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
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
ht : t.Compatible (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows)
mp :
  ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ Opposite.unop X⦄,
    (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows f_1 →
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map f_1.op) :
              (a : (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op (Opposite.unop X)))) →
                (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op Y)))
            ((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))
                (H.amalgamate (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows) t ht) :
              (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj X)) :
          (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map f_1.op) :
              (a : (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op (Opposite.unop X)))) →
                (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op Y)))
            s :
          (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
⊢ (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))
      (H.amalgamate (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows) t ht) =
    s

Tactic:
apply (((isSheaf_iff_isSheaf_of_type J G.obj).1 G.property).isSeparated _
        (Presheaf.imageSieve_mem J f.hom s)).ext

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.isSheaf_iff_isSheaf_of_type, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSeparated, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Presheaf.imageSieve_mem
-- 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
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
ht : t.Compatible (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows)
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g
mp :
  Eq (α := (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op Y)) :
          (a : F.obj.obj (Opposite.op Y)) → G.obj.obj (Opposite.op Y))
        (t g hg) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g.op) :
          (a : (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op Y)))
        s :
      (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
mp₁ : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g
⊢ Eq (α := (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g.op) :
          (a : (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op Y)))
        ((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))
            (H.amalgamate (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows) t ht) :
          (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj X)) :
      (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g.op) :
          (a : (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op Y)))
        s :
      (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))

Tactic:
rw [← NatTrans.naturality_apply, H.valid_glue ht]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Presieve.IsSheafFor.valid_glue
-- 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
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
ht : t.Compatible (R := (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows)
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g
⊢ Eq (α := (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op Y)) :
          (a : F.obj.obj (Opposite.op Y)) → G.obj.obj (Opposite.op Y))
        (t g hg) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g.op) :
          (a : (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op Y)))
        s :
      (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))

Tactic:
Presheaf.app_localPreimage f.hom s g hg

Premises used: CategoryTheory.Presheaf.app_localPreimage, CategoryTheory.InducedCategory.Hom.hom
-- 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 : IsIso f
mpr : IsLocallyInjective (FD := TypeCat.Fun) f
mpr₁ : IsLocallySurjective (FA := TypeCat.Fun) f
⊢ IsLocallyInjective (FD := TypeCat.Fun) f ∧ IsLocallySurjective (FA := TypeCat.Fun) 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 : IsIso f
⊢ IsLocallyInjective (FD := TypeCat.Fun) f

Tactic:
infer_instance
-- 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 : IsIso f
⊢ IsLocallySurjective (FA := TypeCat.Fun) f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
mp : IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f → IsIso f
mpr : IsIso f → IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f
⊢ IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f ↔ IsIso f

Tactic:
constructor