awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : ∀ (W : C) (g : W ⟶ X), arrows (ofObjects Y X) g → (ofArrows Y f).arrows g
⊢ ofArrows Y f = ofObjects Y X

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

Premises used: le_antisymm, CategoryTheory.Sieve.ofArrows_le_ofObjects
-- 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
W : C
g : W ⟶ X
rw : (∃ (i : I), Nonempty.{v₁ + 1} (W ⟶ Y i)) → ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
⊢ arrows (ofObjects Y X) g → (ofArrows Y f).arrows g

Tactic:
rw [mem_ofArrows_iff, mem_ofObjects_iff]

Premises used: CategoryTheory.Sieve.mem_ofObjects_iff, CategoryTheory.Sieve.mem_ofArrows_iff
-- 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
W : C
g : W ⟶ X
i : I
h : W ⟶ Y i
⊢ ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i

Tactic:
⟨i, h, hX.hom_ext _ _⟩

Premises used: Exists.intro, CategoryTheory.Limits.IsTerminal.hom_ext
-- 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
W : C
g : W ⟶ X
i : I
h : W ⟶ Y i
⊢ ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i

Tactic:
exact ⟨i, h, hX.hom_ext _ _⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : I → C
I' : Type u_2
X' : I' → C
Y : C
h : Set.range X ⊆ Set.range X'
Z : C
f : Z ⟶ Y
i : I
g : Z ⟶ X i
obtain : ∀ (i' : I') (h : X' i' = X i), arrows (ofObjects X' Y) f
⊢ arrows (ofObjects X' Y) f

Tactic:
obtain ⟨i', h⟩ := h ⟨i, 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 : I → C
I' : Type u_2
X' : I' → C
Y : C
h_1 : Set.range X ⊆ Set.range X'
Z : C
f : Z ⟶ Y
i : I
g : Z ⟶ X i
i' : I'
h : X' i' = X i
⊢ arrows (ofObjects X' Y) f

Tactic:
⟨i', ⟨h ▸ g⟩⟩

Premises used: Eq.rec, Nonempty.intro, Exists.intro, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : I → C
I' : Type u_2
X' : I' → C
Y : C
h_1 : Set.range X ⊆ Set.range X'
Z : C
f : Z ⟶ Y
i : I
g : Z ⟶ X i
i' : I'
h : X' i' = X i
⊢ arrows (ofObjects X' Y) f

Tactic:
exact ⟨i', ⟨h ▸ g⟩⟩
-- 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 : Sieve.{v₁, u₁} X
h : Y ⟶ X
S : Sieve.{v₁, u₁} X
Y_1 Z_1 : C
f_1 : Y_1 ⟶ Y
g : S.arrows (f_1 ≫ h)
⊢ ∀ (g : Z_1 ⟶ Y_1), S.arrows ((g ≫ f_1) ≫ h)

Tactic:
simp [g]
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
⊢ pullback (𝟙 X) S = S

Tactic:
simp [Sieve.ext_iff]

Premises used: CategoryTheory.Sieve.ext_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ pullback f ⊤ = ⊤

Tactic:
top_unique fun _ _ => id

Premises used: id, top_unique
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
S : Sieve.{v₁, u₁} X
⊢ pullback (g ≫ f) S = pullback g (pullback f S)

Tactic:
simp [Sieve.ext_iff]

Premises used: CategoryTheory.Sieve.ext_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
S R : Sieve.{v₁, u₁} X
⊢ pullback f (S ⊓ R) = pullback f S ⊓ pullback f R

Tactic:
simp [Sieve.ext_iff]

Premises used: CategoryTheory.Sieve.ext_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
rw :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X'),
    (pullback e.hom (ofArrows Z f)).arrows f_1 ↔ arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) f_1
⊢ pullback e.hom (ofArrows Z f) = ofArrows Z fun (i : I) ↦ f i ≫ e.inv

Tactic:
rw [Sieve.ext_iff]

Premises used: CategoryTheory.Sieve.ext_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
mp : (pullback e.hom (ofArrows Z f)).arrows a → arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) a
mpr : arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) a → (pullback e.hom (ofArrows Z f)).arrows a
⊢ (pullback e.hom (ofArrows Z f)).arrows a ↔ arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) a

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
Y : C
i : I
b : W ⟶ Z i
fac : b ≫ f i = a ≫ e.hom
⊢ b ≫ f i ≫ e.inv = a

Tactic:
simp [reassoc_of% fac]
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
Y : C
i : I
b : W ⟶ Z i
fac : b ≫ f i = a ≫ e.hom
⊢ arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) a

Tactic:
exact ⟨_, b, _, ⟨i⟩, by simp [reassoc_of% fac]⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W Y : C
i : I
a : W ⟶ Z i
⊢ a ≫ f i = (a ≫ f i ≫ e.inv) ≫ e.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W Y : C
i : I
a : W ⟶ Z i
⊢ (pullback e.hom (ofArrows Z f)).arrows (a ≫ f i ≫ e.inv)

Tactic:
exact ⟨_, a, _, ⟨i⟩, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
rw : S.arrows f ↔ (pullback f S).arrows (𝟙 Y)
rw₁ : S.arrows f ↔ S.arrows (𝟙 Y ≫ f)
rw₂ rw₃ : S.arrows f ↔ S.arrows f
⊢ S.arrows f ↔ pullback f S = ⊤

Tactic:
rw [← id_mem_iff_eq_top, pullback_apply, id_comp]

Premises used: CategoryTheory.Sieve.pullback_apply, CategoryTheory.Sieve.id_mem_iff_eq_top, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
⊢ S.arrows f → pullback f S = ⊤

Tactic:
(mem_iff_pullback_eq_top f).1

Premises used: CategoryTheory.Sieve.mem_iff_pullback_eq_top, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
h : ∀ ⦃Z : C⦄ (h : Z ⟶ X), arrows (ofObjects Y X) h ↔ arrows ⊤ h
⊢ Eq (α := Sieve.{v₁, u₁} X) (ofObjects Y X) ⊤

Tactic:
ext Z h
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
h₁ : arrows (ofObjects Y X) h
⊢ arrows (ofObjects Y X) h ↔ arrows ⊤ h

Tactic:
simp only [top_apply, iff_true]

Premises used: CategoryTheory.Sieve.top_apply, iff_true
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ ∃ (i : I), Nonempty.{v₁ + 1} (Z ⟶ Y i)

Tactic:
⟨i, ⟨h ≫ g⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ ∃ (i : I), Nonempty.{v₁ + 1} (Z ⟶ Y i)

Tactic:
exact ⟨i, ⟨h ≫ g⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : I → C
Y Z : C
f : Z ⟶ Y
h : ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Z), (pullback f (ofObjects X Y)).arrows f_1 ↔ arrows (ofObjects X Z) f_1
⊢ pullback f (ofObjects X Y) = ofObjects X Z

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : I → C
Y Z : C
f : Z ⟶ Y
Y_1 : C
f_1 : Y_1 ⟶ Z
⊢ (pullback f (ofObjects X Y)).arrows f_1 ↔ arrows (ofObjects X Z) f_1

Tactic:
simp [Sieve.ofObjects]

Premises used: CategoryTheory.Sieve.ofObjects
-- 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_1 : Sieve.{v₁, u₁} X
f : Y ⟶ X
R : Sieve.{v₁, u₁} Y
Y_1 Z_1 : C
f_2 : Y_1 ⟶ X
h_1 : ∃ (g : Y_1 ⟶ Y), g ≫ f = f_2 ∧ R.arrows g
h : Z_1 ⟶ Y_1
j : Y_1 ⟶ Y
k : j ≫ f = f_2
z : R.arrows j
⊢ (h ≫ j) ≫ f = h ≫ f_2

Tactic:
simp [k]
-- 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_1 : Sieve.{v₁, u₁} X
f : Y ⟶ X
R : Sieve.{v₁, u₁} Y
Y_1 Z_1 : C
f_2 : Y_1 ⟶ X
h_1 : ∃ (g : Y_1 ⟶ Y), g ≫ f = f_2 ∧ R.arrows g
h : Z_1 ⟶ Y_1
j : Y_1 ⟶ Y
k : j ≫ f = f_2
z : R.arrows j
⊢ R.arrows (h ≫ j)

Tactic:
simp [z]
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
R : Sieve.{v₁, u₁} Y
Z : C
g : Z ⟶ Y
hg : R.arrows g
f : Y ⟶ X
⊢ (pushforward f R).arrows (g ≫ f)

Tactic:
⟨g, rfl, hg⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve.{v₁, u₁} Z
W : C
h : W ⟶ X
h_1 : (pushforward (g ≫ f) R).arrows h
f₁ : W ⟶ Z
hq : f₁ ≫ g ≫ f = h
hf₁ : R.arrows f₁
⊢ (f₁ ≫ g) ≫ f = h

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve.{v₁, u₁} Z
W : C
h : W ⟶ X
h_1 : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
rw : y ≫ f = h ∧ R.arrows z
⊢ z ≫ g ≫ f = h ∧ R.arrows z

Tactic:
rw [← Category.assoc, hR]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve.{v₁, u₁} Z
W : C
h : W ⟶ X
h_1 : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
left : y ≫ f = h
right : R.arrows z
⊢ y ≫ f = h ∧ R.arrows z

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ GaloisConnection (pushforward f) (pullback f)

Tactic:
fun _ _ => ⟨fun hR _ g hg => hR _ ⟨g, rfl, hg⟩, fun hS _ _ ⟨h, hg, hh⟩ => hg ▸ hS h hh⟩

Premises used: _private.0.CategoryTheory.Sieve.galoisConnection.match_1, Eq.rec, CategoryTheory.Sieve.arrows, And.intro, Iff.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, rfl, GaloisConnection
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ Monotone (pullback f)

Tactic:
(galoisConnection f).monotone_u

Premises used: GaloisConnection.monotone_u, CategoryTheory.Sieve.galoisConnection
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ Monotone (pushforward f)

Tactic:
(galoisConnection f).monotone_l

Premises used: CategoryTheory.Sieve.galoisConnection, GaloisConnection.monotone_l
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Sieve.{v₁, u₁} Y
⊢ R ≤ pullback f (pushforward f R)

Tactic:
(galoisConnection f).le_u_l _

Premises used: GaloisConnection.le_u_l, CategoryTheory.Sieve.galoisConnection
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Sieve.{v₁, u₁} X
⊢ pushforward f (pullback f R) ≤ R

Tactic:
(galoisConnection f).l_u_le _

Premises used: CategoryTheory.Sieve.galoisConnection, GaloisConnection.l_u_le
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
S R : Sieve.{v₁, u₁} Y
⊢ pushforward f (S ⊔ R) = pushforward f S ⊔ pushforward f R

Tactic:
(galoisConnection f).l_sup

Premises used: CategoryTheory.Sieve.galoisConnection, GaloisConnection.l_sup
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ pullback f ⊥ = ⊥

Tactic:
rfl

Premises used: CategoryTheory.Sieve.pullback, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ pushforward f ⊥ = ⊥

Tactic:
(galoisConnection f).l_bot

Premises used: CategoryTheory.Sieve.galoisConnection, GaloisConnection.l_bot
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
S : Sieve.{v₁, u₁} Y
⊢ pushforward f S = ⊥ ↔ S = ⊥

Tactic:
simp [(galoisConnection f).l_eq_bot]

Premises used: GaloisConnection.l_eq_bot, CategoryTheory.Sieve.galoisConnection
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve.{v₁, u₁} Y
f : Y ⟶ X
h : S f
Z : C
g : Z ⟶ Y
hg : (R h).arrows g
⊢ (bind S R).arrows (g ≫ f)

Tactic:
⟨_, g, f, h, hg, rfl⟩

Premises used: CategoryTheory.Presieve.bind, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve.{v₁, u₁} Y
f : Y ⟶ X
h : S f
Z : C
g : Z ⟶ Y
hg : (R h).arrows g
⊢ (bind S R).arrows (g ≫ f)

Tactic:
exact ⟨_, g, f, h, hg, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve.{v₁, u₁} Y
f : Y ⟶ X
h : S f
rw : pushforward f (R h) ≤ bind S R
⊢ R h ≤ pullback f (bind S R)

Tactic:
rw [← galoisConnection f]

Premises used: CategoryTheory.Sieve.galoisConnection
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve.{v₁, u₁} Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R

Tactic:
apply pushforward_le_bind_of_mem

Premises used: CategoryTheory.Sieve.pushforward_le_bind_of_mem
-- 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
f : Y ⟶ X
inst_2 : Mono f
apply : ∀ (b : Sieve.{v₁, u₁} Y), pullback f (pushforward f b) ≤ b
⊢ GaloisCoinsertion (pushforward f) (pullback f)

Tactic:
apply (galoisConnection f).toGaloisCoinsertion

Premises used: GaloisConnection.toGaloisCoinsertion, CategoryTheory.Sieve.galoisConnection
-- 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_1 : C
f_1 : Y ⟶ X
S_1 R : Sieve.{v₁, u₁} X
f : Y ⟶ X
inst_2 : Mono f
S : Sieve.{v₁, u₁} Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ ≫ f = g ≫ f
hg₁ : S.arrows g₁
⊢ g₁ = g

Tactic:
rw [cancel_mono f] at hf

Premises used: CategoryTheory.cancel_mono
-- 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_1 : C
f_1 : Y ⟶ X
S_1 R : Sieve.{v₁, u₁} X
f : Y ⟶ X
inst_2 : Mono f
S : Sieve.{v₁, u₁} Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ ≫ f = g ≫ f
hg₁ : S.arrows g₁
hf₁ : g₁ = g
⊢ S.arrows g₁

Tactic:
rw [cancel_mono f] at hf

Premises used: CategoryTheory.cancel_mono
-- 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_1 : C
f_1 : Y ⟶ X
S_1 R : Sieve.{v₁, u₁} X
f : Y ⟶ X
inst_2 : Mono f
S : Sieve.{v₁, u₁} Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ = g
hg₁ rwa rwa₁ rwa₂ rwa₃ : S.arrows g₁
⊢ S.arrows g

Tactic:
rwa [← 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 : Sieve.{v₁, u₁} X
f : Y ⟶ X
inst_2 : IsSplitEpi f
apply : ∀ (b : Sieve.{v₁, u₁} X), b ≤ pushforward f (pullback f b)
⊢ GaloisInsertion (pushforward f) (pullback f)

Tactic:
apply (galoisConnection f).toGaloisInsertion

Premises used: GaloisConnection.toGaloisInsertion, CategoryTheory.Sieve.galoisConnection
-- 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_1 : C
f_1 : Y ⟶ X
S_1 R : Sieve.{v₁, u₁} X
f : Y ⟶ X
inst_2 : IsSplitEpi f
S : Sieve.{v₁, u₁} X
Z : C
g : Z ⟶ X
hg : S.arrows g
⊢ (g ≫ section_ f) ≫ f = g ∧ (pullback f S).arrows (g ≫ section_ f)

Tactic:
simpa
-- 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_1 : C
f_1 : Y ⟶ X
S_1 R : Sieve.{v₁, u₁} X
f : Y ⟶ X
inst_2 : IsSplitEpi f
S : Sieve.{v₁, u₁} X
Z : C
g : Z ⟶ X
hg : S.arrows g
⊢ (pushforward f (pullback f S)).arrows g

Tactic:
exact ⟨g ≫ section_ f, by simpa⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
h : ∀ ⦃W : C⦄ (g : W ⟶ Y), (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g
⊢ generate (Presieve.pullbackArrows f R) = pullback f (generate R)

Tactic:
ext W g
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W : C
g : W ⟶ Y
h : (generate (Presieve.pullbackArrows f R)).arrows g → (pullback f (generate R)).arrows g
h₁ : (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows g
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 Y W : C
g : W ⟶ X
hg : R g
h : W_1 ⟶ Limits.pullback g f
⊢ HasPullback g f

Tactic:
have := R.hasPullback f hg
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 Y W : C
g : W ⟶ X
hg : R g
h : W_1 ⟶ Limits.pullback g f
this : HasPullback g f
h₁ : (generate R).arrows ((h ≫ pullback.fst g f) ≫ g)
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd g f)

Tactic:
rw [Sieve.pullback_apply, assoc, ← pullback.condition, ← assoc]

Premises used: CategoryTheory.Sieve.pullback_apply, CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 Y W : C
g : W ⟶ X
hg : R g
h : W_1 ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows g

Tactic:
Sieve.le_generate R W _ hg

Premises used: CategoryTheory.Sieve.le_generate
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 Y W : C
g : W ⟶ X
hg : R g
h : W_1 ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows g

Tactic:
exact Sieve.le_generate R W _ hg

Premises used: CategoryTheory.Sieve.le_generate
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 Y W : C
g : W ⟶ X
hg : R g
h : W_1 ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows ((h ≫ pullback.fst g f) ≫ g)

Tactic:
exact Sieve.downward_closed _ (by exact Sieve.le_generate R W _ hg) (h ≫ pullback.fst g f)

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 : C
g : W_1 ⟶ Y
W : C
h : W_1 ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
⊢ HasPullback k f

Tactic:
have := R.hasPullback f hk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 : C
g : W_1 ⟶ Y
W : C
h : W_1 ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
this : HasPullback k f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g

Tactic:
⟨_, _, _, Presieve.pullbackArrows.mk _ _ hk, pullback.lift_snd _ _ comm⟩

Premises used: CategoryTheory.Limits.pullback.lift_snd, And.intro, Exists.intro, CategoryTheory.Presieve.pullbackArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 : C
g : W_1 ⟶ Y
W : C
h : W_1 ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
this : HasPullback k f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g

Tactic:
exact ⟨_, _, _, Presieve.pullbackArrows.mk _ _ hk, pullback.lift_snd _ _ comm⟩
-- 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_1 : Sieve.{v₁, u₁} X
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₂, u₂} (F.obj X)
Y_1 : C
_ :
  ∀ {Z : C} {f : Y_1 ⟶ X},
    Presieve.functorPullback F R.arrows f → ∀ (g : Z ⟶ Y_1), Presieve.functorPullback F R.arrows (g ≫ f)
⊢ ∀ {Z : C} {f : Y_1 ⟶ X},
    Presieve.functorPullback F R.arrows f → ∀ (g : Z ⟶ Y_1), Presieve.functorPullback F R.arrows (g ≫ f)

Tactic:
_
-- 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_1 : Sieve.{v₁, u₁} X
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₂, u₂} (F.obj X)
Y_1 Z_1 : C
f : Y_1 ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z_1 ⟶ Y_1
rw : R.arrows (F.map g ≫ F.map f)
⊢ R.arrows (F.map (g ≫ f))

Tactic:
rw [F.map_comp]

Premises used: CategoryTheory.Functor.map_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 Y Z : C
f_1 : Y ⟶ X
S R_1 : Sieve.{v₁, u₁} X
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₂, u₂} (F.obj X)
Y_1 Z_1 : C
f : Y_1 ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z_1 ⟶ Y_1
⊢ R.arrows (F.map g ≫ F.map f)

Tactic:
R.downward_closed hf (F.map g)

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.Functor.map
-- 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_1 : Sieve.{v₁, u₁} X
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₂, u₂} (F.obj X)
Y_1 Z_1 : C
f : Y_1 ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z_1 ⟶ Y_1
⊢ R.arrows (F.map g ≫ F.map f)

Tactic:
exact R.downward_closed hf (F.map g)

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.Functor.map
-- 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
R : Sieve.{v₂, u₂} (F.obj X)
⊢ (functorPullback F R).arrows = Presieve.functorPullback F R.arrows

Tactic:
rfl

Premises used: CategoryTheory.Presieve.functorPullback, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Sieve.{v₁, u₁} X
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), arrows (functorPullback (𝟭 C) R) f ↔ R.arrows f
⊢ functorPullback (𝟭 C) R = R

Tactic:
ext