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 : Y ⟶ X
S_1 R_1 S R : Sieve.{v₁, u₁} X
Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
h : R.arrows f_1
g : Z_1 ⟶ Y_1
⊢ S.arrows (g ≫ f_1) ∨ R.arrows (g ≫ f_1)

Tactic:
simp [h]
-- 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 : Y ⟶ X
S_1 R_1 S R : Sieve.{v₁, u₁} X
Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
h₁ : S.arrows f_1
h₂ : R.arrows f_1
g : Z_1 ⟶ Y_1
⊢ S.arrows (g ≫ f_1) ∧ R.arrows (g ≫ f_1)

Tactic:
simp [h₁, h₂]
-- 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 x x_1 x_2 : Sieve.{v₁, u₁} X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x.arrows f → x_2.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x_1.arrows f → x_2.arrows f
x_3 : C
f : x_3 ⟶ X
hf : x.arrows f
⊢ x_2.arrows f

Tactic:
h₁ _ hf
-- 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 x x_1 x_2 : Sieve.{v₁, u₁} X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x.arrows f → x_2.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x_1.arrows f → x_2.arrows f
x_3 : C
f : x_3 ⟶ X
hf : x.arrows f
⊢ x_2.arrows f

Tactic:
exact h₁ _ hf
-- 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 x x_1 x_2 : Sieve.{v₁, u₁} X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x.arrows f → x_2.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x_1.arrows f → x_2.arrows f
x_3 : C
f : x_3 ⟶ X
hf : x_1.arrows f
⊢ x_2.arrows f

Tactic:
h₂ _ hf
-- 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 x x_1 x_2 : Sieve.{v₁, u₁} X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x.arrows f → x_2.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x_1.arrows f → x_2.arrows f
x_3 : C
f : x_3 ⟶ X
hf : x_1.arrows f
⊢ x_2.arrows f

Tactic:
exact h₂ _ hf
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Ss : Set (Sieve.{v₁, u₁} X)
Y : C
f : Y ⟶ X
⊢ (sInf Ss).arrows f ↔ ∀ S ∈ Ss, S.arrows f

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Ss : Set (Sieve.{v₁, u₁} X)
Y : C
f : Y ⟶ X
⊢ (sSup Ss).arrows f ↔ ∃ (S : Sieve.{v₁, u₁} X) (_ : S ∈ Ss), S.arrows f

Tactic:
simp [sSup, Sieve.sup]

Premises used: CategoryTheory.Sieve.sup, SupSet.sSup
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
⊢ (R ⊓ S).arrows f ↔ R.arrows f ∧ S.arrows f

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
⊢ (R ⊔ S).arrows f ↔ R.arrows f ∨ S.arrows f

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ arrows ⊤ f

Tactic:
trivial

Premises used: trivial
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ arrows ⊥ f ↔ False

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq (α := Presieve.{v₁, u₁} X) (arrows ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
⊢ S.arrows = ⊤ ↔ S = ⊤

Tactic:
⟨fun h ↦ arrows_ext (h ▸ arrows_top), fun h ↦ h ▸ arrows_top⟩

Premises used: Eq.rec, CategoryTheory.Sieve.arrows_top, CategoryTheory.Sieve.arrows_ext, Iff.intro, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq (α := Presieve.{v₁, u₁} X) (arrows ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
⊢ S.arrows = ⊥ ↔ S = ⊥

Tactic:
⟨fun h ↦ arrows_ext (h ▸ arrows_bot), fun h ↦ h ▸ arrows_bot⟩

Premises used: Eq.rec, CategoryTheory.Sieve.arrows_ext, CategoryTheory.Sieve.arrows_bot, Iff.intro, Eq.symm
-- 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 : Y ⟶ X
S R : Sieve.{v₁, u₁} X
h : Eq (α := Sieve.{v₁, u₁} X) ⊤ ⊥
⊢ False

Tactic:
simp [← bot_apply (𝟙 X), ← h]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Sieve.bot_apply
-- 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_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
Y Z W : C
g : Y ⟶ W
f : W ⟶ X
hf : R f
h : Z ⟶ Y
⊢ (h ≫ g) ≫ f = h ≫ g ≫ f

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 Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
Y Z W : C
g : Y ⟶ W
f : W ⟶ X
hf : R f
h : Z ⟶ Y
⊢ ∃ (Y_2 : C) (h_1 : Z ⟶ Y_2) (g_1 : Y_2 ⟶ X), R g_1 ∧ h_1 ≫ g_1 = h ≫ g ≫ f

Tactic:
exact ⟨_, h ≫ g, _, hf, by 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 : Presieve.{v₁, u₁} X
⊢ (generate (Presieve.map F s)).arrows = Presieve.functorPushforward F s

Tactic:
funext fun Z ↦ funext fun u ↦ propext ⟨?_, ?_⟩

Premises used: CategoryTheory.Presieve, funext, Iff.intro, propext
-- 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 : Presieve.{v₁, u₁} X
refine_1 : ∀ (Z : D) (u : Z ⟶ F.obj X), (generate (Presieve.map F s)).arrows u → Presieve.functorPushforward F s u
refine_2 : ∀ (Z : D) (u : Z ⟶ F.obj X), Presieve.functorPushforward F s u → (generate (Presieve.map F s)).arrows u
⊢ (generate (Presieve.map F s)).arrows = Presieve.functorPushforward F s

Tactic:
refine funext fun Z ↦ funext fun u ↦ propext ⟨?_, ?_⟩

Premises used: funext, Iff.intro, propext
-- 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 : Presieve.{v₁, u₁} X
Z Y : D
Y_1 : C
u : Y_1 ⟶ X
hu : s u
w : Z ⟶ F.obj Y_1
⊢ Presieve.functorPushforward F s (w ≫ F.map u)

Tactic:
⟨_, _, _, hu, rfl⟩

Premises used: And.intro, Exists.intro, CategoryTheory.Presieve.functorPushforward, 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 : C
s : Presieve.{v₁, u₁} X
Z Y : D
Y_1 : C
u : Y_1 ⟶ X
hu : s u
w : Z ⟶ F.obj Y_1
⊢ Presieve.functorPushforward F s (w ≫ F.map u)

Tactic:
exact ⟨_, _, _, hu, 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 : C
s : Presieve.{v₁, u₁} X
Z : D
w : C
w_1 : w ⟶ X
w_2 : Z ⟶ F.obj w
hu : s w_1
⊢ (generate (Presieve.map F s)).arrows (w_2 ≫ F.map w_1)

Tactic:
⟨_, _, _, ⟨hu⟩, rfl⟩

Premises used: And.intro, Exists.intro, CategoryTheory.Presieve.map.of, 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 : C
s : Presieve.{v₁, u₁} X
Z : D
w : C
w_1 : w ⟶ X
w_2 : Z ⟶ F.obj w
hu : s w_1
⊢ (generate (Presieve.map F s)).arrows (w_2 ≫ F.map w_1)

Tactic:
exact ⟨_, _, _, ⟨hu⟩, 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_1 : C
f_1 : Y_1 ⟶ X
S_1 R_1 : Sieve.{v₁, u₁} X
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve.{v₁, u₁} Y
Y Z W : C
f : Y ⟶ W
h : W ⟶ X
hh : S h
hf : (R hh).arrows f
g : Z ⟶ Y
⊢ (fun (x : C) (x_1 : x ⟶ X) (h : S x_1) ↦ (R h).arrows) W h hh (g ≫ f) ∧ (g ≫ f) ≫ h = g ≫ f ≫ h

Tactic:
simp [hf]
-- 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_1 : C
f_1 : Y_1 ⟶ X
S_1 R_1 : Sieve.{v₁, u₁} X
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve.{v₁, u₁} Y
Y Z W : C
f : Y ⟶ W
h : W ⟶ X
hh : S h
hf : (R hh).arrows f
g : Z ⟶ Y
⊢ S.bind (fun (x : C) (x_1 : x ⟶ X) (h : S x_1) ↦ (R h).arrows) (g ≫ f ≫ h)

Tactic:
exact ⟨_, g ≫ f, _, hh, by simp [hf]⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Presieve.{v₁, u₁} X
S : Sieve.{v₁, u₁} X
ss : R ≤ S.arrows
Y Z : C
f : Y ⟶ Z
g : Z ⟶ X
hg : R g
⊢ S.arrows (f ≫ g)

Tactic:
S.downward_closed (ss Z _ hg) f

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Presieve.{v₁, u₁} X
S : Sieve.{v₁, u₁} X
ss : R ≤ S.arrows
Y Z : C
f : Y ⟶ Z
g : Z ⟶ X
hg : R g
⊢ S.arrows (f ≫ g)

Tactic:
exact S.downward_closed (ss Z _ hg) f

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Presieve.{v₁, u₁} X
⊢ R ≤ (generate R).arrows

Tactic:
giGenerate.gc.le_u_l R

Premises used: CategoryTheory.Sieve.giGenerate, GaloisConnection.le_u_l, GaloisInsertion.gc
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
⊢ generate S.arrows = S

Tactic:
giGenerate.l_u_eq S

Premises used: CategoryTheory.Sieve.giGenerate, GaloisInsertion.l_u_eq
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Monotone (α := Presieve.{v₁, u₁} X) generate

Tactic:
(giGenerate (X := X)).gc.monotone_l

Premises used: CategoryTheory.Sieve.giGenerate, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
h : S.arrows (𝟙 X)
Y : C
f : Y ⟶ X
h_1 : arrows ⊤ f
⊢ S.arrows f

Tactic:
simpa using downward_closed _ h f

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
R : Presieve.{v₁, u₁} X
f : Y ⟶ X
inst_1 : IsSplitEpi f
hf : R f
rw : (generate R).arrows (𝟙 X)
⊢ generate R = ⊤

Tactic:
rw [← id_mem_iff_eq_top]

Premises used: CategoryTheory.Sieve.id_mem_iff_eq_top
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
R : Presieve.{v₁, u₁} X
f : Y ⟶ X
inst_1 : IsSplitEpi f
hf : R f
⊢ section_ f ≫ f = 𝟙 X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
R : Presieve.{v₁, u₁} X
f : Y ⟶ X
inst_1 : IsSplitEpi f
hf : R f
⊢ (generate R).arrows (𝟙 X)

Tactic:
exact ⟨_, section_ f, f, hf, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst_1 : IsSplitEpi f
⊢ generate (Presieve.singleton f) = ⊤

Tactic:
generate_of_contains_isSplitEpi f (Presieve.singleton_self _)

Premises used: CategoryTheory.Presieve.singleton_self, CategoryTheory.Sieve.generate_of_contains_isSplitEpi
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq (α := Sieve.{v₁, u₁} X) (generate ⊤) ⊤

Tactic:
generate_of_contains_isSplitEpi (𝟙 _) ⟨⟩

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Sieve.generate_of_contains_isSplitEpi, True.intro
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq (α := Sieve.{v₁, u₁} X) (generate ⊥) ⊥

Tactic:
simp only [eq_bot_iff, generate_le_iff, bot_le]

Premises used: eq_bot_iff, CategoryTheory.Sieve.generate_le_iff, bot_le
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Presieve.{v₁, u₁} X
⊢ generate R = ⊥ ↔ R = ⊥

Tactic:
simp [giGenerate.gc.l_eq_bot]

Premises used: CategoryTheory.Sieve.giGenerate, GaloisConnection.l_eq_bot, GaloisInsertion.gc
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst_1 : IsIso i
S : Sieve.{v₁, u₁} Z
⊢ S.arrows (i ≫ f) ↔ S.arrows f

Tactic:
⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩

Premises used: CategoryTheory.Sieve.downward_closed, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst_1 : IsIso i
S : Sieve.{v₁, u₁} Z
refine : ∀ (H : S.arrows (i ≫ f)), S.arrows f
⊢ S.arrows (i ≫ f) ↔ S.arrows f

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst_1 : IsIso i
S : Sieve.{v₁, u₁} Z
H : S.arrows (i ≫ f)
⊢ S.arrows (inv i ≫ i ≫ f)

Tactic:
S.downward_closed H (inv i)

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst_1 : IsIso i
S : Sieve.{v₁, u₁} Z
H : S.arrows (i ≫ f)
h : f = inv i ≫ i ≫ f
⊢ S.arrows f

Tactic:
convert! S.downward_closed H (inv i)

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst_1 : IsIso i
S : Sieve.{v₁, u₁} Z
H : S.arrows (i ≫ f)
⊢ f = inv i ≫ i ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
i : I
⊢ 𝟙 (Y i) ≫ f i = f i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
mp : (ofArrows Y f).arrows g → ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
mpr : (∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i) → (ofArrows Y f).arrows g
⊢ (ofArrows Y f).arrows g ↔ ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y_1 : I → C
f : (i : I) → Y_1 i ⟶ X
W Y : C
i : I
a : W ⟶ Y_1 i
⊢ ∃ (i_1 : I) (a_1 : W ⟶ Y_1 i_1), a ≫ f i = a_1 ≫ f i_1

Tactic:
⟨i, a, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y_1 : I → C
f : (i : I) → Y_1 i ⟶ X
W Y : C
i : I
a : W ⟶ Y_1 i
⊢ ∃ (i_1 : I) (a_1 : W ⟶ Y_1 i_1), a ≫ f i = a_1 ≫ f i_1

Tactic:
exact ⟨i, a, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
i : I
a : W ⟶ Y i
⊢ (ofArrows Y f).arrows (a ≫ f i)

Tactic:
apply downward_closed _ (ofArrows_mk Y f i)

Premises used: CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
obtain : ∀ ⦃Y_1 : C⦄ (i : I) (h : W ⟶ Y i), ∃ (i_1 : I) (h_1 : W ⟶ Y i_1), h ≫ f i = h_1 ≫ f i_1
⊢ ∃ (i : I) (h : W ⟶ Y i), g = h ≫ f i

Tactic:
obtain ⟨_, h, _, ⟨i⟩, rfl⟩ := hg

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y_1 : I → C
f : (i : I) → Y_1 i ⟶ X
W Y : C
i : I
h : W ⟶ Y_1 i
⊢ ∃ (i_1 : I) (h_1 : W ⟶ Y_1 i_1), h ≫ f i = h_1 ≫ f i_1

Tactic:
⟨i, h, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y_1 : I → C
f : (i : I) → Y_1 i ⟶ X
W Y : C
i : I
h : W ⟶ Y_1 i
⊢ ∃ (i_1 : I) (h_1 : W ⟶ Y_1 i_1), h ≫ f i = h_1 ≫ f i_1

Tactic:
exact ⟨i, h, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
⊢ h hg ≫ f (i hg) = g

Tactic:
(ofArrows.exists hg).choose_spec.choose_spec.symm

Premises used: Exists.choose_spec, CategoryTheory.Sieve.ofArrows.h, CategoryTheory.Sieve.ofArrows.exists, CategoryTheory.Sieve.ofArrows.i, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
⊢ (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom) =
    generate R

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
refine_1 :
  (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom) ≤
    generate R
refine_2 :
  generate R ≤
    ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom
⊢ (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom) =
    generate R

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
refine_1 :
  (Presieve.ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left)
      fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom) ≤
    (generate R).arrows
⊢ (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom) ≤
    generate R

Tactic:
rw [Sieve.generate_le_iff]

Premises used: CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
Y : C
f : Over.{v₁, u₁} S
hf : R f.hom
⊢ 𝟙
        (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom)
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom) f hf)).left ≫
      f.hom =
    (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom) f hf)).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
Y : C
f : Over.{v₁, u₁} S
hf : R f.hom
⊢ (generate R).arrows
    (ObjectProperty.FullSubcategory.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom) f hf)).hom

Tactic:
exact ⟨_, 𝟙 _, f.hom, hf, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
Y w : C
a : Y ⟶ w
b : w ⟶ S
h : R b
⊢ arrows
    (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom)
    (a ≫ b)

Tactic:
⟨_, _, _, .mk (ι := R.category) ⟨Over.mk b, h⟩, rfl⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Over.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
Y w : C
a : Y ⟶ w
b : w ⟶ S
h : R b
⊢ arrows
    (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom)
    (a ≫ b)

Tactic:
exact ⟨_, _, _, .mk (ι := R.category) ⟨Over.mk b, h⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Sieve.{v₁, u₁} S
rw : generate R.arrows = R
rw₁ rw₂ : R = R
⊢ (ofArrows (fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R.arrows f.hom).left)
      fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R.arrows f.hom).hom) =
    R

Tactic:
rw [ofArrows_category', generate_sieve]

Premises used: CategoryTheory.Sieve.ofArrows_category', CategoryTheory.Sieve.generate_sieve
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Sieve.{v₁, u₁} X
⊢ ∃ (I : Type (max u₁ v₁)) (Y : I → C) (f : (i : I) → Y i ⟶ X), R = ofArrows Y f

Tactic:
⟨_, _, _, (ofArrows_category R).symm⟩

Premises used: CategoryTheory.Sieve.ofArrows_category, Exists.intro, Eq.symm
-- 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_1 Y_1 Z : C
f_1 : Y_1 ⟶ X_1
S R : Sieve.{v₁, u₁} X_1
I : Type u_1
Y : I → C
X Z₁ Z₂ : C
p : Z₁ ⟶ X
i : I
f : Z₁ ⟶ Y i
g : Z₂ ⟶ Z₁
⊢ ∃ (i : I), Nonempty.{v₁ + 1} (Z₂ ⟶ Y i)

Tactic:
⟨i, ⟨g ≫ f⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.CategoryStruct.comp
-- 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_1 Y_1 Z : C
f_1 : Y_1 ⟶ X_1
S R : Sieve.{v₁, u₁} X_1
I : Type u_1
Y : I → C
X Z₁ Z₂ : C
p : Z₁ ⟶ X
i : I
f : Z₁ ⟶ Y i
g : Z₂ ⟶ Z₁
⊢ ∃ (i : I), Nonempty.{v₁ + 1} (Z₂ ⟶ Y i)

Tactic:
exact ⟨i, ⟨g ≫ f⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
Z X : C
g : Z ⟶ X
⊢ arrows (ofObjects Y X) g ↔ ∃ (i : I), Nonempty.{v₁ + 1} (Z ⟶ Y i)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
⊢ ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i

Tactic:
rw [mem_ofArrows_iff] at hg

Premises used: CategoryTheory.Sieve.mem_ofArrows_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
obtain : ∀ (i : I) (a : W ⟶ Y i), arrows (ofObjects Y X) (a ≫ f i)
⊢ arrows (ofObjects Y X) g

Tactic:
obtain ⟨i, a, rfl⟩ := hg

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
i : I
a : W ⟶ Y i
⊢ arrows (ofObjects Y X) (a ≫ f i)

Tactic:
⟨i, ⟨a⟩⟩

Premises used: Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
i : I
a : W ⟶ Y i
⊢ arrows (ofObjects Y X) (a ≫ f i)

Tactic:
exact ⟨i, ⟨a⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsTerminal.{v₁, u₁} X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
⊢ ofArrows Y f = ofObjects Y X

Tactic:
le_antisymm (ofArrows_le_ofObjects Y f) (fun W g => ?_)

Premises used: le_antisymm, CategoryTheory.Sieve.ofArrows_le_ofObjects