awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Membership.mem (γ := Set (Presieve.{v, u} (X i))) (J.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
ι' : Type (max u v) := (↑(Presieve.ofArrows X f).uncurry : Type (max u v))
σ' : (i : ι') → Type (max u v) :=
  fun (i : ι') ↦
    (↑(Presieve.uncurry (Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯)))) :
      Type (max u v))
α : Type (max u v) :=
  (↑(Presieve.uncurry
        (Presieve.ofArrows
          (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
          fun (x : (i : ι) × σ i) ↦
          g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i)))) :
    Type (max u v))
τ' : (a : α) → Type (max u v) :=
  fun (a : α) ↦
    (↑(Presieve.uncurry
          (Presieve.ofArrows (Y ((Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i)))
            (g ((Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i))))) :
      Type (max u v))
fib : (i : ι' ⊕ α) → Type (max u v) := fun (i : ι' ⊕ α) ↦ Sum.elim (fun (i : ι') ↦ σ' i) (fun (i : α) ↦ Unit ⊕ τ' i) i
incl : (p : ι' ⊕ α) → ι :=
  fun (p : ι' ⊕ α) ↦
    Sum.elim (fun (i : ι') ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : α) ↦ (Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i)) p
fibincl : (i : ι' ⊕ α) → (j : fib i) → σ (incl i) :=
  fun (i : ι' ⊕ α) (j : fib i) ↦
    match (motive := (i : ι' ⊕ α) → (j : fib i) → σ (incl i)) i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j =>
      Sum.elim (fun (x : Unit) ↦ (Presieve.ofArrows.idx ⋯).snd (β := fun (i : ι) ↦ σ i))
        (fun (i_2 : τ' i) ↦ Presieve.ofArrows.idx ⋯) j
i_1 : ι' ⊕ α
T : C
i : ι'
u : T ⟶ X (incl (Sum.inl i))
hu : Presieve.ofArrows (Y (incl (Sum.inl i))) (g (incl (Sum.inl i))) u
⊢ Presieve.ofArrows (fun (j : fib (Sum.inl i)) ↦ Y (incl (Sum.inl i)) (fibincl (Sum.inl i) j))
    ((fun (i : ι' ⊕ α) (j : fib i) ↦ g (incl i) (fibincl i j)) (Sum.inl i)) u

Tactic:
exact .mk' ⟨⟨_, _⟩, hu⟩ (by cat_disch) (by cat_disch)
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Membership.mem (γ := Set (Presieve.{v, u} (X i))) (J.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
ι' : Type (max u v) := (↑(Presieve.ofArrows X f).uncurry : Type (max u v))
σ' : (i : ι') → Type (max u v) :=
  fun (i : ι') ↦
    (↑(Presieve.uncurry (Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯)))) :
      Type (max u v))
α : Type (max u v) :=
  (↑(Presieve.uncurry
        (Presieve.ofArrows
          (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
          fun (x : (i : ι) × σ i) ↦
          g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i)))) :
    Type (max u v))
τ' : (a : α) → Type (max u v) :=
  fun (a : α) ↦
    (↑(Presieve.uncurry
          (Presieve.ofArrows (Y ((Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i)))
            (g ((Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i))))) :
      Type (max u v))
fib : (i : ι' ⊕ α) → Type (max u v) := fun (i : ι' ⊕ α) ↦ Sum.elim (fun (i : ι') ↦ σ' i) (fun (i : α) ↦ Unit ⊕ τ' i) i
incl : (p : ι' ⊕ α) → ι :=
  fun (p : ι' ⊕ α) ↦
    Sum.elim (fun (i : ι') ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : α) ↦ (Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i)) p
fibincl : (i : ι' ⊕ α) → (j : fib i) → σ (incl i) :=
  fun (i : ι' ⊕ α) (j : fib i) ↦
    match (motive := (i : ι' ⊕ α) → (j : fib i) → σ (incl i)) i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j =>
      Sum.elim (fun (x : Unit) ↦ (Presieve.ofArrows.idx ⋯).snd (β := fun (i : ι) ↦ σ i))
        (fun (i_2 : τ' i) ↦ Presieve.ofArrows.idx ⋯) j
i_1 : ι' ⊕ α
T : C
i : α
u : T ⟶ X (incl (Sum.inr i))
hu : Presieve.ofArrows (Y (incl (Sum.inr i))) (g (incl (Sum.inr i))) u
⊢ Presieve.ofArrows (fun (j : fib (Sum.inr i)) ↦ Y (incl (Sum.inr i)) (fibincl (Sum.inr i) j))
    ((fun (i : ι' ⊕ α) (j : fib i) ↦ g (incl i) (fibincl i j)) (Sum.inr i)) u

Tactic:
exact .mk' (.inr ⟨⟨_, _⟩, hu⟩) (by cat_disch) (by cat_disch)
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Membership.mem (γ := Set (Presieve.{v, u} (X i))) (J.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
ι' : Type (max u v) := (↑(Presieve.ofArrows X f).uncurry : Type (max u v))
σ' : (i : ι') → Type (max u v) :=
  fun (i : ι') ↦
    (↑(Presieve.uncurry (Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯)))) :
      Type (max u v))
α : Type (max u v) :=
  (↑(Presieve.uncurry
        (Presieve.ofArrows
          (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
          fun (x : (i : ι) × σ i) ↦
          g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i)))) :
    Type (max u v))
τ' : (a : α) → Type (max u v) :=
  fun (a : α) ↦
    (↑(Presieve.uncurry
          (Presieve.ofArrows (Y ((Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i)))
            (g ((Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i))))) :
      Type (max u v))
fib : (i : ι' ⊕ α) → Type (max u v) := fun (i : ι' ⊕ α) ↦ Sum.elim (fun (i : ι') ↦ σ' i) (fun (i : α) ↦ Unit ⊕ τ' i) i
incl : (p : ι' ⊕ α) → ι :=
  fun (p : ι' ⊕ α) ↦
    Sum.elim (fun (i : ι') ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : α) ↦ (Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i)) p
fibincl : (i : ι' ⊕ α) → (j : fib i) → σ (incl i) :=
  fun (i : ι' ⊕ α) (j : fib i) ↦
    match (motive := (i : ι' ⊕ α) → (j : fib i) → σ (incl i)) i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j =>
      Sum.elim (fun (x : Unit) ↦ (Presieve.ofArrows.idx ⋯).snd (β := fun (i : ι) ↦ σ i))
        (fun (i_1 : τ' i) ↦ Presieve.ofArrows.idx ⋯) j
i : ι' ⊕ α
T : C
u : T ⟶ X (incl i)
hu : Presieve.ofArrows (Y (incl i)) (g (incl i)) u
⊢ Presieve.ofArrows (fun (j : fib i) ↦ Y (incl i) (fibincl i j))
    ((fun (i : ι' ⊕ α) (j : fib i) ↦ g (incl i) (fibincl i j)) i) u

Tactic:
match i with
      | .inl i => exact .mk' ⟨⟨_, _⟩, hu⟩ (by cat_disch) (by cat_disch)
      | .inr i => exact .mk' (.inr ⟨⟨_, _⟩, hu⟩) (by cat_disch) (by cat_disch)
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
R : Presieve.{v, u} Y
hR : R ∈ J.coverings Y
inst_2 : R.HasPullbacks f
obtain :
  ∀ (ι : Type (max u v)) (Z : ι → C) (g : (i : ι) → Z i ⟶ Y) (hR : Presieve.ofArrows Z g ∈ J.coverings Y)
    [inst_3 : (Presieve.ofArrows Z g).HasPullbacks f], Presieve.pullbackArrows f (Presieve.ofArrows Z g) ∈ J.coverings X
⊢ Presieve.pullbackArrows f R ∈ J.coverings X

Tactic:
obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst_2 : (Presieve.ofArrows Z g).HasPullbacks f
⊢ ∀ (i : ι), Limits.HasPullback (g i) f

Tactic:
have (i : ι) : Limits.HasPullback (g i) f := Presieve.hasPullback f (Presieve.ofArrows.mk i)
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst_2 : (Presieve.ofArrows Z g).HasPullbacks f
this : ∀ (i : ι), Limits.HasPullback (g i) f
rw :
  (Presieve.ofArrows (fun (i : ι) ↦ Limits.pullback (g i) f) fun (x : ι) ↦ Limits.pullback.snd (g x) f) ∈ J.coverings X
⊢ Presieve.pullbackArrows f (Presieve.ofArrows Z g) ∈ J.coverings X

Tactic:
rw [← Presieve.ofArrows_pullback]

Premises used: CategoryTheory.Presieve.ofArrows_pullback
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst_2 : (Presieve.ofArrows Z g).HasPullbacks f
this : ∀ (i : ι), Limits.HasPullback (g i) f
⊢ (Presieve.ofArrows (fun (i : ι) ↦ Limits.pullback (g i) f) fun (x : ι) ↦ Limits.pullback.snd (g x) f) ∈ J.coverings X

Tactic:
mem_coverings_of_isPullback _ hR _ _ _ fun i ↦ (IsPullback.of_hasPullback _ _).flip

Premises used: CategoryTheory.Precoverage.mem_coverings_of_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst_2 : (Presieve.ofArrows Z g).HasPullbacks f
this : ∀ (i : ι), Limits.HasPullback (g i) f
⊢ (Presieve.ofArrows (fun (i : ι) ↦ Limits.pullback (g i) f) fun (x : ι) ↦ Limits.pullback.snd (g x) f) ∈ J.coverings X

Tactic:
exact mem_coverings_of_isPullback _ hR _ _ _ fun i ↦ (IsPullback.of_hasPullback _ _).flip

Premises used: CategoryTheory.Precoverage.mem_coverings_of_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J : Precoverage.{v_1, u_1} D
X : C
R : Presieve.{v, u} X
⊢ R ∈ (comap F J).coverings X ↔
    Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj X))) (J.coverings (F.obj X)) (Presieve.map F R)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
⊢ comap F (J ⊓ K) = comap F J ⊓ comap F K

Tactic:
rfl

Premises used: CategoryTheory.Presieve, Set.Mem, setOf, Set.inter, rfl, CategoryTheory.Precoverage.comap
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
coverings : ∀ (x : C) (x_1 : Presieve.{v, u} x), x_1 ∈ (comap (𝟭 C) K).coverings x ↔ x_1 ∈ K.coverings x
⊢ comap (𝟭 C) K = K

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
x : C
x_1 : Presieve.{v, u} x
⊢ x_1 ∈ (comap (𝟭 C) K).coverings x ↔ x_1 ∈ K.coverings x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v, v_1, u, u_1} C D
G : Functor.{v_1, v_2, u_1, u_2} D E
J : Precoverage.{v_2, u_2} E
coverings : ∀ (X : C) (R : Presieve.{v, u} X), R ∈ (comap (F ⋙ G) J).coverings X ↔ R ∈ (comap F (comap G J)).coverings X
⊢ comap (F ⋙ G) J = comap F (comap G J)

Tactic:
ext X R
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v, v_1, u, u_1} C D
G : Functor.{v_1, v_2, u_1, u_2} D E
J : Precoverage.{v_2, u_2} E
X : C
R : Presieve.{v, u} X
coverings :
  ∀ (ι : Type (max u v)) (Y : ι → C) (f : (i : ι) → Y i ⟶ X),
    Presieve.ofArrows Y f ∈ (comap (F ⋙ G) J).coverings X ↔ Presieve.ofArrows Y f ∈ (comap F (comap G J)).coverings X
⊢ R ∈ (comap (F ⋙ G) J).coverings X ↔ R ∈ (comap F (comap G J)).coverings X

Tactic:
obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v, v_1, u, u_1} C D
G : Functor.{v_1, v_2, u_1, u_2} D E
J : Precoverage.{v_2, u_2} E
X : C
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ Presieve.ofArrows Y f ∈ (comap (F ⋙ G) J).coverings X ↔ Presieve.ofArrows Y f ∈ (comap F (comap G J)).coverings X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : J.HasIsos
S T : C
f : S ⟶ T
hf : IsIso f
⊢ Presieve.singleton f ∈ (comap F J).coverings T

Tactic:
simpa using mem_coverings_of_isIso (F.map f)

Premises used: CategoryTheory.Precoverage.mem_coverings_of_isIso, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : J.IsStableUnderComposition
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
hf : Presieve.ofArrows Y f ∈ (comap F J).coverings S
σ : ι → Type (max u v)
Z : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Z i j ⟶ Y i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v, u} (Y i))) ((comap F J).coverings (Y i)) (Presieve.ofArrows (Z i) (g i))
simp :
  ∀
    (hf :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (J.coverings (F.obj S))
        (Presieve.ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)))
    (hg :
      ∀ (i : ι),
        Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj (Y i)))) (J.coverings (F.obj (Y i)))
          (Presieve.ofArrows (fun (i_1 : σ i) ↦ F.obj (Z i i_1)) fun (i_1 : σ i) ↦ F.map (g i i_1))),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (J.coverings (F.obj S))
      (Presieve.ofArrows
        (fun (i : (i : ι) × σ i) ↦ F.obj (Z (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i))))
        fun (i : (i : ι) × σ i) ↦
        F.map (g (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i))) ≫
          F.map (f (i.fst (β := fun (i : ι) ↦ σ i))))
⊢ (Presieve.ofArrows (fun (p : (i : ι) × σ i) ↦ Z (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (x : (i : ι) × σ i) ↦
      g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i))) ∈
    (comap F J).coverings S

Tactic:
simp only [mem_comap_iff, Presieve.map_ofArrows, Functor.map_comp] at hf hg ⊢

Premises used: CategoryTheory.Presieve.map_ofArrows, CategoryTheory.Functor.map_comp, CategoryTheory.Precoverage.mem_comap_iff
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : J.IsStableUnderComposition
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
σ : ι → Type (max u v)
Z : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Z i j ⟶ Y i
hf :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (J.coverings (F.obj S))
    (Presieve.ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj (Y i)))) (J.coverings (F.obj (Y i)))
      (Presieve.ofArrows (fun (i_1 : σ i) ↦ F.obj (Z i i_1)) fun (i_1 : σ i) ↦ F.map (g i i_1))
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (J.coverings (F.obj S))
    (Presieve.ofArrows
      (fun (i : (i : ι) × σ i) ↦ F.obj (Z (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i))))
      fun (i : (i : ι) × σ i) ↦
      F.map (g (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i))) ≫
        F.map (f (i.fst (β := fun (i : ι) ↦ σ i))))

Tactic:
J.comp_mem_coverings _ hf _ hg

Premises used: Set.Mem, CategoryTheory.Precoverage.comp_mem_coverings
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : J.IsStableUnderComposition
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
σ : ι → Type (max u v)
Z : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Z i j ⟶ Y i
hf :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (J.coverings (F.obj S))
    (Presieve.ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj (Y i)))) (J.coverings (F.obj (Y i)))
      (Presieve.ofArrows (fun (i_1 : σ i) ↦ F.obj (Z i i_1)) fun (i_1 : σ i) ↦ F.map (g i i_1))
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (J.coverings (F.obj S))
    (Presieve.ofArrows
      (fun (i : (i : ι) × σ i) ↦ F.obj (Z (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i))))
      fun (i : (i : ι) × σ i) ↦
      F.map (g (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i))) ≫
        F.map (f (i.fst (β := fun (i : ι) ↦ σ i))))

Tactic:
exact J.comp_mem_coverings _ hf _ hg

Premises used: CategoryTheory.Precoverage.comp_mem_coverings
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : PreservesLimitsOfShape WalkingCospan F
inst_3 : J.IsStableUnderBaseChange
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
hf : Presieve.ofArrows Y f ∈ (comap F J).coverings S
Z : C
g : Z ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Z
p₂ : (i : ι) → P i ⟶ Y i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
simp :
  ∀
    (hf :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (J.coverings (F.obj S))
        (Presieve.ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj Z))) (J.coverings (F.obj Z))
      (Presieve.ofArrows (fun (i : ι) ↦ F.obj (P i)) fun (i : ι) ↦ F.map (p₁ i))
⊢ Presieve.ofArrows P p₁ ∈ (comap F J).coverings Z

Tactic:
simp only [mem_comap_iff, Presieve.map_ofArrows] at hf ⊢

Premises used: CategoryTheory.Presieve.map_ofArrows, CategoryTheory.Precoverage.mem_comap_iff
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : PreservesLimitsOfShape WalkingCospan F
inst_3 : J.IsStableUnderBaseChange
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
Z : C
g : Z ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Z
p₂ : (i : ι) → P i ⟶ Y i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
hf :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (J.coverings (F.obj S))
    (Presieve.ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj Z))) (J.coverings (F.obj Z))
    (Presieve.ofArrows (fun (i : ι) ↦ F.obj (P i)) fun (i : ι) ↦ F.map (p₁ i))

Tactic:
mem_coverings_of_isPullback _ hf _ _ _
      fun i ↦ CategoryTheory.Functor.map_isPullback F (h i)

Premises used: CategoryTheory.Functor.map_isPullback, CategoryTheory.Precoverage.mem_coverings_of_isPullback
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : PreservesLimitsOfShape WalkingCospan F
inst_3 : J.IsStableUnderBaseChange
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
Z : C
g : Z ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Z
p₂ : (i : ι) → P i ⟶ Y i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
hf :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj S))) (J.coverings (F.obj S))
    (Presieve.ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (F.obj Z))) (J.coverings (F.obj Z))
    (Presieve.ofArrows (fun (i : ι) ↦ F.obj (P i)) fun (i : ι) ↦ F.map (p₁ i))

Tactic:
exact mem_coverings_of_isPullback _ hf _ _ _
      fun i ↦ CategoryTheory.Functor.map_isPullback F (h i)

Premises used: CategoryTheory.Functor.map_isPullback, CategoryTheory.Precoverage.mem_coverings_of_isPullback
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : CreatesLimitsOfShape WalkingCospan F
inst_3 : J.HasPullbacks
X Y : C
R : Presieve.{v, u} Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
⊢ R.HasPullbacks f

Tactic:
⟨fun {Z g} hg ↦ ?_⟩

Premises used: CategoryTheory.Presieve.HasPullbacks.mk
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : CreatesLimitsOfShape WalkingCospan F
inst_3 : J.HasPullbacks
X Y : C
R : Presieve.{v, u} Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
refine : ∀ {Z : C} {g : Z ⟶ Y} (hg : R g), HasPullback g f
⊢ R.HasPullbacks f

Tactic:
refine ⟨fun {Z g} hg ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : CreatesLimitsOfShape WalkingCospan F
inst_3 : J.HasPullbacks
X Y : C
R : Presieve.{v, u} Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
Z : C
g : Z ⟶ Y
hg : R g
⊢ (Presieve.map F R).HasPullbacks (F.map f)

Tactic:
have : (Presieve.map F R).HasPullbacks (F.map f) := J.hasPullbacks_of_mem (F.map f) hR
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : CreatesLimitsOfShape WalkingCospan F
inst_3 : J.HasPullbacks
X Y : C
R : Presieve.{v, u} Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
Z : C
g : Z ⟶ Y
hg : R g
this : (Presieve.map F R).HasPullbacks (F.map f)
⊢ HasPullback (F.map g) (F.map f)

Tactic:
have : HasPullback (F.map g) (F.map f) := (R.map F).hasPullback _ (R.map_map hg)
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : CreatesLimitsOfShape WalkingCospan F
inst_3 : J.HasPullbacks
X Y : C
R : Presieve.{v, u} Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
Z : C
g : Z ⟶ Y
hg : R g
this_1 : (Presieve.map F R).HasPullbacks (F.map f)
this : HasPullback (F.map g) (F.map f)
⊢ HasPullback g f

Tactic:
.of_createsLimit F g f

Premises used: CategoryTheory.Limits.HasPullback.of_createsLimit
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
J K : Precoverage.{v_1, u_1} D
inst_2 : CreatesLimitsOfShape WalkingCospan F
inst_3 : J.HasPullbacks
X Y : C
R : Presieve.{v, u} Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
Z : C
g : Z ⟶ Y
hg : R g
this_1 : (Presieve.map F R).HasPullbacks (F.map f)
this : HasPullback (F.map g) (F.map f)
⊢ HasPullback g f

Tactic:
exact .of_createsLimit F g f