awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
choose :
  ∀ (κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v))
    (W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C)
    (p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y)
    (hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)),
    (ofArrows Z g).bind Ti ∈ J.coverings X
⊢ (ofArrows Z g).bind Ti ∈ J.coverings X

Tactic:
choose κ W p hp using fun ⦃Y⦄ (f : Y ⟶ X) hf ↦ (Ti f hf).exists_eq_ofArrows

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
a :
  (ofArrows Z g).bind Ti ≤
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))
a₁ :
  (ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ≤
    (ofArrows Z g).bind Ti
⊢ (ofArrows Z g).bind Ti =
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
T Y : C
i : ι
v : T ⟶ Z i
hv : Ti (g i) ⋯ v
⊢ ofArrows (ι := κ (g i) ⋯) (W (g i) ⋯) (p (g i) ⋯) v

Tactic:
rw [hp] at hv
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
T Y : C
i : ι
v : T ⟶ Z i
hv : ofArrows (ι := κ (g i) ⋯) (W (g i) ⋯) (p (g i) ⋯) v
a :
  ∀ ⦃Y : C⦄ (j : κ (g i) ⋯),
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
          g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g i) ⋯ j ≫ g i)
⊢ ofArrows
    (fun (ij : (i : ι) × κ (g i) ⋯) ↦
      W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
    (fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
    (v ≫ g i)

Tactic:
obtain ⟨j⟩ := hv
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y_1 : C
i : ι
Y : C
j : κ (g i) ⋯
⊢ ofArrows
    (fun (ij : (i : ι) × κ (g i) ⋯) ↦
      W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
    (fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
    (p (g i) ⋯ j ≫ g i)

Tactic:
.mk <| Sigma.mk (β := fun i : ι ↦ κ (g i) ⟨i⟩) i j

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sigma.mk
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y_1 : C
i : ι
Y : C
j : κ (g i) ⋯
⊢ ofArrows
    (fun (ij : (i : ι) × κ (g i) ⋯) ↦
      W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
    (fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
    (p (g i) ⋯ j ≫ g i)

Tactic:
exact .mk <| Sigma.mk (β := fun i : ι ↦ κ (g i) ⟨i⟩) i j

Premises used: Sigma.mk
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y : C
ij : (i : ι) × κ (g i) ⋯
h :
  Ti (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (Y :=
      W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯))) ∧
    Eq (α := W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ⟶ X)
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
⊢ (ofArrows Z g).bind Ti (Y := W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
    (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
      g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))

Tactic:
use Z ij.1, p (g ij.1) ⟨ij.1⟩ ij.2, g ij.1, ⟨ij.1⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sigma.fst, Sigma.snd
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y : C
ij : (i : ι) × κ (g i) ⋯
h :
  ofArrows (W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯) (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯) (Y :=
      W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯))) ∧
    Eq (α := W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ⟶ X)
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
⊢ Ti (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (Y :=
      W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯))) ∧
    Eq (α := W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ⟶ X)
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))

Tactic:
rw [hp]
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y : C
ij : (i : ι) × κ (g i) ⋯
⊢ ofArrows (W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯) (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯) (Y :=
      W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯))) ∧
    Eq (α := W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ⟶ X)
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))

Tactic:
⟨⟨_⟩, rfl⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, And.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y : C
ij : (i : ι) × κ (g i) ⋯
⊢ ofArrows (W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯) (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯) (Y :=
      W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯))) ∧
    Eq (α := W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ⟶ X)
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))
      (p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯)))

Tactic:
exact ⟨⟨_⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows Z g).bind Ti =
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))

Tactic:
have : (Presieve.ofArrows Z g).bind Ti =
        .ofArrows (fun ij : Σ i, κ (g i) ⟨i⟩ ↦ W _ _ ij.2) (fun ij ↦ p _ _ ij.2 ≫ g ij.1) := by
      apply le_antisymm
      · rintro T u ⟨S, v, w, ⟨i⟩, hv, rfl⟩
        rw [hp] at hv
        obtain ⟨j⟩ := hv
        exact .mk <| Sigma.mk (β := fun i : ι ↦ κ (g i) ⟨i⟩) i j
      · rintro T u ⟨ij⟩
        use Z ij.1, p (g ij.1) ⟨ij.1⟩ ij.2, g ij.1, ⟨ij.1⟩
        rw [hp]
        exact ⟨⟨_⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this :
  (ofArrows Z g).bind Ti =
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))
rw :
  (ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ∈
    J.coverings X
⊢ (ofArrows Z g).bind Ti ∈ J.coverings X

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this :
  (ofArrows Z g).bind Ti =
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))
⊢ (ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ∈
    J.coverings X

Tactic:
J.comp_mem_coverings (Y := fun (i : ι) (j : κ (g i) ⟨i⟩) ↦ W _ _ j)
      (g := fun i j ↦ p _ _ j) _ hR fun i ↦ ?_

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Precoverage.comp_mem_coverings
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this :
  (ofArrows Z g).bind Ti =
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))
refine :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v, u} (Z i))) (J.coverings (Z i))
      (ofArrows (ι := κ (g i) ⋯) ((fun (i : ι) (j : κ (g i) ⋯) ↦ W (g i) ⋯ j) i)
        ((fun (i : ι) (j : κ (g i) ⋯) ↦ p (g i) ⋯ j) i))
⊢ (ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ∈
    J.coverings X

Tactic:
refine J.comp_mem_coverings (Y := fun (i : ι) (j : κ (g i) ⟨i⟩) ↦ W _ _ j)
      (g := fun i j ↦ p _ _ j) _ hR fun i ↦ ?_

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Precoverage.comp_mem_coverings
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this :
  (ofArrows Z g).bind Ti =
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))
i : ι
rw : Membership.mem (γ := Set (Presieve.{v, u} (Z i))) (J.coverings (Z i)) (Ti (g i) ⋯)
⊢ Membership.mem (γ := Set (Presieve.{v, u} (Z i))) (J.coverings (Z i))
    (ofArrows (ι := κ (g i) ⋯) ((fun (i : ι) (j : κ (g i) ⋯) ↦ W (g i) ⋯ j) i)
      ((fun (i : ι) (j : κ (g i) ⋯) ↦ p (g i) ⋯ j) i))

Tactic:
rw [← hp]