awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : Limits.HasPullbacks.{u_1, u_2} C
inst_4 : J.HasIsos
x : C
x_1 : Sieve.{u_1, u_2} x
⊢ x_1 ∈ (Pretopology.toGrothendieck (toPretopology C J) : (a : C) → Set (Sieve a)) x ↔
    x_1 ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) x

Tactic:
exact J.mem_toGrothendieck_iff_of_isStableUnderComposition.symm

Premises used: CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, Iff.symm
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
h : IsSheaf J.toGrothendieck P
S : C
R : Presieve.{u_2, u_3} S
hR : R ∈ J.coverings S
rw :
  ∀ (h : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows)
    {S : C} {R : Presieve.{u_2, u_3} S} (hR : R ∈ J.coverings S), IsSheafFor P R
⊢ IsSheafFor P R

Tactic:
rw [J.isSheaf_toGrothendieck_iff] at h

Premises used: CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
h : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
S : C
R : Presieve.{u_2, u_3} S
hR : R ∈ J.coverings S
⊢ IsSheafFor P R

Tactic:
simpa [Presieve.isSheafFor_iff_generate] using h (f := 𝟙 S) R hR

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S : C
𝒰 𝒱 : PreZeroHypercover.{u_4, u_2, u_3} S
e : 𝒰 ≅ 𝒱
rw : Presieve.IsSheafFor F (Sieve.generate 𝒰.presieve₀).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₁ : Presieve.IsSheafFor F (Sieve.ofArrows 𝒰.X 𝒰.f).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₂ : Presieve.IsSheafFor F 𝒰.sieve₀.arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₃ : Presieve.IsSheafFor F 𝒱.sieve₀.arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
rw₄ rw₅ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.X 𝒱.f) ↔ Presieve.IsSheafFor F 𝒱.presieve₀
⊢ Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀

Tactic:
rw [Presieve.isSheafFor_iff_generate, ← Sieve.ofArrows, ← PreZeroHypercover.sieve₀,
    PreZeroHypercover.sieve₀_eq_of_iso e, ← Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.PreZeroHypercover.sieve₀, CategoryTheory.Sieve.ofArrows, CategoryTheory.Presieve.isSheafFor_iff_generate, CategoryTheory.PreZeroHypercover.sieve₀_eq_of_iso
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
F : Functor.{u_3, u_1, u_4, u_1 + 1} Cᵒᵖ (Type u_1)
X : C
ι : Type u_2
Y Z : ι → C
g : (i : ι) → Z i ⟶ X
e_1 : (i : ι) → Y i ≅ Z i
𝒰 : PreZeroHypercover.{u_2, u_3, u_4} X := { I₀ := ι, X := Z, f := g }
𝒱 : PreZeroHypercover.{u_2, u_3, u_4} X := { I₀ := ι, X := Y, f := fun (i : ι) ↦ (e_1 i).hom ≫ g i }
e : 𝒰 ≅ 𝒱 := PreZeroHypercover.isoMk (Equiv.refl 𝒰.I₀) (fun (i : 𝒰.I₀) ↦ (e_1 i).symm) ⋯
⊢ IsSheafFor (X := X) F (ofArrows Y fun (i : ι) ↦ (e_1 i).hom ≫ g i) ↔ IsSheafFor F (ofArrows Z g)

Tactic:
PreZeroHypercover.isSheafFor_iff_of_iso e.symm

Premises used: CategoryTheory.PreZeroHypercover.isSheafFor_iff_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
F : Functor.{u_3, u_1, u_4, u_1 + 1} Cᵒᵖ (Type u_1)
X : C
ι : Type u_2
Y Z : ι → C
g : (i : ι) → Z i ⟶ X
e_1 : (i : ι) → Y i ≅ Z i
𝒰 : PreZeroHypercover.{u_2, u_3, u_4} X := { I₀ := ι, X := Z, f := g }
𝒱 : PreZeroHypercover.{u_2, u_3, u_4} X := { I₀ := ι, X := Y, f := fun (i : ι) ↦ (e_1 i).hom ≫ g i }
e : 𝒰 ≅ 𝒱 := PreZeroHypercover.isoMk (Equiv.refl 𝒰.I₀) (fun (i : 𝒰.I₀) ↦ (e_1 i).symm) ⋯
⊢ IsSheafFor (X := X) F (ofArrows Y fun (i : ι) ↦ (e_1 i).hom ≫ g i) ↔ IsSheafFor F (ofArrows Z g)

Tactic:
exact PreZeroHypercover.isSheafFor_iff_of_iso e.symm

Premises used: CategoryTheory.PreZeroHypercover.isSheafFor_iff_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S X Y : C
f : X ⟶ S
g : Y ⟶ S
e : X ≅ Y
he : e.hom ≫ g = f
subst : IsSheafFor F (singleton (e.hom ≫ g)) ↔ IsSheafFor F (singleton g)
⊢ IsSheafFor F (singleton f) ↔ IsSheafFor F (singleton g)

Tactic:
subst he
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
F : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
S X Y : C
g : Y ⟶ S
e : X ≅ Y
rw :
  IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ e.hom ≫ g) ↔
    IsSheafFor F (singleton g)
rw₁ :
  IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ e.hom ≫ g) ↔
    IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ g)
rw₂ rw₃ :
  IsSheafFor (X := S) F (ofArrows (fun (i : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ g) ↔
    IsSheafFor (X := S) F (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ g)
⊢ IsSheafFor F (singleton (e.hom ≫ g)) ↔ IsSheafFor F (singleton g)

Tactic:
rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ← Presieve.ofArrows_pUnit,
    Presieve.isSheafFor_ofArrows_comp_iff]

Premises used: CategoryTheory.Presieve.ofArrows_pUnit, CategoryTheory.Presieve.isSheafFor_ofArrows_comp_iff
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
R : Presieve.{u_3, u_4} X
inst_2 : R.HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks R
⊢ (map F R).HasPairwisePullbacks

Tactic:
have : (R.map F).HasPairwisePullbacks := .map_of_preservesPairwisePullbacks _ _
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
R : Presieve.{u_3, u_4} X
inst_2 : R.HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks R
this : (map F R).HasPairwisePullbacks
obtain :
  ∀ (ι : Type (max u_4 u_3)) (Y : ι → C) (f : (i : ι) → Y i ⟶ X) [(ofArrows Y f).HasPairwisePullbacks]
    [F.PreservesPairwisePullbacks (ofArrows Y f)] (this : (map F (ofArrows Y f)).HasPairwisePullbacks),
    IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔ IsSheafFor P (map F (ofArrows Y f))
⊢ IsSheafFor (F.op ⋙ P) R ↔ IsSheafFor P (map F R)

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

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (map F (ofArrows Y f)).HasPairwisePullbacks
rw :
  ∀
    (this :
      HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
        (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))),
    IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔
      IsSheafFor (X := F.obj X) P (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
⊢ IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔ IsSheafFor P (map F (ofArrows Y f))

Tactic:
rw [map_ofArrows] at this ⊢

Premises used: CategoryTheory.Presieve.map_ofArrows
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
simp_rw :
  (∀ (x : (i : ι) → (F.op ⋙ P).obj (Opposite.op (Y i))),
      Arrows.PullbackCompatible (F.op ⋙ P) f x →
        ∃! t : (F.op ⋙ P).obj (Opposite.op X),
          ∀ (i : ι),
            (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.op ⋙ P).map (f i).op) :
                  (a : (F.op ⋙ P).obj (Opposite.op X)) → (F.op ⋙ P).obj (Opposite.op (Y i)))
                t =
              x i) ↔
    ∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
      Arrows.PullbackCompatible P (B := F.obj X) (fun (i : ι) ↦ F.map (f i)) x →
        ∃! t : P.obj (Opposite.op (F.obj X)),
          ∀ (i : ι),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map (f i)).op) :
                  (a : P.obj (Opposite.op (F.obj X))) → P.obj (Opposite.op (F.obj (Y i))))
                t =
              x i
⊢ IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔
    IsSheafFor (X := F.obj X) P (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))

Tactic:
simp_rw [Presieve.isSheafFor_arrows_iff_pullbacks]

Premises used: CategoryTheory.Presieve.isSheafFor_arrows_iff_pullbacks
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
⊢ PreservesLimit (cospan (f i) (f j)) F

Tactic:
have : PreservesLimit (cospan (f i) (f j)) F :=
    F.preservesLimit_cospan_of_mem_presieve (ofArrows _ f) ⟨i⟩ ⟨j⟩
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this_1 :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this : PreservesLimit (cospan (f i) (f j)) F
⊢ HasPullback (F.map (f i)) (F.map (f j))

Tactic:
have : HasPullback (F.map (f i)) (F.map (f j)) := hasPullback_of_preservesPullback _ _ _
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this_1 :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this_2 : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
rw :
  IsIso (X := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j))))) (Y :=
    P.obj (Opposite.op (F.obj (pullback (f i) (f j))))) (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))
⊢ Function.Bijective (α := (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) (β :=
    (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
      (a : (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) →
        (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))

Tactic:
rw [← isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this_1 :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this_2 : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ IsIso (X := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j))))) (Y :=
    P.obj (Opposite.op (F.obj (pullback (f i) (f j))))) (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this_1 :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this_2 : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ Function.Bijective (α := (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) (β :=
    (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
      (a : (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) →
        (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))

Tactic:
have : Function.Bijective (P.map (pullbackComparison F (f i) (f j)).op) := by
    rw [← isIso_iff_bijective]
    infer_instance
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this_1 :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this_2 : PreservesLimit (cospan (f i) (f j)) F
this_3 : HasPullback (F.map (f i)) (F.map (f j))
this :
  Function.Bijective (α := (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) (β :=
    (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
      (a : (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) →
        (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))
⊢ Eq (α := P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullback.fst (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y i)))) → P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
          (x i) :
        P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullback.snd (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y j)))) → P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
          (x j) :
        P.obj (Opposite.op (F.obj (pullback (f i) (f j))))) ↔
    Eq (α := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (F.map (f i)) (F.map (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y i)))) → P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
          (x i) :
        P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (F.map (f i)) (F.map (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y j)))) → P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
          (x j) :
        P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))

Tactic:
this.1.eq_iff

Premises used: Function.Injective.eq_iff, And.left
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this_1 :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this_2 : PreservesLimit (cospan (f i) (f j)) F
this_3 : HasPullback (F.map (f i)) (F.map (f j))
this :
  Function.Bijective (α := (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) (β :=
    (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
      (a : (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) →
        (fun (X : Type u_2) ↦ X) (P.obj (Opposite.op (F.obj (pullback (f i) (f j))))))
⊢ Eq (α := P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullback.fst (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y i)))) → P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
          (x i) :
        P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullback.snd (F.map (f i)) (F.map (f j)))))
                (P.map (Quiver.Hom.op (pullbackComparison F (f i) (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y j)))) → P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
          (x j) :
        P.obj (Opposite.op (F.obj (pullback (f i) (f j))))) ↔
    Eq (α := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (F.map (f i)) (F.map (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y i)))) → P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
          (x i) :
        P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (F.map (f i)) (F.map (f j))))) :
            (a : P.obj (Opposite.op (F.obj (Y j)))) → P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
          (x j) :
        P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))

Tactic:
exact this.1.eq_iff

Premises used: Function.Injective.eq_iff, And.left
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : GrothendieckTopology.{u_2, u_3} C
S : C
R : Presieve.{u_2, u_3} S
⊢ R ∈ J.toPrecoverage.coverings S ↔ Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : GrothendieckTopology.{u_2, u_3} C
S : C
R : Sieve.{u_2, u_3} S
rw : Sieve.generate R.arrows ∈ (J : (a : C) → Set (Sieve a)) S ↔ R ∈ (J : (a : C) → Set (Sieve a)) S
rw₁ rw₂ : R ∈ (J : (a : C) → Set (Sieve a)) S ↔ R ∈ (J : (a : C) → Set (Sieve a)) S
⊢ R.arrows ∈ J.toPrecoverage.coverings S ↔ R ∈ (J : (a : C) → Set (Sieve a)) S

Tactic:
rw [mem_toPrecoverage_iff, Sieve.generate_sieve]

Premises used: CategoryTheory.Sieve.generate_sieve, CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{u_2, u_3} C
S T : C
f : S ⟶ T
hf : IsIso f
⊢ Presieve.singleton f ∈ J.toPrecoverage.coverings T

Tactic:
simp [mem_toPrecoverage_iff]

Premises used: CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{u_2, u_3} C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
σ : ι → Type (max u_3 u_2)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{u_2, u_3} (X i))) (J.toPrecoverage.coverings (X i))
      (Presieve.ofArrows (Y i) (g i))
rw :
  Sieve.generate (Presieve.bindOfArrows X f fun (i : ι) ↦ Presieve.ofArrows (Y i) (g i)) ∈
    (J : (a : C) → Set (Sieve a)) S
⊢ (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))) ∈
    J.toPrecoverage.coverings S

Tactic:
rw [mem_toPrecoverage_iff, ← Presieve.bindOfArrows_ofArrows]

Premises used: CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff, CategoryTheory.Presieve.bindOfArrows_ofArrows
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
J : GrothendieckTopology.{u_2, u_3} C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
σ : ι → Type (max u_3 u_2)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{u_2, u_3} (X i))) (J.toPrecoverage.coverings (X i))
      (Presieve.ofArrows (Y i) (g i))
⊢ Sieve.generate (Presieve.bindOfArrows X f fun (i : ι) ↦ Presieve.ofArrows (Y i) (g i)) ∈
    (J : (a : C) → Set (Sieve a)) S

Tactic:
J.bindOfArrows hf hg

Premises used: CategoryTheory.GrothendieckTopology.bindOfArrows