awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
⊢ Eq (α :=
    (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₁) ⋯).op) :
          (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₁)))) →
            (fun (X : Type w) ↦ X)
              (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
        ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₁) :
      (fun (X : Type w) ↦ X)
        (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₂) ⋯).op) :
          (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₂)))) →
            (fun (X : Type w) ↦ X)
              (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
        ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₂) :
      (fun (X : Type w) ↦ X)
        (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))

Tactic:
have := s.property i₁ i₂ (Over.mk (g₁.left ≫ (f i₁).left ≫ X.hom))
          (Over.homMk g₁.left) (Over.homMk g₂.left (by
            have := Over.w (f i₂)
            dsimp at this ⊢
            rw [reassoc_of% h, this])) (by cat_disch)
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this :
  Eq (α :=
    (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₁) ⋯).op) :
          (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₁)))) →
            (fun (X : Type w) ↦ X)
              (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
        ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₁) :
      (fun (X : Type w) ↦ X)
        (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₂) ⋯).op) :
          (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₂)))) →
            (fun (X : Type w) ↦ X)
              (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
        ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₂) :
      (fun (X : Type w) ↦ X)
        (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
⊢ 𝟙 Z.left ≫ ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))).hom = Z.hom

Tactic:
simpa using Over.w g₁

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map φ.op) :
          (a : P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) →
            P.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map ((Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op) :
              (a : P.obj (op ((Over.map p).obj (Y i₁)))) →
                P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
            ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₁) :
          P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map φ.op) :
          (a : P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) →
            P.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map ((Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op) :
              (a : P.obj (op ((Over.map p).obj (Y i₂)))) →
                P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
            ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₂) :
          P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) :
      P.obj (op Z))
⊢ Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₁)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₁) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₂)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₂) :
      P.obj (op Z))

Tactic:
simp only [← comp_apply, ← Functor.map_comp, ← op_comp] at this

Premises used: CategoryTheory.op_comp, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₁)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₁) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₂)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₂) :
      P.obj (op Z))
⊢ Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₁)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₁) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₂)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₂) :
      P.obj (op Z))

Tactic:
this
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₁)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₁) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op) :
          (a : P.obj (op ((Over.map p).obj (Y i₂)))) → P.obj (op Z))
        ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₂) :
      P.obj (op Z))
h₁ : g₁ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)
h₂ : g₂ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₁)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₂)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
convert! this
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s :
  Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
    (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i))
i₁ i₂ : I
Z : Over.{v₁, u₁} B
g₁ : Z ⟶ Y i₁
g₂ : Z ⟶ Y i₂
h : g₁ ≫ f i₁ = g₂ ≫ f i₂
⊢ Eq (α := (Over.map p).obj Z ⟶ (Over.map p).obj X) ((Over.map p).map g₁ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₁)
    ((Over.map p).map g₂ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₂)

Tactic:
simp only [← Functor.map_comp, h]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
e : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f) ≃
  Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
    (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i)) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i))
        (fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) ⋯,
    invFun :=
      fun
        (s :
          Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
            (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i))) ↦
      Subtype.mk (p := Arrows.Compatible ((Over.map p).op ⋙ P) f)
        (fun (i : I) ↦ (↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
simp :
  Function.Bijective (β :=
      Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
        (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i)))
      ((⇑e :
          (a : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)) →
            Subtype (Arrows.Compatible P fun (i : I) ↦ (Over.map p).map (f i))) ∘
        Arrows.toCompatible ((Over.map p).op ⋙ P) f) ↔
    Function.Bijective (α := P.obj (op ((Over.map p).obj X))) (β :=
      Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
        (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i)))
      (Arrows.toCompatible P fun (i : I) ↦ (Over.map p).map (f i))
⊢ IsSheafFor ((Over.map p).op ⋙ P) (ofArrows Y f) ↔
    IsSheafFor (X := (Over.map p).obj X) P
      (ofArrows (fun (i : I) ↦ (Over.map p).obj (Y i)) fun (i : I) ↦ (Over.map p).map (f i))

Tactic:
simp only [isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← e.bijective.of_comp_iff']

Premises used: Equiv.bijective, Function.Bijective.of_comp_iff', CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
e : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f) ≃
  Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
    (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i)) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i))
        (fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) ⋯,
    invFun :=
      fun
        (s :
          Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
            (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i))) ↦
      Subtype.mk (p := Arrows.Compatible ((Over.map p).op ⋙ P) f)
        (fun (i : I) ↦ (↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Function.Bijective (β :=
      Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
        (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i)))
      ((⇑e :
          (a : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)) →
            Subtype (Arrows.Compatible P fun (i : I) ↦ (Over.map p).map (f i))) ∘
        Arrows.toCompatible ((Over.map p).op ⋙ P) f) ↔
    Function.Bijective (α := P.obj (op ((Over.map p).obj X))) (β :=
      Subtype (α := (i : I) → P.obj (op ((Over.map p).obj (Y i))))
        (Arrows.Compatible P (B := (Over.map p).obj X) fun (i : I) ↦ (Over.map p).map (f i)))
      (Arrows.toCompatible P fun (i : I) ↦ (Over.map p).map (f i))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
R : Sieve X
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
obtain :
  ∀ (ι : Type (max u₁ v₁)) (Z : ι → Over.{v₁, u₁} B) (g : (i : ι) → Z i ⟶ X),
    IsSheafFor ((Over.map p).op ⋙ P) (Sieve.ofArrows Z g).arrows ↔
      IsSheafFor P (Sieve.pullback e.inv (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g))).arrows
⊢ IsSheafFor ((Over.map p).op ⋙ P) R.arrows ↔
    IsSheafFor P (Sieve.pullback e.inv (Sieve.functorPushforward (Over.map p) R)).arrows

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

Premises used: CategoryTheory.Sieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
rw :
  IsSheafFor (X := (Over.map p).obj X) P
      (arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)))) ↔
    IsSheafFor P (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)).arrows
⊢ IsSheafFor ((Over.map p).op ⋙ P) (Sieve.ofArrows Z g).arrows ↔
    IsSheafFor P (Sieve.pullback e.inv (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g))).arrows

Tactic:
rw [← isSheafFor_iff_generate, isSheafFor_pullback_iff,
    isSheafFor_over_map_op_comp_ofArrows_iff, isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_pullback_iff, CategoryTheory.Presieve.isSheafFor_iff_generate, CategoryTheory.Presieve.isSheafFor_over_map_op_comp_ofArrows_iff
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
⊢ IsSheafFor (X := (Over.map p).obj X) P
      (arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)))) ↔
    IsSheafFor (X := (Over.map p).obj X) P
      (arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
h :
  Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) =
    generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))
⊢ IsSheafFor (X := (Over.map p).obj X) P
      (arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)))) ↔
    IsSheafFor P (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)).arrows

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
⊢ Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) =
    generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
h :
  Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) ≤
    generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))
h₁ :
  generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)) ≤
    Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)
⊢ Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) =
    generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
W : Over.{v₁, u₁} B'
T : Over.{v₁, u₁} B
a : W ⟶ (Over.map p).obj T
Y : Over.{v₁, u₁} B
i : ι
b : T ⟶ Z i
⊢ arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)))
    (a ≫ (Over.map p).map (b ≫ g i))

Tactic:
⟨(Over.map p).obj (Z i), Over.homMk (a.left ≫ b.left) ?_, _, ⟨i⟩, ?_⟩

Premises used: CategoryTheory.Over.map, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Over.Hom.left, CategoryTheory.Over.homMk, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
W : Over.{v₁, u₁} B'
T : Over.{v₁, u₁} B
a : W ⟶ (Over.map p).obj T
Y : Over.{v₁, u₁} B
i : ι
b : T ⟶ Z i
h : (Over.Hom.left a ≫ Over.Hom.left b) ≫ ((Over.map p).obj (Z i)).hom = W.hom
h₁ : Over.homMk (Over.Hom.left a ≫ Over.Hom.left b) ⋯ ≫ (Over.map p).map (g i) = a ≫ (Over.map p).map (b ≫ g i)
⊢ arrows (generate (ofArrows (fun (i : ι) ↦ (Over.map p).obj (Z i)) fun (i : ι) ↦ (Over.map p).map (g i)))
    (a ≫ (Over.map p).map (b ≫ g i))

Tactic:
refine ⟨(Over.map p).obj (Z i), Over.homMk (a.left ≫ b.left) ?_, _, ⟨i⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
W : Over.{v₁, u₁} B'
T : Over.{v₁, u₁} B
a : W ⟶ (Over.map p).obj T
Y : Over.{v₁, u₁} B
i : ι
b : T ⟶ Z i
⊢ (Over.Hom.left a ≫ Over.Hom.left b) ≫ ((Over.map p).obj (Z i)).hom = W.hom

Tactic:
simpa [(Over.w_assoc b)] using Over.w a

Premises used: CategoryTheory.Over.w, CategoryTheory.Over.w_assoc
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
W Y : Over.{v₁, u₁} B'
i : ι
a : W ⟶ (Over.map p).obj (Z i)
⊢ (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)).arrows (a ≫ (Over.map p).map (g i))

Tactic:
⟨_, _, _, Sieve.ofArrows_mk _ _ i, rfl⟩

Premises used: CategoryTheory.Sieve.ofArrows_mk, And.intro, Exists.intro, CategoryTheory.Presieve.functorPushforward, rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
X' : Over.{v₁, u₁} B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over.{v₁, u₁} B
g : (i : ι) → Z i ⟶ X
W Y : Over.{v₁, u₁} B'
i : ι
a : W ⟶ (Over.map p).obj (Z i)
⊢ (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)).arrows (a ≫ (Over.map p).map (g i))

Tactic:
exact ⟨_, _, _, Sieve.ofArrows_mk _ _ i, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
⊢ Compatible P π x ↔ PullbackCompatible P π x

Tactic:
⟨fun t i j ↦ ?_, fun t i j Z gi gj comm ↦ ?_⟩

Premises used: Iff.intro