awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
inst_1 : S.X₂.IsFlasque
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
this :
  Epi (S.g.hom.app U ≫ S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i)
⊢ Epi (S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i)

Tactic:
CategoryTheory.epi_of_epi (S.g.1.app U) (S.X₃.obj.map i)

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.ShortComplex.X₃, CategoryTheory.ShortComplex.g, CategoryTheory.NatTrans.app
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
inst_1 : S.X₂.IsFlasque
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
this :
  Epi (S.g.hom.app U ≫ S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i)
⊢ Epi (S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map i)

Tactic:
exact CategoryTheory.epi_of_epi (S.g.1.app U) (S.X₃.obj.map i)

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.ShortComplex.X₃, CategoryTheory.ShortComplex.g, CategoryTheory.NatTrans.app
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
pos :
  ∀ (h1 : p₀ ∈ unop U),
    Epi (X :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        U)
      (CategoryTheory.Functor.map
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        r)
neg :
  ∀ (h1 : p₀ ∉ unop U),
    Epi (X :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        U)
      (CategoryTheory.Functor.map
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        r)
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)

Tactic:
by_cases h1 : p₀ ∈ unop U

Premises used: Opposite.unop
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
pos :
  ∀ (h2 : p₀ ∈ unop V),
    Epi (X :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        U)
      (CategoryTheory.Functor.map
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        r)
neg :
  ∀ (h2 : p₀ ∉ unop V),
    Epi (X :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        U)
      (CategoryTheory.Functor.map
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
        r)
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)

Tactic:
by_cases h2 : p₀ ∈ unop V

Premises used: Opposite.unop
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
h2 : p₀ ∈ unop V
pos : Epi.{v_1, u_1} (X := if p₀ ∈ unop U then A else terminal.{v_1, u_1} C) (eqToHom ⋯)
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)

Tactic:
simp_all only [skyscraperSheaf_obj_obj, skyscraperSheaf_obj_map, ↓reduceDIte]

Premises used: skyscraperSheaf_obj_obj, skyscraperSheaf_obj_map, reduceDIte
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
h2 : p₀ ∈ unop V
⊢ Epi.{v_1, u_1} (X := if p₀ ∈ unop U then A else terminal.{v_1, u_1} C) (eqToHom ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
h2 : p₀ ∉ unop V
neg :
  Epi.{v_1, u_1} (C := C) (X := if p₀ ∈ unop U then A else terminal.{v_1, u_1} C) (Y :=
    if p₀ ∈ unop V then A else terminal.{v_1, u_1} C)
    (if h : p₀ ∈ unop V then eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{v_1, u_1} C = x) ↦ IsTerminal.{v_1, u_1} x) terminalIsTerminal
          (if p₀ ∈ unop V then A else terminal.{v_1, u_1} C) ⋯)
        (if p₀ ∈ unop U then A else terminal.{v_1, u_1} C))
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
h2 : p₀ ∉ unop V
⊢ Epi.{v_1, u_1} (C := C) (X := if p₀ ∈ unop U then A else terminal.{v_1, u_1} C) (Y :=
    if p₀ ∈ unop V then A else terminal.{v_1, u_1} C)
    (if h : p₀ ∈ unop V then eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{v_1, u_1} C = x) ↦ IsTerminal.{v_1, u_1} x) terminalIsTerminal
          (if p₀ ∈ unop V then A else terminal.{v_1, u_1} C) ⋯)
        (if p₀ ∈ unop U then A else terminal.{v_1, u_1} C))

Tactic:
grind
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∉ unop U
⊢ p₀ ∉ unop V

Tactic:
have h2 : p₀ ∉ unop V := fun hV => h1 (r.unop.le hV)
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∉ unop U
h2 : p₀ ∉ unop V
⊢ IsIso (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)

Tactic:
have := isIso_of_isTerminal (isTerminalSkyscraperSheafObjObjOfNotMem h1)
        (isTerminalSkyscraperSheafObjObjOfNotMem h2) ((skyscraperSheaf p₀ A).obj.map r)
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)
U V : (Opens (↑X : Type v_1))ᵒᵖ
r : U ⟶ V
h1 : p₀ ∉ unop U
h2 : p₀ ∉ unop V
this :
  IsIso (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)
⊢ Epi (X :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      U)
    (CategoryTheory.Functor.map
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v_1))) (skyscraperSheaf p₀ A))
      r)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
p₀ : (↑X : Type v_1)
inst : (U : Opens (↑X : Type v_1)) → Decidable (p₀ ∈ U)
C : Type u_1
inst_1 : Category.{v_1, u_1} C
A : C
inst_2 : HasZeroObject.{v_1, u_1} C
⊢ Sheaf.IsFlasque (skyscraperSheaf p₀ A)

Tactic:
isFlasque_skyscraperSheaf_of_epi_from p₀ A

Premises used: isFlasque_skyscraperSheaf_of_epi_from
-- Module: Mathlib.Topology.Sheaves.Forget
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : G.ReflectsIsomorphisms
inst_3 : HasLimitsOfSize.{v, v, v₁, u₁} C
inst_4 : PreservesLimitsOfSize.{v, v, v₁, v₂, u₁, u₂} G
X : TopCat
F : Presheaf.{v, v₁, u₁} C X
⊢ F.IsSheaf ↔ IsSheaf (F ⋙ G)

Tactic:
Presheaf.isSheaf_iff_isSheaf_comp _ F G

Premises used: TopCat.Presheaf.IsSheaf, CategoryTheory.Presheaf.isSheaf_iff_isSheaf_comp
-- Module: Mathlib.Topology.Sheaves.Forget
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : Type u₂
inst_1 : Category.{v, u₂} D
G : CategoryTheory.Functor.{v, v, u₁, u₂} C D
inst_2 : G.ReflectsIsomorphisms
inst_3 : HasLimits.{v, u₁} C
inst_4 : PreservesLimits G
X : TopCat
F : Presheaf C X
⊢ F.IsSheaf ↔ IsSheaf (F ⋙ G)

Tactic:
isSheaf_iff_isSheaf_comp' G F

Premises used: TopCat.Presheaf.isSheaf_iff_isSheaf_comp'
-- Module: Mathlib.Topology.Sheaves.Functors
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf.{w, v, u} C X
h : F.IsSheaf
⊢ (Functor.obj (pushforward C f) F).IsSheaf

Tactic:
(Opens.map f).op_comp_isSheaf _ _ ⟨_, h⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Functor.comp, TopCat.Presheaf.IsSheaf, CategoryTheory.Functor.op_comp_isSheaf, TopologicalSpace.Opens.map
-- Module: Mathlib.Topology.Sheaves.Functors
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
⊢ Eq (α := Sheaf.{w, v, u} C X ⥤ Presheaf.{w, v, u} C Y) (pushforward C f ⋙ forget C Y)
    (forget C X ⋙ Presheaf.pushforward C f)

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.inducedFunctor, CategoryTheory.Functor.sheafPushforwardContinuous, TopCat.Sheaf.forget, rfl, TopCat.Sheaf.pushforward
-- Module: Mathlib.Topology.Sheaves.Functors
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Sheaf.{w, v, u} C X
⊢ (Functor.obj (pushforward C f) F).obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w))) =
    Functor.obj (Presheaf.pushforward C f)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.Topology.Sheaves.Functors
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F F' : Sheaf.{w, v, u} C X
α : F ⟶ F'
⊢ Eq (α :=
    (Functor.obj (pushforward C f) F).obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w))) ⟶
      (Functor.obj (pushforward C f) F').obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑Y : Type w))))
    (InducedCategory.Hom.hom (CategoryTheory.Functor.map (pushforward C f) α))
    (CategoryTheory.Functor.map (Presheaf.pushforward C f) α.hom)

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.Topology.Sheaves.Functors
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens (↑Y : Type w)
A : Type u_1
inst_1 : Category.{w, u_1} A
FA : A → A → Type u_2
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_2 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory A FA (CC := CA)
inst_4 : HasColimits.{w, u_1} A
inst_5 : HasLimits.{w, u_1} A
inst_6 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_7 : PreservesFilteredColimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_8 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ Functor.IsLeftAdjoint (C := Sheaf A Y) (pullback A (FA := FA) (CA := CA) f)

Tactic:
(pullbackPushforwardAdjunction A f).isLeftAdjoint

Premises used: TopCat.Sheaf.pullbackPushforwardAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.Topology.Sheaves.Functors
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens (↑Y : Type w)
A : Type u_1
inst_1 : Category.{w, u_1} A
FA : A → A → Type u_2
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_2 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory A FA (CC := CA)
inst_4 : HasColimits.{w, u_1} A
inst_5 : HasLimits.{w, u_1} A
inst_6 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_7 : PreservesFilteredColimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_8 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ Functor.IsRightAdjoint (C := Sheaf A Y) (pushforward A f)

Tactic:
(pullbackPushforwardAdjunction A f).isRightAdjoint

Premises used: TopCat.Sheaf.pullbackPushforwardAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.Topology.Sheaves.Functors
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f_1 : X ⟶ Y
ι : Type w
U : ι → Opens (↑Y : Type w)
A : Type u_1
inst_1 : Category.{w, u_1} A
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
FA : A → A → Type u_2
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_2 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory A FA (CC := CA)
inst_4 : HasColimits.{w, u_1} A
inst_5 : HasLimits.{w, u_1} A
inst_6 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_7 : PreservesFilteredColimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_8 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CA))
F : TopCat.Sheaf A Y
⊢ Functor.obj (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A)
      F ≅
    Functor.obj (sheafPullback A hf) F

Tactic:
exact (presheafToSheaf (Opens.grothendieckTopology ↑X) A).mapIso
      (hf.isOpenMap.pullbackIso.app _) ≪≫
      (fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology X) A).preimageIso
      (isoSheafify (Opens.grothendieckTopology X)
      (TopCat.Presheaf.isSheaf_of_isOpenEmbedding hf F.2)).symm

Premises used: Topology.IsOpenEmbedding.isOpenMap, Opens.grothendieckTopology, CategoryTheory.presheafToSheaf, TopCat.carrier, IsOpenMap.pullbackIso, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Topology.Sheaves.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{v_1, w} J
inst_2 : HasLimitsOfShape.{v_1, w, v, u} J C
X : TopCat
⊢ HasLimitsOfShape J (Presheaf.{t, v, u} C X)

Tactic:
functorCategoryHasLimitsOfShape

Premises used: TopCat.Presheaf, CategoryTheory.Limits.functorCategoryHasLimitsOfShape
-- Module: Mathlib.Topology.Sheaves.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{v_1, w} J
inst_2 : HasColimitsOfShape.{v_1, w, v, u} J C
X : TopCat
⊢ HasColimitsOfShape J (Presheaf.{u_1, v, u} C X)

Tactic:
functorCategoryHasColimitsOfShape

Premises used: TopCat.Presheaf, CategoryTheory.Limits.functorCategoryHasColimitsOfShape
-- Module: Mathlib.Topology.Sheaves.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{v_1, w} J
inst_2 : HasLimitsOfShape.{v_1, w, v, u} J C
X : TopCat
⊢ HasLimitsOfShape J (Sheaf.{t, v, u} C X)

Tactic:
hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (Sheaf.forget C X)

Premises used: CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{v_1, w} J
inst_2 : HasLimitsOfShape.{v_1, w, v, u} J C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
F' : J ⥤ Sheaf C X :=
  {
    obj := fun (j : J) ↦
      ObjectProperty.FullSubcategory.mk (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))) (F.obj j) ⋯,
    map := fun {X_1 Y : J} (f : X_1 ⟶ Y) ↦ { hom := F.map f }, map_id := ⋯, map_comp := ⋯ }
e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents (fun (x : J) ↦ Iso.refl ((F' ⋙ Sheaf.forget C X).obj x)) ⋯
⊢ c.pt.IsSheaf

Tactic:
Presheaf.isSheaf_of_iso
    ((isLimitOfPreserves (Sheaf.forget C X) (limit.isLimit F')).conePointsIsoOfNatIso hc e)
    (limit F').2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, TopCat.Presheaf.isSheaf_of_iso, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso, CategoryTheory.Limits.isLimitOfPreserves, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{v_1, w} J
inst_2 : HasLimitsOfShape.{v_1, w, v, u} J C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
F' : J ⥤ Sheaf C X :=
  {
    obj := fun (j : J) ↦
      ObjectProperty.FullSubcategory.mk (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))) (F.obj j) ⋯,
    map := fun {X_1 Y : J} (f : X_1 ⟶ Y) ↦ { hom := F.map f }, map_id := ⋯, map_comp := ⋯ }
e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents (fun (x : J) ↦ Iso.refl ((F' ⋙ Sheaf.forget C X).obj x)) ⋯
⊢ c.pt.IsSheaf

Tactic:
exact Presheaf.isSheaf_of_iso
    ((isLimitOfPreserves (Sheaf.forget C X) (limit.isLimit F')).conePointsIsoOfNatIso hc e)
    (limit F').2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, TopCat.Presheaf.isSheaf_of_iso, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso, CategoryTheory.Limits.isLimitOfPreserves, TopCat.Sheaf.forget
-- Module: Mathlib.Topology.Sheaves.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{v_1, w} J
inst_2 : HasLimitsOfShape.{v_1, w, v, u} J C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
⊢ (limit F).IsSheaf

Tactic:
isSheaf_of_isLimit F H (limit.isLimit F)

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, TopCat.isSheaf_of_isLimit
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_2) → Type u_1
T : Type u_3
inst : TopologicalSpace T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦
        f ((i : (a : ↥V) → ↥U) x)
apply : ∀ (x : ↥U), ContinuousAt f x
⊢ (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) f

Tactic:
apply continuous_iff_continuousAt.2

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_2) → Type u_1
T : Type u_3
inst : TopologicalSpace T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦
        f ((i : (a : ↥V) → ↥U) x)
x : ↥U
⊢ ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
    (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
specialize w x
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_2) → Type u_1
T : Type u_3
inst : TopologicalSpace T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T
x : ↥U
w :
  ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
    (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
rcases :
  ∀ (V : Opens (↑X : Type u_2)) (m : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U)
    (w :
      (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦
        f ((i : (a : ↥V) → ↥U) x)),
    ContinuousAt f x
⊢ ContinuousAt f x

Tactic:
rcases w with ⟨V, m, i, w⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_2) → Type u_1
T : Type u_3
inst : TopologicalSpace T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T
x : ↥U
V : Opens (↑X : Type u_2)
m : (↑x : (↑X : Type u_2)) ∈ V
i : V ⟶ U
w : Continuous.{u_2, u_3} (Y := T) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
⊢ ∀ (x : ↥V), ContinuousAt.{u_2, u_3} (Y := T) (fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)) x

Tactic:
rw [continuous_iff_continuousAt] at w

Premises used: continuous_iff_continuousAt