awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
h :
  ∀ (Y : C),
    Eq (α := (Y ⟶ X) → Prop)
      ((ofArrows Z g).bind fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H))
      (ofArrows
        (fun (i : (i : ι) × j (g i) ⋯) ↦
          W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
        fun (ij : (i : ι) × j (g i) ⋯) ↦
        k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
          g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
⊢ ((ofArrows Z g).bind fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) =
    ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      fun (ij : (i : ι) × j (g i) ⋯) ↦
      k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))

Tactic:
funext Y
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
h :
  ∀ (f : Y ⟶ X),
    (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f ↔
      ofArrows
        (fun (i : (i : ι) × j (g i) ⋯) ↦
          W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
        (fun (ij : (i : ι) × j (g i) ⋯) ↦
          k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
            g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
        f
⊢ Eq (α := (Y ⟶ X) → Prop) ((ofArrows Z g).bind fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H))
    (ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      fun (ij : (i : ι) × j (g i) ⋯) ↦
      k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))

Tactic:
ext f
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
h :
  (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f →
    ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      (fun (ij : (i : ι) × j (g i) ⋯) ↦
        k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
          g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
      f
h₁ :
  ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      (fun (ij : (i : ι) × j (g i) ⋯) ↦
        k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
          g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
      f →
    (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f
⊢ (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f ↔
    ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      (fun (ij : (i : ι) × j (g i) ⋯) ↦
        k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
          g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
      f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y_1 : C
i : ι
Y : C
i' : j (g i) ⋯
⊢ ofArrows
    (fun (i : (i : ι) × j (g i) ⋯) ↦
      W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
    (fun (ij : (i : ι) × j (g i) ⋯) ↦
      k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
    (k (g i) ⋯ i' ≫ g i)

Tactic:
ofArrows.mk (Sigma.mk _ _)

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sigma.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y_1 : C
i : ι
Y : C
i' : j (g i) ⋯
⊢ ofArrows
    (fun (i : (i : ι) × j (g i) ⋯) ↦
      W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
    (fun (ij : (i : ι) × j (g i) ⋯) ↦
      k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
    (k (g i) ⋯ i' ≫ g i)

Tactic:
exact ofArrows.mk (Sigma.mk _ _)

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sigma.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
i : (i : ι) × j (g i) ⋯
⊢ (ofArrows Z g).bind fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H) (Y :=
    W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
    (k (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
      g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯)))

Tactic:
bind_comp _ (ofArrows.mk _) (ofArrows.mk _)

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.bind_comp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
i : (i : ι) × j (g i) ⋯
⊢ (ofArrows Z g).bind fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H) (Y :=
    W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
    (k (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
      g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯)))

Tactic:
exact bind_comp _ (ofArrows.mk _) (ofArrows.mk _)

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.bind_comp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
g : Z ⟶ X
hg : ofArrows Y f g
obtain : ∀ ⦃Y_1 : C⦄ (i : ι), ∃ (i_1 : ι) (h : Y i_1 = Y i), f i = eqToHom ⋯ ≫ f i_1
⊢ ∃ (i : ι) (h : Y i = Z), g = eqToHom ⋯ ≫ f i

Tactic:
obtain ⟨i⟩ := hg
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
Y : C
i : ι
⊢ f i = eqToHom ⋯ ≫ f i

Tactic:
simp only [eqToHom_refl, id_comp]

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

Tactic:
exact ⟨i, rfl, by simp only [eqToHom_refl, id_comp]⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Presieve.{v₁, u₁} X
ι : Type (max 0 u₁ v₁) := { x : (Z : C) × (Z ⟶ X) // R (x.snd (β := fun (Z : C) ↦ Z ⟶ X)) }
h :
  R =
    ofArrows (fun (x : ι) ↦ (↑x : (Z : C) × (Z ⟶ X)).fst (β := fun (Z : C) ↦ Z ⟶ X)) fun (x : ι) ↦
      (↑x : (Z : C) × (Z ⟶ X)).snd (β := fun (Z : C) ↦ Z ⟶ X)
⊢ ∃ (ι : Type (max u₁ v₁)) (Y : ι → C) (f : (i : ι) → Y i ⟶ X), R = ofArrows Y f

Tactic:
use ι, fun x ↦ x.1.1, fun x ↦ x.1.2
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Presieve.{v₁, u₁} X
ι : Type (max 0 u₁ v₁) := { x : (Z : C) × (Z ⟶ X) // R (x.snd (β := fun (Z : C) ↦ Z ⟶ X)) }
⊢ R =
    ofArrows (fun (x : ι) ↦ (↑x : (Z : C) × (Z ⟶ X)).fst (β := fun (Z : C) ↦ Z ⟶ X)) fun (x : ι) ↦
      (↑x : (Z : C) × (Z ⟶ X)).snd (β := fun (Z : C) ↦ Z ⟶ X)

Tactic:
le_antisymm (fun Z g hg ↦ .mk (⟨⟨_, _⟩, hg⟩ : ι)) fun Z g ⟨x⟩ ↦ x.2

Premises used: _private.0.CategoryTheory.Presieve.exists_eq_ofArrows.match_1, le_antisymm, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Presieve.{v₁, u₁} X
ι : Type (max 0 u₁ v₁) := { x : (Z : C) × (Z ⟶ X) // R (x.snd (β := fun (Z : C) ↦ Z ⟶ X)) }
⊢ R =
    ofArrows (fun (x : ι) ↦ (↑x : (Z : C) × (Z ⟶ X)).fst (β := fun (Z : C) ↦ Z ⟶ X)) fun (x : ι) ↦
      (↑x : (Z : C) × (Z ⟶ X)).snd (β := fun (Z : C) ↦ Z ⟶ X)

Tactic:
exact le_antisymm (fun Z g hg ↦ .mk (⟨⟨_, _⟩, hg⟩ : ι)) fun Z g ⟨x⟩ ↦ x.2

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
⊢ (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) =
    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) ≤
    R
refine_2 :
  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) =
    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
Y : C
X : Over.{v₁, u₁} S
h : R X.hom
⊢ R
    (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) X h)).hom

Tactic:
h
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
Y : C
X : Over.{v₁, u₁} S
h : R X.hom
⊢ R
    (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) X h)).hom

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
X : C
g : X ⟶ S
hg : R g
⊢ 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) g

Tactic:
.mk (ι := R.category) ⟨Over.mk g, hg⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Over.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
X : C
g : X ⟶ S
hg : R g
⊢ 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) g

Tactic:
exact .mk (ι := R.category) ⟨Over.mk g, hg⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
hf : ofArrows X f g
⊢ X hf.idx = Y

Tactic:
(ofArrows_surj _ _ hf).choose_spec.1

Premises used: Exists.choose_spec, CategoryTheory.Presieve.ofArrows_surj, CategoryTheory.Presieve.ofArrows.idx
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
hf : ofArrows X f g
⊢ g = eqToHom ⋯ ≫ f hf.idx

Tactic:
(Presieve.ofArrows_surj _ _ hf).choose_spec.2

Premises used: Exists.choose_spec, CategoryTheory.Presieve.ofArrows_surj, CategoryTheory.Presieve.ofArrows.idx
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
hf : ofArrows X f g
⊢ f hf.idx = eqToHom ⋯ ≫ g

Tactic:
simp [eq_eqToHom_comp_hom_idx hf]

Premises used: CategoryTheory.Presieve.ofArrows.eq_eqToHom_comp_hom_idx
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
a : σ → ι
Y : C
i : σ
⊢ ofArrows Y_1 f (Y := (Y_1 ∘ a) i) (f (a i))

Tactic:
use a i
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
a : σ → ι
ha : Function.Surjective a
⊢ (ofArrows (Y ∘ a) fun (i : σ) ↦ f (a i)) = ofArrows Y f

Tactic:
le_antisymm (ofArrows_comp_le f a) ?_

Premises used: CategoryTheory.Presieve.ofArrows_comp_le, le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
a : σ → ι
ha : Function.Surjective a
refine : ofArrows Y f ≤ ofArrows (Y ∘ a) fun (i : σ) ↦ f (a i)
⊢ (ofArrows (Y ∘ a) fun (i : σ) ↦ f (a i)) = ofArrows Y f

Tactic:
refine le_antisymm (ofArrows_comp_le f a) ?_

Premises used: CategoryTheory.Presieve.ofArrows_comp_le, le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
a : σ → ι
ha : Function.Surjective a
Y : C
i : ι
obtain : ∀ (j : σ), ofArrows (Y_1 ∘ a) fun (i : σ) ↦ f (a i) (Y := Y_1 (a j)) (f (a j))
⊢ ofArrows (Y_1 ∘ a) (fun (i : σ) ↦ f (a i)) (f i)

Tactic:
obtain ⟨j, rfl⟩ := ha i

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
a : σ → ι
ha : Function.Surjective a
Y : C
j : σ
⊢ ofArrows (Y_1 ∘ a) fun (i : σ) ↦ f (a i) (Y := Y_1 (a j)) (f (a j))

Tactic:
use j
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
R : Presieve.{v₁, u₁} X
⊢ ofArrows Y f ≤ R ↔ ∀ (i : ι), R (f i)

Tactic:
⟨fun hle i ↦ hle _ _ ⟨i⟩, fun h _ g ⟨i⟩ ↦ h i⟩

Premises used: _private.0.CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback.match_1, CategoryTheory.Presieve.ofArrows.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f = singleton (Y := Y default) (f default)

Tactic:
le_antisymm ?_ fun Y _ ⟨⟩ ↦ ⟨default⟩

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
refine : ofArrows Y f ≤ singleton (Y := Y default) (f default)
⊢ ofArrows Y f = singleton (Y := Y default) (f default)

Tactic:
refine le_antisymm ?_ fun Y _ ⟨⟩ ↦ ⟨default⟩

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
rw : ∀ (i : ι), singleton (Y := Y default) (f default) (f i)
⊢ ofArrows Y f ≤ singleton (Y := Y default) (f default)

Tactic:
rw [ofArrows_le_iff]

Premises used: CategoryTheory.Presieve.ofArrows_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
⊢ i = default

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
obtain : singleton (Y := Y default) (f default) (Y := Y default) (f default)
⊢ singleton (Y := Y default) (f default) (f i)

Tactic:
obtain rfl : i = default := Subsingleton.elim _ _

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ singleton (Y := Y default) (f default) (Y := Y default) (f default)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
rw rw₁ : singleton f = singleton f
⊢ (ofArrows (fun (x : PUnit.{u_1 + 1}) ↦ Y) fun (x : PUnit.{u_1 + 1}) ↦ f) = singleton f

Tactic:
rw [ofArrows_of_unique]

Premises used: CategoryTheory.Presieve.ofArrows_of_unique
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : IsEmpty ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
rw : ∀ (i : ι), ⊥ (f i)
⊢ ofArrows Y f = ⊥

Tactic:
rw [eq_bot_iff, ofArrows_le_iff]

Premises used: CategoryTheory.Presieve.ofArrows_le_iff, eq_bot_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : IsEmpty ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ∀ (i : ι), ⊥ (f i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
σ : ι → Type u_2
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
⊢ (bindOfArrows X f fun (i : ι) ↦ ofArrows (Y i) (g i)) =
    ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (p : (i : ι) × σ i) ↦
      g (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)) ≫ f (p.fst (β := fun (i : ι) ↦ σ i))

Tactic:
le_antisymm ?_ (fun _ _ ⟨p⟩ ↦ ⟨p.1, _, ⟨p.2⟩⟩)

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
σ : ι → Type u_2
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
refine :
  (bindOfArrows X f fun (i : ι) ↦ ofArrows (Y i) (g i)) ≤
    ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (p : (i : ι) × σ i) ↦
      g (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)) ≫ f (p.fst (β := fun (i : ι) ↦ σ i))
⊢ (bindOfArrows X f fun (i : ι) ↦ ofArrows (Y i) (g i)) =
    ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (p : (i : ι) × σ i) ↦
      g (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)) ≫ f (p.fst (β := fun (i : ι) ↦ σ i))

Tactic:
refine le_antisymm ?_ (fun _ _ ⟨p⟩ ↦ ⟨p.1, _, ⟨p.2⟩⟩)

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
σ : ι → Type u_2
Y_1 : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y_1 i j ⟶ X i
Y_2 : C
i : ι
Y : C
j : σ i
⊢ ofArrows (fun (p : (i : ι) × σ i) ↦ Y_1 (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
    (fun (p : (i : ι) × σ i) ↦
      g (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)) ≫ f (p.fst (β := fun (i : ι) ↦ σ i)))
    (g i j ≫ f i)

Tactic:
⟨Sigma.mk i j⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sigma.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
σ : ι → Type u_2
Y_1 : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y_1 i j ⟶ X i
Y_2 : C
i : ι
Y : C
j : σ i
⊢ ofArrows (fun (p : (i : ι) × σ i) ↦ Y_1 (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
    (fun (p : (i : ι) × σ i) ↦
      g (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)) ≫ f (p.fst (β := fun (i : ι) ↦ σ i)))
    (g i j ≫ f i)

Tactic:
exact ⟨Sigma.mk i j⟩
-- 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)
Y : C
f : Y ⟶ X
⊢ functorPullback F R f ↔ R (F.map f)

Tactic:
Iff.rfl

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

Tactic:
rfl

Premises used: CategoryTheory.Presieve.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 Y Z : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_2 : HasPullbacks.{v₁, u₁} C
⊢ R.HasPairwisePullbacks

Tactic:
⟨fun _ _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Presieve.HasPairwisePullbacks.mk
-- 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
α : Type v₂
X : α → C
B : C
π : (a : α) → X a ⟶ B
inst_2 : (ofArrows X π).HasPairwisePullbacks
a b : α
⊢ HasPullback (π a) (π b)

Tactic:
Presieve.HasPairwisePullbacks.has_pullbacks (Presieve.ofArrows.mk _) (Presieve.ofArrows.mk _)

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.HasPairwisePullbacks.has_pullbacks
-- 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 (α := Presieve.{v₁, u₁} X) (functorPushforward F)

Tactic:
fun _ _ hle _ _ ⟨Z, g, u, hg, hf⟩ ↦ ⟨Z, g, u, hle _ _ hg, hf⟩

Premises used: _private.0.CategoryTheory.Presieve.functorPushforward_monotone.match_1, Monotone, 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_1 : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z : C
f_1 : Y_1 ⟶ X
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
F : Functor.{v₁, v₂, u₁, u₂} C D
S : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
h : functorPushforward F S f
choose :
  (Z : C) → (f' : Z ⟶ X) → (g : Y ⟶ F.obj Z) → (h₁ : S f') → (h : f = g ≫ F.map f') → FunctorPushforwardStructure F S f
⊢ FunctorPushforwardStructure F S f

Tactic:
choose Z f' g h₁ h using h