awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ Membership.mem (γ := Set (Presieve.{v, u} Y))
    {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f}
    (pullbackArrows f (Presieve.singleton g))

Tactic:
⟨pullback g f, pullback.snd _ _, ?_, ?_⟩

Premises used: CategoryTheory.Limits.pullback, Set.Mem, CategoryTheory.Limits.pullback.snd, setOf, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
refine_1 : IsIso (X := pullback g f) (pullback.snd g f)
refine_2 : pullbackArrows f (Presieve.singleton g) = Presieve.singleton (Y := pullback g f) (pullback.snd g f)
⊢ Membership.mem (γ := Set (Presieve.{v, u} Y))
    {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f}
    (pullbackArrows f (Presieve.singleton g))

Tactic:
refine ⟨pullback g f, pullback.snd _ _, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (f ≫ inv g) ≫ g = 𝟙 Y ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ CategoryStruct.comp (Y := pullback g f) (pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) (pullback.snd g f) = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
refine_1 : pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯ = 𝟙 (pullback g f)
⊢ IsIso (X := pullback g f) (pullback.snd g f)

Tactic:
refine ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨?_, by simp⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
refine_1 :
  CategoryStruct.comp (Y := pullback g f) (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) (pullback.fst g f) =
    𝟙 (pullback g f) ≫ pullback.fst g f
refine_1₁ :
  CategoryStruct.comp (Y := pullback g f) (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) (pullback.snd g f) =
    𝟙 (pullback g f) ≫ pullback.snd g f
⊢ pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯ = 𝟙 (pullback g f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
refine_1 : pullback.fst g f ≫ g ≫ inv g = 𝟙 (pullback g f) ≫ pullback.fst g f
⊢ CategoryStruct.comp (Y := pullback g f) (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) (pullback.fst g f) =
    𝟙 (pullback g f) ≫ pullback.fst g f

Tactic:
rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.fst g f ≫ g ≫ inv g = 𝟙 (pullback g f) ≫ pullback.fst g f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ CategoryStruct.comp (Y := pullback g f) (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) (pullback.snd g f) =
    𝟙 (pullback g f) ≫ pullback.snd g f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullbackArrows f (Presieve.singleton g) = Presieve.singleton (Y := pullback g f) (pullback.snd g f)

Tactic:
apply pullback_singleton

Premises used: CategoryTheory.Presieve.pullback_singleton
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
rcases :
  ∀ (Y : C) (f : Y ⟶ Z) (i : IsIso f) (hTi : Ti g ⋯ = Presieve.singleton f),
    Membership.mem (γ := Set (Presieve.{v, u} X))
      {S : Presieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X) (_ : IsIso f), S = Presieve.singleton f}
      ((Presieve.singleton g).bind Ti)
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
    {S : Presieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X) (_ : IsIso f), S = Presieve.singleton f}
    ((Presieve.singleton g).bind Ti)

Tactic:
rcases hS g (singleton_self g) with ⟨Y, f, i, hTi⟩

Premises used: CategoryTheory.Presieve.singleton_self
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
    {S : Presieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X) (_ : IsIso f), S = Presieve.singleton f}
    ((Presieve.singleton g).bind Ti)

Tactic:
⟨_, f ≫ g, ?_, ?_⟩

Premises used: Set.Mem, setOf, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
refine_1 : IsIso (f ≫ g)
refine_2 : (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
    {S : Presieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X) (_ : IsIso f), S = Presieve.singleton f}
    ((Presieve.singleton g).bind Ti)

Tactic:
refine ⟨_, f ≫ g, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ IsIso (f ≫ g)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
refine_2 : ∀ (x : C), Eq (α := (x ⟶ X) → Prop) ((Presieve.singleton g).bind Ti) (Presieve.singleton (f ≫ g))
⊢ (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)

Tactic:
apply funext

Premises used: funext
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
refine_2 : ∀ (K : W ⟶ X), (Presieve.singleton g).bind Ti K ↔ Presieve.singleton (f ≫ g) K
⊢ Eq (α := (W ⟶ X) → Prop) ((Presieve.singleton g).bind Ti) (Presieve.singleton (f ≫ g))

Tactic:
ext K
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
refine_2 : (Presieve.singleton g).bind Ti K → Presieve.singleton (f ≫ g) K
refine_2₁ : Presieve.singleton (f ≫ g) K → (Presieve.singleton g).bind Ti K
⊢ (Presieve.singleton g).bind Ti K ↔ Presieve.singleton (f ≫ g) K

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W Y : C
h : W ⟶ Z
hh : Ti g ⋯ h
⊢ Presieve.singleton f h

Tactic:
rw [hTi] at hh
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W Y : C
h : W ⟶ Z
hh : Presieve.singleton f h
refine_2 : Presieve.singleton (f ≫ g) (f ≫ g)
⊢ Presieve.singleton (f ≫ g) (h ≫ g)

Tactic:
cases hh
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ Presieve.singleton (f ≫ g) (f ≫ g)

Tactic:
apply singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ (Presieve.singleton g).bind Ti (f ≫ g)

Tactic:
bind_comp g singleton.mk ?_

Premises used: CategoryTheory.Presieve.singleton.mk, CategoryTheory.Presieve.bind_comp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
refine_2 : Ti g ⋯ f
⊢ (Presieve.singleton g).bind Ti (f ≫ g)

Tactic:
refine bind_comp g singleton.mk ?_

Premises used: CategoryTheory.Presieve.singleton.mk, CategoryTheory.Presieve.bind_comp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
refine_2 : Presieve.singleton f f
⊢ Ti g ⋯ f

Tactic:
rw [hTi]
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ Presieve.singleton f f

Tactic:
apply singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X Y : C
f : Y ⟶ X
hf : IsIso f
⊢ Presieve.singleton f ∈ K.coverings X

Tactic:
K.has_isos f

Premises used: CategoryTheory.Pretopology.has_isos
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X Y : C
f : Y ⟶ X
hf : IsIso f
⊢ Presieve.singleton f ∈ K.coverings X

Tactic:
exact K.has_isos f

Premises used: CategoryTheory.Pretopology.has_isos
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
⊢ Eq (α := GrothendieckTopology.{v, u} C) (toGrothendieck ⊥) ⊥

Tactic:
(gi C).gc.l_bot

Premises used: CategoryTheory.Pretopology.gi, GaloisConnection.l_bot, GaloisInsertion.gc
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J K : Pretopology.{v, u} C
h : J ≤ K
⊢ J.toGrothendieck ≤ K.toGrothendieck

Tactic:
fun _ _ ⟨R, hR, hle⟩ ↦ ⟨R, h _ hR, hle⟩

Premises used: Membership.mem, CategoryTheory.Pretopology.toGrothendieck, _private.0.CategoryTheory.Pretopology.toGrothendieck_mono.match_1, Set.Subset, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X Y : C
f : Y ⟶ X
h : IsIso f
simp : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), Presieve.singleton f ∈ i.coverings X
⊢ Membership.mem (γ := Set (Presieve.{v, u} X)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) X)
    (Presieve.singleton f)

Tactic:
simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image,
        Set.iInter_exists,
        Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter]

Premises used: Set.iInf_eq_iInter, Set.iInter_iInter_eq_right, Set.mem_image, sInf_apply, Set.mem_iInter, Set.iInter_exists, Set.biInter_and', Set.iInter_coe_set
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X Y : C
f : Y ⟶ X
h : IsIso f
t : Pretopology.{v, u} C
_ : t ∈ T → Presieve.singleton f ∈ t.coverings X
⊢ ∀ (i : t ∈ T), Presieve.singleton f ∈ t.coverings X

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X Y : C
f : Y ⟶ X
h : IsIso f
t : Pretopology.{v, u} C
i : t ∈ T
⊢ Presieve.singleton f ∈ t.coverings X

Tactic:
t.has_isos f

Premises used: CategoryTheory.Pretopology.has_isos
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X Y : C
f : Y ⟶ X
h : IsIso f
t : Pretopology.{v, u} C
i : t ∈ T
⊢ Presieve.singleton f ∈ t.coverings X

Tactic:
exact t.has_isos f

Premises used: CategoryTheory.Pretopology.has_isos
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X Y : C
f : Y ⟶ X
S : Presieve.{v, u} X
hS : Membership.mem (γ := Set (Presieve.{v, u} X)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) X) S
simp :
  ∀ (hS : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S ∈ i.coverings X) (i : Pretopology.{v, u} C) (i_1 : i ∈ T),
    pullbackArrows f S ∈ i.coverings Y
⊢ Membership.mem (γ := Set (Presieve.{v, u} Y)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) Y)
    (pullbackArrows f S)

Tactic:
simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image,
        Set.iInter_exists, Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter] at hS ⊢

Premises used: Set.iInf_eq_iInter, Set.iInter_iInter_eq_right, Set.mem_image, sInf_apply, Set.mem_iInter, Set.iInter_exists, Set.biInter_and', Set.iInter_coe_set
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X Y : C
f : Y ⟶ X
S : Presieve.{v, u} X
hS : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S ∈ i.coverings X
t : Pretopology.{v, u} C
ht : t ∈ T
⊢ pullbackArrows f S ∈ t.coverings Y

Tactic:
t.pullbacks f S (hS t ht)

Premises used: CategoryTheory.Pretopology.pullbacks
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X Y : C
f : Y ⟶ X
S : Presieve.{v, u} X
hS : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S ∈ i.coverings X
t : Pretopology.{v, u} C
ht : t ∈ T
⊢ pullbackArrows f S ∈ t.coverings Y

Tactic:
exact t.pullbacks f S (hS t ht)

Premises used: CategoryTheory.Pretopology.pullbacks
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS : Membership.mem (γ := Set (Presieve.{v, u} X)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) X) S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) Y)
      (Ti f H)
simp :
  ∀ (hS : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S ∈ i.coverings X)
    (hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f) (i : Pretopology.{v, u} C) (i_1 : i ∈ T), Ti f H ∈ i.coverings Y)
    (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S.bind Ti ∈ i.coverings X
⊢ Membership.mem (γ := Set (Presieve.{v, u} X)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) X)
    (S.bind Ti)

Tactic:
simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image,
        Set.iInter_exists, Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter] at hS hTi ⊢

Premises used: Set.iInf_eq_iInter, Set.iInter_iInter_eq_right, Set.mem_image, sInf_apply, Set.mem_iInter, Set.iInter_exists, Set.biInter_and', Set.iInter_coe_set
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S ∈ i.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f) (i : Pretopology.{v, u} C) (i_1 : i ∈ T), Ti f H ∈ i.coverings Y
t : Pretopology.{v, u} C
ht : t ∈ T
⊢ S.bind Ti ∈ t.coverings X

Tactic:
t.transitive S Ti (hS t ht) (fun Y f H ↦ hTi f H t ht)

Premises used: CategoryTheory.Pretopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S ∈ i.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f) (i : Pretopology.{v, u} C) (i_1 : i ∈ T), Ti f H ∈ i.coverings Y
t : Pretopology.{v, u} C
ht : t ∈ T
⊢ S.bind Ti ∈ t.coverings X

Tactic:
exact t.transitive S Ti (hS t ht) (fun Y f H ↦ hTi f H t ht)

Premises used: CategoryTheory.Pretopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X : C
S : Presieve.{v, u} X
⊢ Membership.mem (γ := Set (Presieve.{v, u} X)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) X) S ↔
    ∀ t ∈ T, S ∈ t.coverings X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (GrothendieckTopology.{v, u} C)
coverings :
  ∀ (X : C) (S : Presieve.{v, u} X),
    S ∈ (toPrecoverage (sInf T).toPretopology).coverings X ↔
      S ∈ (toPrecoverage (sInf (GrothendieckTopology.toPretopology '' T))).coverings X
⊢ Eq (α := Pretopology.{v, u} C) (sInf T).toPretopology (sInf (GrothendieckTopology.toPretopology '' T))

Tactic:
ext X S
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (GrothendieckTopology.{v, u} C)
X : C
S : Presieve.{v, u} X
⊢ S ∈ (toPrecoverage (sInf T).toPretopology).coverings X ↔
    S ∈ (toPrecoverage (sInf (GrothendieckTopology.toPretopology '' T))).coverings X

Tactic:
simp [mem_sInf, GrothendieckTopology.mem_toPretopology, GrothendieckTopology.mem_sInf]

Premises used: CategoryTheory.GrothendieckTopology.mem_toPretopology, CategoryTheory.GrothendieckTopology.mem_sInf, CategoryTheory.Pretopology.mem_sInf
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
⊢ IsGLB T (sInf T)

Tactic:
IsGLB.of_image (f := fun J ↦ J.coverings) Iff.rfl (_root_.isGLB_sInf _)

Premises used: IsGLB.of_image
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
t₁ t₂ : Pretopology.{v, u} C
X : C
S : Presieve.{v, u} X
⊢ S ∈ (t₁ ⊓ t₂).coverings X ↔ S ∈ t₁.coverings X ∧ S ∈ t₂.coverings X

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
R : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → R f → Presieve.{v, u} Y
hR : R ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : R f), Ti f H ∈ J.coverings Y
obtain :
  ∀ (ι : Type (max u v)) (Z : ι → C) (g : (i : ι) → Z i ⟶ X)
    (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y) (hR : ofArrows Z g ∈ J.coverings X)
    (hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y), (ofArrows Z g).bind Ti ∈ J.coverings X
⊢ R.bind Ti ∈ J.coverings X

Tactic:
obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl