awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
⊢ arrows (functorPullback (𝟭 C) R) f ↔ R.arrows f

Tactic:
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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₃, u₃} ((F ⋙ G).obj X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), (functorPullback (F ⋙ G) R).arrows f ↔ (functorPullback F (functorPullback G R)).arrows f
⊢ functorPullback (F ⋙ G) R = functorPullback F (functorPullback G R)

Tactic:
ext
-- 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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₃, u₃} ((F ⋙ G).obj X)
Y : C
f : Y ⟶ X
⊢ (functorPullback (F ⋙ G) R).arrows f ↔ (functorPullback F (functorPullback G R)).arrows f

Tactic:
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
R : Presieve.{v₂, u₂} (F.obj X)
rw : Presieve.functorPullback F R ≤ (functorPullback F (generate R)).arrows
⊢ generate (Presieve.functorPullback F R) ≤ functorPullback F (generate R)

Tactic:
rw [generate_le_iff]

Premises used: CategoryTheory.Sieve.generate_le_iff
-- 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 : Presieve.{v₂, u₂} (F.obj X)
Z : C
g : Z ⟶ X
hg : Presieve.functorPullback F R g
⊢ (functorPullback F (generate R)).arrows g

Tactic:
le_generate _ _ _ hg

Premises used: CategoryTheory.Sieve.le_generate, CategoryTheory.Presieve.functorPullback
-- 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 : Presieve.{v₂, u₂} (F.obj X)
Z : C
g : Z ⟶ X
hg : Presieve.functorPullback F R g
⊢ (functorPullback F (generate R)).arrows g

Tactic:
exact le_generate _ _ _ hg

Premises used: CategoryTheory.Sieve.le_generate
-- 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 : C
f : X ⟶ Y
S : Sieve.{v₂, u₂} (F.obj Y)
h :
  ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ X),
    (functorPullback F (pullback (F.map f) S)).arrows f_1 ↔ (pullback f (functorPullback F S)).arrows f_1
⊢ functorPullback F (pullback (F.map f) S) = pullback f (functorPullback F S)

Tactic:
ext
-- 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 : C
f : X ⟶ Y
S : Sieve.{v₂, u₂} (F.obj Y)
Y_1 : C
f_1 : Y_1 ⟶ X
⊢ (functorPullback F (pullback (F.map f) S)).arrows f_1 ↔ (pullback f (functorPullback F S)).arrows f_1

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
R : Presieve.{v₁, u₁} X
h :
  ∀ (Y : D),
    Eq (α := (Y ⟶ F.obj X) → Prop) (Presieve.functorPushforward F (generate R).arrows) (Presieve.functorPushforward F R)
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R

Tactic:
funext Y
-- 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 : Presieve.{v₁, u₁} X
Y : D
h : ∀ (f : Y ⟶ F.obj X), Presieve.functorPushforward F (generate R).arrows f ↔ Presieve.functorPushforward F R f
⊢ Eq (α := (Y ⟶ F.obj X) → Prop) (Presieve.functorPushforward F (generate R).arrows) (Presieve.functorPushforward F R)

Tactic:
ext f
-- 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 : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
h : Presieve.functorPushforward F (generate R).arrows f → Presieve.functorPushforward F R f
h₁ : Presieve.functorPushforward F R f → Presieve.functorPushforward F (generate R).arrows f
⊢ Presieve.functorPushforward F (generate R).arrows f ↔ Presieve.functorPushforward F R f

Tactic:
constructor
-- 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 : Presieve.{v₁, u₁} X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ f' ≫ F.map (g' ≫ f'') = (f' ≫ F.map g') ≫ F.map 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 : C
R : Presieve.{v₁, u₁} X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ Presieve.functorPushforward F R (f' ≫ F.map (g' ≫ f''))

Tactic:
exact ⟨X'', f'', f' ≫ F.map g', h₁, 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
R : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
X' : C
g : X' ⟶ X
f' : Y ⟶ F.obj X'
h₁ : R g
h₂ : f = f' ≫ F.map g
⊢ Presieve.functorPushforward F (generate R).arrows f

Tactic:
⟨X', g, f', le_generate R _ _ h₁, h₂⟩

Premises used: CategoryTheory.Sieve.le_generate, And.intro, Exists.intro, CategoryTheory.Presieve.functorPushforward
-- 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 : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
X' : C
g : X' ⟶ X
f' : Y ⟶ F.obj X'
h₁ : R g
h₂ : f = f' ≫ F.map g
⊢ Presieve.functorPushforward F (generate R).arrows f

Tactic:
exact ⟨X', g, f', le_generate R _ _ 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 : 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₁} X
Y_1 : D
_ :
  ∀ {Z : D} {f : Y_1 ⟶ F.obj X},
    Presieve.functorPushforward F R.arrows f → ∀ (g : Z ⟶ Y_1), Presieve.functorPushforward F R.arrows (g ≫ f)
⊢ ∀ {Z : D} {f : Y_1 ⟶ F.obj X},
    Presieve.functorPushforward F R.arrows f → ∀ (g : Z ⟶ Y_1), Presieve.functorPushforward 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₁} X
Y_1 Z_1 : D
f : Y_1 ⟶ F.obj X
h : Presieve.functorPushforward F R.arrows f
g : Z_1 ⟶ Y_1
obtain :
  ∀ (X_1 : C) (α : X_1 ⟶ X) (β : Y_1 ⟶ F.obj X_1) (hα : R.arrows α),
    Presieve.functorPushforward F R.arrows (g ≫ β ≫ F.map α)
⊢ Presieve.functorPushforward F R.arrows (g ≫ f)

Tactic:
obtain ⟨X, α, β, hα, rfl⟩ := h

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

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_1 Y Z : C
f : Y ⟶ X_1
S R_1 : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₁, u₁} X_1
Y_1 Z_1 : D
g : Z_1 ⟶ Y_1
X : C
α : X ⟶ X_1
β : Y_1 ⟶ F.obj X
hα : R.arrows α
⊢ Presieve.functorPushforward F R.arrows (g ≫ β ≫ F.map α)

Tactic:
exact ⟨X, α, g ≫ β, hα, 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
h : ∀ ⦃Y : D⦄ (f : Y ⟶ F.obj X), (generate (Presieve.map F s)).arrows f ↔ (functorPushforward F (generate s)).arrows f
⊢ generate (Presieve.map F s) = functorPushforward F (generate s)

Tactic:
ext
-- 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
Y : D
f : Y ⟶ F.obj X
h : Presieve.functorPushforward F s f ↔ (functorPushforward F (generate s)).arrows f
⊢ (generate (Presieve.map F s)).arrows f ↔ (functorPushforward F (generate s)).arrows f

Tactic:
rw [arrows_generate_map_eq_functorPushforward]

Premises used: CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward
-- 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
Y : D
f : Y ⟶ F.obj X
⊢ Presieve.functorPushforward F s f ↔ (functorPushforward F (generate s)).arrows f

Tactic:
simp [functorPushforward_extend_eq]

Premises used: CategoryTheory.Sieve.functorPushforward_extend_eq
-- 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
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
rw : generate (Presieve.map F (Presieve.ofArrows Y f)) = ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)
rw₁ rw₂ :
  Eq (α := Sieve.{v₂, u₂} (F.obj X))
    (generate (Presieve.ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)))
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
⊢ functorPushforward F (ofArrows Y f) = ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)

Tactic:
rw [← generate_map_eq_functorPushforward, Presieve.map_ofArrows]

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

Tactic:
ext X f
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 : C
R : Sieve.{v₁, u₁} X_1
X : C
f : X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X_1
h : arrows (functorPushforward (𝟭 C) R) f → R.arrows f
h₁ : R.arrows f → arrows (functorPushforward (𝟭 C) R) f
⊢ arrows (functorPushforward (𝟭 C) R) f ↔ R.arrows f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 : C
R : Sieve.{v₁, u₁} X_1
X : C
f : X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X_1
hf : arrows (functorPushforward (𝟭 C) R) f
h :
  ∀ (X_2 : C) (g : X_2 ⟶ X_1) (h : X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X_2) (hg : R.arrows g),
    R.arrows (h ≫ Functor.map (𝟭 C) g)
⊢ R.arrows f

Tactic:
obtain ⟨X, g, h, hg, rfl⟩ := hf

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 : C
R : Sieve.{v₁, u₁} X_1
X_2 X : C
g : X ⟶ X_1
h : X_2 ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X
hg : R.arrows g
⊢ R.arrows (h ≫ Functor.map (𝟭 C) g)

Tactic:
R.downward_closed hg h

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 : C
R : Sieve.{v₁, u₁} X_1
X_2 X : C
g : X ⟶ X_1
h : X_2 ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X
hg : R.arrows g
⊢ R.arrows (h ≫ Functor.map (𝟭 C) g)

Tactic:
exact R.downward_closed hg h

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 : C
R : Sieve.{v₁, u₁} X_1
X : C
f : X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X_1
hf : R.arrows f
⊢ f = 𝟙 X ≫ Functor.map (𝟭 C) f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 : C
R : Sieve.{v₁, u₁} X_1
X : C
f : X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X_1
hf : R.arrows f
⊢ arrows (functorPushforward (𝟭 C) R) f

Tactic:
exact ⟨X, f, 𝟙 _, 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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₁, u₁} X
h :
  ∀ ⦃Y : E⦄ (f : Y ⟶ (F ⋙ G).obj X),
    (functorPushforward (F ⋙ G) R).arrows f ↔ (functorPushforward G (functorPushforward F R)).arrows f
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)

Tactic:
ext
-- 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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₁, u₁} X
Y : E
f : Y ⟶ (F ⋙ G).obj X
⊢ (functorPushforward (F ⋙ G) R).arrows f ↔ (functorPushforward G (functorPushforward F R)).arrows f

Tactic:
simp [R.arrows.functorPushforward_comp F G]

Premises used: CategoryTheory.Sieve.arrows, CategoryTheory.Presieve.functorPushforward_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 : C
R : Sieve.{v₁, u₁} X
S : Sieve.{v₂, u₂} (F.obj X)
mp : functorPushforward F R ≤ S → R ≤ functorPullback F S
mpr : R ≤ functorPullback F S → functorPushforward F R ≤ S
⊢ functorPushforward F R ≤ S ↔ R ≤ functorPullback F S

Tactic:
constructor
-- 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 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X_1
hf : R.arrows f
mp : (functorPushforward F R).arrows (F.map f)
⊢ (functorPullback F S).arrows f

Tactic:
apply hle
-- 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 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X_1
hf : R.arrows f
⊢ (functorPushforward F R).arrows (F.map f)

Tactic:
⟨X, f, 𝟙 _, hf, ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, And.intro, Exists.intro, CategoryTheory.Presieve.functorPushforward
-- 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 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X_1
hf : R.arrows f
mp : F.map f = 𝟙 (F.obj X) ≫ F.map f
⊢ (functorPushforward F R).arrows (F.map f)

Tactic:
refine ⟨X, f, 𝟙 _, 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_1 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X_1
hf : R.arrows f
mp mp₁ : F.map f = F.map f
⊢ F.map f = 𝟙 (F.obj X) ≫ F.map f

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_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 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : R ≤ functorPullback F S
Y : D
X : C
g : X ⟶ X_1
h : Y ⟶ F.obj X
hg : R.arrows g
mpr : S.arrows (F.map g)
⊢ S.arrows (h ≫ F.map g)

Tactic:
apply Sieve.downward_closed S

Premises used: CategoryTheory.Sieve.downward_closed
-- 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 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : R ≤ functorPullback F S
Y : D
X : C
g : X ⟶ X_1
h : Y ⟶ F.obj X
hg : R.arrows g
⊢ S.arrows (F.map g)

Tactic:
hle g hg

Premises used: CategoryTheory.Presieve.functorPullback
-- 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 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : R ≤ functorPullback F S
Y : D
X : C
g : X ⟶ X_1
h : Y ⟶ F.obj X
hg : R.arrows g
⊢ S.arrows (F.map g)

Tactic:
exact hle g hg
-- 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₁} X
R : Sieve.{v₂, u₂} (F.obj X)
⊢ functorPushforward F S ≤ R ↔ S ≤ functorPullback F R

Tactic:
(Sieve.functor_galoisConnection F X).le_iff_le

Premises used: GaloisConnection.le_iff_le, CategoryTheory.Sieve.functor_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 : C
⊢ Monotone (α := Sieve.{v₂, u₂} (F.obj X)) (functorPullback F)

Tactic:
(functor_galoisConnection F X).monotone_u

Premises used: GaloisConnection.monotone_u, CategoryTheory.Sieve.functor_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 : C
⊢ Monotone (α := Sieve.{v₁, u₁} X) (functorPushforward F)

Tactic:
(functor_galoisConnection F X).monotone_l

Premises used: CategoryTheory.Sieve.functor_galoisConnection, GaloisConnection.monotone_l
-- 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₁} X
⊢ R ≤ functorPullback F (functorPushforward F R)

Tactic:
(functor_galoisConnection F X).le_u_l _

Premises used: GaloisConnection.le_u_l, CategoryTheory.Sieve.functor_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 : C
R : Sieve.{v₂, u₂} (F.obj X)
⊢ functorPushforward F (functorPullback F R) ≤ R

Tactic:
(functor_galoisConnection F X).l_u_le _

Premises used: CategoryTheory.Sieve.functor_galoisConnection, GaloisConnection.l_u_le
-- 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 R : Sieve.{v₁, u₁} X
⊢ functorPushforward F (S ⊔ R) = functorPushforward F S ⊔ functorPushforward F R

Tactic:
(functor_galoisConnection F X).l_sup

Premises used: CategoryTheory.Sieve.functor_galoisConnection, GaloisConnection.l_sup
-- 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 R : Sieve.{v₂, u₂} (F.obj X)
⊢ functorPullback F (S ⊔ R) = functorPullback F S ⊔ functorPullback F R

Tactic:
rfl

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

Tactic:
rfl

Premises used: CategoryTheory.Sieve.inter, CategoryTheory.Presieve.functorPullback, CategoryTheory.Sieve.functorPullback, 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
⊢ Eq (α := Sieve.{v₂, u₂} (F.obj X)) (functorPushforward F ⊥) ⊥

Tactic:
(functor_galoisConnection F X).l_bot

Premises used: CategoryTheory.Sieve.functor_galoisConnection, GaloisConnection.l_bot
-- 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
⊢ Eq (α := Sieve.{v₂, u₂} (F.obj X)) (functorPushforward F ⊤) ⊤

Tactic:
(generate_sieve _).symm.trans ?_

Premises used: CategoryTheory.Sieve.generate_sieve, Eq.symm, Eq.trans
-- 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
refine : Eq (α := Sieve.{v₂, u₂} (F.obj X)) (generate (arrows (functorPushforward F ⊤))) ⊤
⊢ Eq (α := Sieve.{v₂, u₂} (F.obj X)) (functorPushforward F ⊤) ⊤

Tactic:
refine (generate_sieve _).symm.trans ?_

Premises used: CategoryTheory.Sieve.generate_sieve, Eq.symm, Eq.trans
-- 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
apply : arrows (functorPushforward F ⊤) (𝟙 (F.obj X))
⊢ Eq (α := Sieve.{v₂, u₂} (F.obj X)) (generate (arrows (functorPushforward F ⊤))) ⊤

Tactic:
apply generate_of_contains_isSplitEpi (𝟙 (F.obj X))

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.obj, CategoryTheory.Sieve.generate_of_contains_isSplitEpi
-- 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
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X) ≫ F.map (𝟙 X)

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
⊢ arrows (functorPushforward F ⊤) (𝟙 (F.obj X))

Tactic:
exact ⟨X, 𝟙 _, 𝟙 _, trivial, 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
⊢ Eq (α := Sieve.{v₁, u₁} X) (functorPullback F ⊥) ⊥

Tactic:
rfl

Premises used: CategoryTheory.Presieve.functorPullback, CategoryTheory.Sieve.functorPullback, 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
⊢ Eq (α := Sieve.{v₁, u₁} X) (functorPullback F ⊤) ⊤

Tactic:
rfl

Premises used: CategoryTheory.Presieve.functorPullback, CategoryTheory.Sieve.functorPullback, 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
R : Sieve.{v₁, u₁} X
V : C
f : V ⟶ X
h : R.arrows f
⊢ F.map f = 𝟙 (F.obj V) ≫ F.map 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 : C
f : Y ⟶ X
S : Sieve.{v₁, u₁} X
rw : pullback f S ≤ pullback f (functorPullback F (functorPushforward F S))
⊢ functorPushforward F (pullback f S) ≤ pullback (F.map f) (functorPushforward F S)

Tactic:
rw [Sieve.functorPushforward_le_iff_le_functorPullback, Sieve.functorPullback_pullback]

Premises used: CategoryTheory.Sieve.functorPullback_pullback, CategoryTheory.Sieve.functorPushforward_le_iff_le_functorPullback
-- 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 : C
f : Y ⟶ X
S : Sieve.{v₁, u₁} X
a : S ≤ functorPullback F (functorPushforward F S)
⊢ pullback f S ≤ pullback f (functorPullback F (functorPushforward F S))

Tactic:
apply Sieve.pullback_monotone

Premises used: CategoryTheory.Sieve.pullback_monotone