awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S R : Sieve.{v₁, u₁} X
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{max w' w, v₁, u₁} C
U V : Cᵒᵖ
f : U ⟶ V
x :
  ULift.{w', w}
    { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) U //
      S.arrows (Y := Opposite.unop U)
        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X) x) }
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V)
    ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{max w w', v₁, u₁} X) f.unop.op) :
          (a :
              (fun (X : Type (max w w')) ↦ X)
                ((shrinkYoneda.{max w w', v₁, u₁}.obj X).obj (Opposite.op (Opposite.unop U)))) →
            (fun (X : Type (max w w')) ↦ X)
              ((shrinkYoneda.{max w w', v₁, u₁}.obj X).obj (Opposite.op (Opposite.unop V))))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : Opposite.unop (Opposite.op (Opposite.unop U)) ⟶ X) →
              (shrinkYoneda.{max w w', v₁, u₁}.obj X).obj (Opposite.op (Opposite.unop U)))
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
            (↑x.down : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U))) :
      (fun (X : Type (max w w')) ↦ X)
        (Functor.obj (Functor.obj shrinkYoneda.{max w w', v₁, u₁} X) (Opposite.op (Opposite.unop V))))
    ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) f) :
          (a : (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj U) → (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj V)
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : Opposite.unop U ⟶ X) → (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj U)
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
            (↑x.down : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U))) :
      Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : LocallySmall.{max w' w, v₁, u₁} C
⊢ Eq (α :=
    Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) (shrinkFunctor.{max w' w, v₁, u₁} S) ⟶
      Functor.obj shrinkYoneda.{w, v₁, u₁} X ⋙ CategoryTheory.uliftFunctor.{w', w})
    (Iso.inv S.shrinkFunctorUliftFunctorIso ≫
      Functor.whiskerRight (Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S)) CategoryTheory.uliftFunctor.{w', w})
    (Subfunctor.ι (shrinkFunctor.{max w' w, v₁, u₁} S) ≫ NatTrans.app (Iso.inv shrinkYonedaUliftFunctorIso) X)

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, TypeCat.Fun.comp, CategoryTheory.Subfunctor.ι, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z : C
f : Y_1 ⟶ X
S R : Sieve.{v₁, u₁} X
Y : Cᵒᵖ
⊢ ∀ (a : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) Y),
    Membership.mem (γ := Set (Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) Y))
        (Subfunctor.obj (shrinkFunctor.{v₁, v₁, u₁} S) Y) a ↔
      S.arrows (Y := Opposite.unop Y)
        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj Y) → Opposite.unop Y ⟶ X) a)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
S : Sieve.{v₂, u₂} (F.obj X)
⊢ functorPullback F S.arrows = (Sieve.functorPullback F S).arrows

Tactic:
rfl

Premises used: CategoryTheory.Presieve.functorPullback, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve.{v₁, u₁} (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
rw : (Sieve.generate (bindOfArrows Z f R)).arrows (u ≫ u' ≫ f (Sieve.ofArrows.i hv'))
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (v ≫ v')

Tactic:
rw [← Sieve.ofArrows.fac hv', ← reassoc_of% hu]

Premises used: CategoryTheory.Sieve.ofArrows.fac
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve.{v₁, u₁} (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (u ≫ u' ≫ f (Sieve.ofArrows.i hv'))

Tactic:
⟨S, u, u' ≫ f _, ⟨_, _, h⟩, rfl⟩

Premises used: CategoryTheory.Presieve.bindOfArrows.mk, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve.{v₁, u₁} (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (u ≫ u' ≫ f (Sieve.ofArrows.i hv'))

Tactic:
exact ⟨S, u, u' ≫ f _, ⟨_, _, h⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
X : Over.{v₁, u₁} S
R : Presieve X
⊢ Eq (α := Presieve.{v₁, u₁} (Functor.obj (Over.forget S) X)) (functorPushforward (Over.forget S) R)
    (Sieve.arrows (Sieve.generate (map (Over.forget S) R)))

Tactic:
(Sieve.arrows_generate_map_eq_functorPushforward (Over.forget S)).symm

Premises used: CategoryTheory.Over.forget, CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
y : T
hy : y ∈ Y
rcases :
  ∀ (U : Opens T) (g : U ⟶ X) (hg : S.arrows g) (hU : y ∈ U),
    ∃ (U : Opens T) (f_1 : U ⟶ Y), (Sieve.pullback f S).arrows f_1 ∧ y ∈ U
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), (Sieve.pullback f S).arrows f_1 ∧ y ∈ U

Tactic:
rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩

Premises used: Quiver.Hom.le
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), (Sieve.pullback f S).arrows f_1 ∧ y ∈ U

Tactic:
⟨U ⊓ Y, homOfLE inf_le_right, ?_, hU, hy⟩

Premises used: inf_le_right, CategoryTheory.homOfLE, And.intro, Exists.intro, Min.min
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
refine : (Sieve.pullback f S).arrows (Y := U ⊓ Y) (homOfLE ⋯)
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), (Sieve.pullback f S).arrows f_1 ∧ y ∈ U

Tactic:
refine ⟨U ⊓ Y, homOfLE inf_le_right, ?_, hU, hy⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ (Sieve.pullback f S).arrows (Y := U ⊓ Y) (homOfLE ⋯)

Tactic:
apply S.downward_closed hg (homOfLE inf_le_left)

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.homOfLE, inf_le_left
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Sieve X
hS : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve Y)) {S : Sieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), S.arrows f ∧ x ∈ U}
        (Sieve.pullback f R)
x : T
hx : x ∈ X
rcases : ∀ (U : Opens T) (f : U ⟶ X) (hf : S.arrows f) (hU : x ∈ U), ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U

Tactic:
rcases hS x hx with ⟨U, f, hf, hU⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Sieve X
hS : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve Y)) {S : Sieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), S.arrows f ∧ x ∈ U}
        (Sieve.pullback f R)
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
rcases :
  ∀ (V : Opens T) (g : V ⟶ U) (hg : (Sieve.pullback f R).arrows g) (hV : x ∈ V),
    ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U

Tactic:
rcases hR hf _ hU with ⟨V, g, hg, hV⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Sieve X
hS : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve Y)) {S : Sieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), S.arrows f ∧ x ∈ U}
        (Sieve.pullback f R)
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : (Sieve.pullback f R).arrows g
hV : x ∈ V
⊢ ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U

Tactic:
⟨_, g ≫ f, hg, hV⟩

Premises used: And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Sieve X
hS : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve Y)) {S : Sieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), S.arrows f ∧ x ∈ U}
        (Sieve.pullback f R)
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : (Sieve.pullback f R).arrows g
hV : x ∈ V
⊢ ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U

Tactic:
exact ⟨_, g ≫ f, hg, hV⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
x : T
hx : x ∈ Y
rcases :
  ∀ (U : Opens T) (g : U ⟶ X) (hg : S g) (hU : x ∈ U),
    ∃ (U : Opens T) (f_1 : U ⟶ Y), Presieve.pullbackArrows f S f_1 ∧ x ∈ U
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), Presieve.pullbackArrows f S f_1 ∧ x ∈ U

Tactic:
rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩

Premises used: Quiver.Hom.le
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), Presieve.pullbackArrows f S f_1 ∧ x ∈ U

Tactic:
⟨_, _, Presieve.pullbackArrows.mk _ _ hg, ?_⟩

Premises used: And.intro, Exists.intro, CategoryTheory.Presieve.pullbackArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
refine : x ∈ pullback g f
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), Presieve.pullbackArrows f S f_1 ∧ x ∈ U

Tactic:
refine ⟨_, _, Presieve.pullbackArrows.mk _ _ hg, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ U ⊓ Y ≤ pullback g f

Tactic:
have : U ⊓ Y ≤ pullback g f :=
      leOfHom (pullback.lift (homOfLE inf_le_left) (homOfLE inf_le_right) rfl)
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
this : U ⊓ Y ≤ pullback g f
⊢ x ∈ pullback g f

Tactic:
apply this ⟨hU, hx⟩

Premises used: And.intro
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
hTi :
  ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve Y)) {R : Presieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), R f ∧ x ∈ U} (Ti f H)
x : T
hx : x ∈ X
rcases : ∀ (U : Opens T) (f : U ⟶ X) (hf : S f) (hU : x ∈ U), ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U

Tactic:
rcases hS x hx with ⟨U, f, hf, hU⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
hTi :
  ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve Y)) {R : Presieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), R f ∧ x ∈ U} (Ti f H)
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
rcases : ∀ (V : Opens T) (g : V ⟶ U) (hg : Ti f hf g) (hV : x ∈ V), ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U

Tactic:
rcases hTi f hf x hU with ⟨V, g, hg, hV⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
hTi :
  ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve Y)) {R : Presieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), R f ∧ x ∈ U} (Ti f H)
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : Ti f hf g
hV : x ∈ V
⊢ ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U

Tactic:
⟨_, _, ⟨_, g, f, hf, hg, rfl⟩, hV⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
hTi :
  ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve Y)) {R : Presieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), R f ∧ x ∈ U} (Ti f H)
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : Ti f hf g
hV : x ∈ V
⊢ ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U

Tactic:
exact ⟨_, _, ⟨_, g, f, hf, hg, rfl⟩, hV⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
a : LE.le (α := Pretopology (Opens T)) (GrothendieckTopology.toPretopology (grothendieckTopology T)) (pretopology T)
a₁ : LE.le (α := Pretopology (Opens T)) (pretopology T) (GrothendieckTopology.toPretopology (grothendieckTopology T))
⊢ Eq (α := Pretopology (Opens T)) (GrothendieckTopology.toPretopology (grothendieckTopology T)) (pretopology T)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
R : Presieve X
hR :
  R ∈ Precoverage.coverings (Pretopology.toPrecoverage (GrothendieckTopology.toPretopology (grothendieckTopology T))) X
x : T
hx : x ∈ X
a :
  ∀ (U : Opens T) (f : U ⟶ X) (hU : x ∈ U) (V : Opens T) (g₁ : U ⟶ V) (g₂ : V ⟶ X) (hg₂ : R g₂),
    g₁ ≫ g₂ = f → ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U

Tactic:
rcases hR x hx with ⟨U, f, ⟨V, g₁, g₂, hg₂, _⟩, hU⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
R : Presieve X
hR :
  R ∈ Precoverage.coverings (Pretopology.toPrecoverage (GrothendieckTopology.toPretopology (grothendieckTopology T))) X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hU : x ∈ U
V : Opens T
g₁ : U ⟶ V
g₂ : V ⟶ X
hg₂ : R g₂
right : g₁ ≫ g₂ = f
⊢ ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U

Tactic:
⟨V, g₂, hg₂, g₁.le hU⟩

Premises used: Quiver.Hom.le, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
R : Presieve X
hR :
  R ∈ Precoverage.coverings (Pretopology.toPrecoverage (GrothendieckTopology.toPretopology (grothendieckTopology T))) X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hU : x ∈ U
V : Opens T
g₁ : U ⟶ V
g₂ : V ⟶ X
hg₂ : R g₂
right : g₁ ≫ g₂ = f
⊢ ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U

Tactic:
exact ⟨V, g₂, hg₂, g₁.le hU⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Precoverage.coverings (Pretopology.toPrecoverage (pretopology T)) X
x : T
hx : x ∈ X
a :
  ∀ (U : Opens T) (f : U ⟶ X) (hf : R f) (hU : x ∈ U), ∃ (U : Opens T) (f : U ⟶ X), (Sieve.generate R).arrows f ∧ x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), (Sieve.generate R).arrows f ∧ x ∈ U

Tactic:
rcases hR x hx with ⟨U, f, hf, hU⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Precoverage.coverings (Pretopology.toPrecoverage (pretopology T)) X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : R f
hU : x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), (Sieve.generate R).arrows f ∧ x ∈ U

Tactic:
⟨U, f, Sieve.le_generate R U _ hf, hU⟩

Premises used: CategoryTheory.Sieve.le_generate, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Precoverage.coverings (Pretopology.toPrecoverage (pretopology T)) X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : R f
hU : x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), (Sieve.generate R).arrows f ∧ x ∈ U

Tactic:
exact ⟨U, f, Sieve.le_generate R U _ hf, hU⟩
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
rw :
  Eq (α := GrothendieckTopology (Opens T))
    (Pretopology.toGrothendieck (GrothendieckTopology.toPretopology (grothendieckTopology T))) (grothendieckTopology T)
⊢ Eq (α := GrothendieckTopology (Opens T)) (Pretopology.toGrothendieck (pretopology T)) (grothendieckTopology T)

Tactic:
rw [← toPretopology_grothendieckTopology]

Premises used: Opens.toPretopology_grothendieckTopology
-- Module: Mathlib.CategoryTheory.Sites.Spaces
Goal:
T : Type u
inst : TopologicalSpace T
⊢ Eq (α := GrothendieckTopology (Opens T))
    (Pretopology.toGrothendieck (GrothendieckTopology.toPretopology (grothendieckTopology T))) (grothendieckTopology T)

Tactic:
apply (Pretopology.gi (Opens T)).l_u_eq

Premises used: TopologicalSpace.Opens, CategoryTheory.Pretopology.gi, GaloisInsertion.l_u_eq
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
⊢ Eq.{v + 1} (α := F.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.yonedaEquiv : (a : J.yoneda.obj X ⟶ F) → F.obj.obj (op X)) f : F.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op X)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj X).obj.obj (op X))) → (fun (X : Type v) ↦ X) (F.obj.obj (op X)))
        (𝟙 X) :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X : C
F : Sheaf J (Type v)
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
Y : Cᵒᵖ
f : unop Y ⟶ X
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf J).obj Y)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              (InducedCategory.Hom.hom ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x))
              Y) :
          (a : unop Y ⟶ X) → F.obj.obj Y)
        f :
      F.obj (P := Presheaf.IsSheaf J).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F.obj.obj (op X)) → F.obj.obj Y)
        x :
      F.obj (P := Presheaf.IsSheaf J).obj Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
simp :
  Eq (α := obj CategoryTheory.yoneda Y ⟶ F.obj (P := Presheaf.IsSheaf J))
    (map CategoryTheory.yoneda g ≫
      (FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J (Type v)) :
          (a : J.yoneda.obj X ⟶ F) → CategoryTheory.yoneda.obj X ⟶ F.obj)
        f)
    ((FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J (Type v)) :
        (a : J.yoneda.obj Y ⟶ F) → CategoryTheory.yoneda.obj Y ⟶ F.obj)
      (J.yoneda.map g ≫ f))
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F.obj.obj (op Y)))
        ((J.yonedaEquiv : (a : J.yoneda.obj X ⟶ F) → F.obj.obj (op X)) f : F.obj (P := Presheaf.IsSheaf J).obj (op X)) :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((J.yonedaEquiv : (a : J.yoneda.obj Y ⟶ F) → F.obj.obj (op Y)) (J.yoneda.map g ≫ f) :
      F.obj (P := Presheaf.IsSheaf J).obj (op Y))

Tactic:
simp [yonedaEquiv, CategoryTheory.yonedaEquiv_naturality]

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv, CategoryTheory.yonedaEquiv_naturality
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ Eq (α := obj CategoryTheory.yoneda Y ⟶ F.obj (P := Presheaf.IsSheaf J))
    (map CategoryTheory.yoneda g ≫
      (FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J (Type v)) :
          (a : J.yoneda.obj X ⟶ F) → CategoryTheory.yoneda.obj X ⟶ F.obj)
        f)
    ((FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J (Type v)) :
        (a : J.yoneda.obj Y ⟶ F) → CategoryTheory.yoneda.obj Y ⟶ F.obj)
      (J.yoneda.map g ≫ f))

Tactic:
rfl