awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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) J.W
have 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))
Tactic: rw [W_eq_inverseImage_isomorphisms]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (hypothesis)
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
⊢ 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
have hZ₁ : Presieve.IsSheaf J Z
Tactic: rw [isSheaf_iff_isSheaf_of_type] at hZ
Cleared hypotheses: hZ
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
⊢ 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
have rw : Presieve.IsSheafFor Z S.arrows
Tactic: rw [← Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
⊢ IsSheafFor (F.op ⋙ G) S.arrows
have 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
Tactic: rw [Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp, ← Functor.whiskeringLeft_obj_obj,
    ← adj.map_comp_bijective_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Localization (goal)
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
have refine : Presheaf.IsSheaf K G
Tactic: refine h hS _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallyInjective (FD := TypeCat.Fun) f ∧ IsLocallySurjective (FA := TypeCat.Fun) f ↔ IsIso f
have mp : IsLocallyInjective (FD := TypeCat.Fun) f ∧ IsLocallySurjective (FA := TypeCat.Fun) f → IsIso f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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
⊢ IsLocallyInjective (FD := TypeCat.Fun) f ∧ IsLocallySurjective (FA := TypeCat.Fun) f ↔ IsIso f
have mpr : IsIso f → IsLocallyInjective (FD := TypeCat.Fun) f ∧ IsLocallySurjective (FA := TypeCat.Fun) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (hypothesis)
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
⊢ IsIso f
have 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)
Tactic: rw [isLocallyInjective_iff_injective] at h₁
Cleared hypotheses: h₁, right
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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))
⊢ IsIso f
have rw : ∀ (X : Cᵒᵖ),
  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_of_reflects_iso _ (sheafToPresheaf _ _), NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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ᵒᵖ
⊢ IsIso (X := (Functor.obj (sheafToPresheaf J (Type w)) F).obj X)
    (NatTrans.app (Functor.map (sheafToPresheaf J (Type w)) f) X)
have 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))
Tactic: rw [isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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
⊢ IsIso f
have 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))
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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (hypothesis)
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
⊢ ∃ (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
have H : 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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 (α := (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)))
have 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))
Tactic: apply h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (hypothesis)
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
⊢ ∃ (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
have ht : 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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
have 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
Tactic: refine ⟨H.amalgamate t ht, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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)
⊢ (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
have 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)))
Tactic: apply (((isSheaf_iff_isSheaf_of_type J G.obj).1 G.property).isSeparated _
        (Presheaf.imageSieve_mem J f.hom s)).ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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) (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)))
have 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)))
Tactic: rw [← NatTrans.naturality_apply, H.valid_glue ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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 ∧ IsLocallySurjective (FA := TypeCat.Fun) f
have mpr : IsLocallyInjective (FD := TypeCat.Fun) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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
⊢ IsLocallyInjective (FD := TypeCat.Fun) f ∧ IsLocallySurjective (FA := TypeCat.Fun) f
have mpr₁ : IsLocallySurjective (FA := TypeCat.Fun) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
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))
⊢ IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f ↔ IsIso f
have mp : IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f → IsIso f
Tactic: constructor