awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC_1 : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC_1 X) (CC_1 Y)
CC : C → Type v
inst_3 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_5 : HasLimits.{v, u} C
inst_6 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_7 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
x : (↑X : Type v)
⊢ PreservesMonomorphisms (C := Sheaf C X) (Sheaf.forget C X ⋙ stalkFunctor C x)

Tactic:
⟨@fun _𝓐 _𝓑 f _ =>
    ConcreteCategory.mono_of_injective _ <|
      (app_injective_iff_stalkFunctor_map_injective f.1).mpr
        (fun c =>
          (ConcreteCategory.mono_iff_injective_of_preservesPullback (f.1.app (op c))).mp
            ((NatTrans.mono_iff_mono_app f.1).mp
                (CategoryTheory.presheaf_mono_of_mono ..) <|
              op c))
        x⟩

Premises used: Iff.mpr, CategoryTheory.Functor.comp, CategoryTheory.presheaf_mono_of_mono, Opens.grothendieckTopology, CategoryTheory.Functor.PreservesMonomorphisms.mk, CategoryTheory.Functor.map, CategoryTheory.NatTrans.mono_iff_mono_app, TopCat.carrier, Opposite.op, CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback, Iff.mp, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.ConcreteCategory.mono_of_injective, TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective, TopCat.Presheaf.stalkFunctor, TopCat.Sheaf.forget, CategoryTheory.NatTrans.app
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
inst_7 : Mono f
⊢ ∀ (x : (↑X : Type v)),
    Mono (X :=
      obj (stalkFunctor C x) (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C x) f.hom)

Tactic:
fun x => Functor.map_mono (Sheaf.forget.{v} C X ⋙ stalkFunctor C x) f

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.map_mono, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map, TopCat.Presheaf.stalkFunctor, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
inst_7 :
  ∀ (x : (↑X : Type v)),
    Mono (X :=
      obj (stalkFunctor C x) (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C x) f.hom)
⊢ Mono f

Tactic:
(Sheaf.Hom.mono_iff_presheaf_mono _ _ _).mpr <|
    (NatTrans.mono_iff_mono_app _).mpr fun U =>
      (ConcreteCategory.mono_iff_injective_of_preservesPullback _).mpr <|
        app_injective_of_stalkFunctor_map_injective f.1 U.unop fun _x _hx =>
          (ConcreteCategory.mono_iff_injective_of_preservesPullback
            ((stalkFunctor C _).map f.hom)).mp <| inferInstance

Premises used: Iff.mpr, inferInstance, CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono, TopCat.Sheaf, CategoryTheory.Functor.map, CategoryTheory.NatTrans.mono_iff_mono_app, TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective, CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback, Iff.mp, CategoryTheory.InducedCategory.Hom.hom, Opposite.unop, TopCat.Presheaf.stalkFunctor, CategoryTheory.NatTrans.app
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
⊢ Mono f ↔
    ∀ (x : (↑X : Type v)),
      Mono (X :=
        obj (stalkFunctor C x)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
        (map (stalkFunctor C x) f.hom)

Tactic:
⟨fun _ => stalk_mono_of_mono _, fun _ => mono_of_stalk_mono _⟩

Premises used: TopCat.Presheaf.mono_of_stalk_mono, TopCat.Presheaf.stalk_mono_of_mono, Iff.intro
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
h :
  ∀ x ∈ U,
    Function.Bijective.{v + 1, v + 1} (α :=
      CC
        (obj (stalkFunctor C x)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (β :=
      CC
        (obj (stalkFunctor C x)
          (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f.hom)) :
        (a : CC ((stalkFunctor C x).obj F.obj)) → CC ((stalkFunctor C x).obj G.obj))
⊢ Function.Surjective.{v + 1, v + 1} (α :=
    CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))) (β :=
    CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op U))) :
      (a : CC (F.obj.obj (op U))) → CC (G.obj.obj (op U)))

Tactic:
app_surjective_of_injective_of_locally_surjective f U (And.left <| h · ·) fun t x hx => ?_

Premises used: TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective, And.left
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
h :
  ∀ x ∈ U,
    Function.Bijective.{v + 1, v + 1} (α :=
      CC
        (obj (stalkFunctor C x)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (β :=
      CC
        (obj (stalkFunctor C x)
          (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f.hom)) :
        (a : CC ((stalkFunctor C x).obj F.obj)) → CC ((stalkFunctor C x).obj G.obj))
refine :
  ∀ (t : CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (x : (↑X : Type v)) (hx : x ∈ U),
    ∃ (V : Opens (↑X : Type v)) (_ : x ∈ V) (iVU : V ⟶ U) (s :
      ToType (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V))),
      Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op V)) :
              (a : CC (F.obj.obj (op V))) → CC (G.obj.obj (op V)))
            s :
          CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC)
                (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map iVU.op) :
              (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op V)))
            t :
          CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V)))
⊢ Function.Surjective.{v + 1, v + 1} (α :=
    CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))) (β :=
    CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op U))) :
      (a : CC (F.obj.obj (op U))) → CC (G.obj.obj (op U)))

Tactic:
refine app_surjective_of_injective_of_locally_surjective f U (And.left <| h · ·) fun t x hx => ?_

Premises used: TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective, And.left
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
h :
  ∀ x ∈ U,
    Function.Bijective.{v + 1, v + 1} (α :=
      CC
        (obj (stalkFunctor C x)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (β :=
      CC
        (obj (stalkFunctor C x)
          (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f.hom)) :
        (a : CC ((stalkFunctor C x).obj F.obj)) → CC ((stalkFunctor C x).obj G.obj))
⊢ Function.Bijective.{v + 1, v + 1} (α :=
    CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))) (β :=
    CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op U))) :
      (a : CC (F.obj.obj (op U))) → CC (G.obj.obj (op U)))

Tactic:
⟨app_injective_of_stalkFunctor_map_injective f.1 U fun x hx => (h x hx).1,
    app_surjective_of_stalkFunctor_map_bijective f U h⟩

Premises used: TopCat.Presheaf.app_surjective_of_stalkFunctor_map_bijective, TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective, And.left, And.intro, Function.Bijective, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
this :
  IsIso (X :=
    obj (forget C (FC := FC) (CC := CC))
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))
⊢ IsIso (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
    (f.hom.app (op U))

Tactic:
isIso_of_reflects_iso (f.1.app (op U)) (forget C)

Premises used: CategoryTheory.isIso_of_reflects_iso, Opposite.op, CategoryTheory.forget, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
this :
  IsIso (X :=
    obj (forget C (FC := FC) (CC := CC))
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))
⊢ IsIso (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
    (f.hom.app (op U))

Tactic:
exact isIso_of_reflects_iso (f.1.app (op U)) (forget C)

Premises used: CategoryTheory.isIso_of_reflects_iso, Opposite.op, CategoryTheory.forget, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
suffices :
  IsIso (X :=
    obj (forget C (FC := FC) (CC := CC))
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))
⊢ IsIso (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
    (f.hom.app (op U))

Tactic:
suffices IsIso ((forget C).map (f.1.app (op U))) by
    exact isIso_of_reflects_iso (f.1.app (op U)) (forget C)
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
rw :
  Function.Bijective (α :=
    (fun (X : Type v) ↦ X)
      (obj (forget C (FC := FC) (CC := CC))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))))
    (β :=
    (fun (X : Type v) ↦ X)
      (obj (forget C (FC := FC) (CC := CC))
        (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))) :
      (a : (fun (X : Type v) ↦ X) ((forget C).obj (F.obj.obj (op U)))) →
        (fun (X : Type v) ↦ X) ((forget C).obj (G.obj.obj (op U))))
⊢ IsIso (X :=
    obj (forget C (FC := FC) (CC := CC))
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))

Tactic:
rw [isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
h :
  ∀ x ∈ U,
    Function.Bijective.{v + 1, v + 1} (α :=
      obj (forget C (FC := FC) (CC := CC))
        (obj (stalkFunctor C x)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (β :=
      obj (forget C (FC := FC) (CC := CC))
        (obj (stalkFunctor C x)
          (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := obj (forget C (FC := FC) (CC := CC))) (map (stalkFunctor C x) f.hom)) :
        (a : (forget C).obj ((stalkFunctor C x).obj F.obj)) → (forget C).obj ((stalkFunctor C x).obj G.obj))
⊢ Function.Bijective (α :=
    (fun (X : Type v) ↦ X)
      (obj (forget C (FC := FC) (CC := CC))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))))
    (β :=
    (fun (X : Type v) ↦ X)
      (obj (forget C (FC := FC) (CC := CC))
        (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))) :
      (a : (fun (X : Type v) ↦ X) ((forget C).obj (F.obj.obj (op U)))) →
        (fun (X : Type v) ↦ X) ((forget C).obj (G.obj.obj (op U))))

Tactic:
apply app_bijective_of_stalkFunctor_map_bijective

Premises used: TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
x : (↑X : Type v)
hx : x ∈ U
h :
  IsIso.{v, v + 1} (X :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (Y :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := obj (forget C (FC := FC) (CC := CC))) (map (stalkFunctor C x) f.hom)) :
        (a : (forget C).obj ((stalkFunctor C x).obj F.obj)) → (forget C).obj ((stalkFunctor C x).obj G.obj)))
⊢ Function.Bijective.{v + 1, v + 1} (α :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (β :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (⇑(ConcreteCategory.hom (FC := FC) (CC := obj (forget C (FC := FC) (CC := CC))) (map (stalkFunctor C x) f.hom)) :
      (a : (forget C).obj ((stalkFunctor C x).obj F.obj)) → (forget C).obj ((stalkFunctor C x).obj G.obj))

Tactic:
apply (bijective_iff_isIso_ofHom _).mpr

Premises used: Iff.mpr, CategoryTheory.bijective_iff_isIso_ofHom
-- Module: Mathlib.Topology.Sheaves.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
x : (↑X : Type v)
hx : x ∈ U
⊢ IsIso.{v, v + 1} (X :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (Y :=
    obj (forget C (FC := FC) (CC := CC))
      (obj (stalkFunctor C x)
        (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
    (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := obj (forget C (FC := FC) (CC := CC))) (map (stalkFunctor C x) f.hom)) :
        (a : (forget C).obj ((stalkFunctor C x).obj F.obj)) → (forget C).obj ((stalkFunctor C x).obj G.obj)))

Tactic:
Functor.map_isIso (forget C) ((stalkFunctor C (⟨x, hx⟩ : U).1).map f.1)

Premises used: CategoryTheory.Functor.map, Subtype.mk, CategoryTheory.forget, CategoryTheory.Functor.map_isIso, CategoryTheory.InducedCategory.Hom.hom, Subtype.val, TopCat.Presheaf.stalkFunctor