awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
y : P.obj (op B)
hy : (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) = x
refine_2 :
  ∀ (hx : Arrows.Compatible P π (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i)))),
    ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) i
⊢ ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i

Tactic:
subst hy
-- 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
h : Function.Bijective (Arrows.toCompatible P π)
y : P.obj (op B)
hx : Arrows.Compatible P π (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i)))
y' : (fun (X : Type w) ↦ X) (P.obj (op B))
hy' :
  (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) i)
    y'
a :
  ∀ (x : I),
    (↑(Arrows.toCompatible P π y') : (i : I) → P.obj (op (X i))) x =
      (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) x
⊢ Arrows.toCompatible P π y' = Arrows.toCompatible P π y

Tactic:
ext
-- 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
h : Function.Bijective (Arrows.toCompatible P π)
y : P.obj (op B)
hx : Arrows.Compatible P π (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i)))
y' : (fun (X : Type w) ↦ X) (P.obj (op B))
hy' :
  (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) i)
    y'
x : I
⊢ (↑(Arrows.toCompatible P π y') : (i : I) → P.obj (op (X i))) x =
    (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) x

Tactic:
apply hy'
-- 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
h : Function.Bijective (Arrows.toCompatible P π)
y : P.obj (op B)
hx : Arrows.Compatible P π (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i)))
⊢ ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) i

Tactic:
exact ⟨y, fun _ ↦ rfl, fun y' hy' ↦ h.1 (by ext; apply hy')⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
inst_1 : IsIso f
obtain :
  ∀ (ι : Type (max u₁ v₁)) (Z : ι → C) (g : (i : ι) → Z i ⟶ X),
    IsSheafFor P (Sieve.pullback f (Sieve.ofArrows Z g)).arrows ↔ IsSheafFor P (Sieve.ofArrows Z g).arrows
⊢ IsSheafFor P (Sieve.pullback f R).arrows ↔ IsSheafFor 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
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
⊢ Sieve.pullback (asIso f).hom (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ (asIso f).inv

Tactic:
have := Sieve.pullback_ofArrows_of_iso _ g (asIso f)
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P g)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : Eq (α := W ⟶ Y) (g₁ ≫ (fun (i : ι) ↦ g i ≫ inv f) i₁) (g₂ ≫ (fun (i : ι) ↦ g i ≫ inv f) i₂)
⊢ g₁ ≫ g i₁ = g₂ ≫ g i₂

Tactic:
simp only [← cancel_mono f, assoc, IsIso.inv_hom_id, comp_id] at h

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P g)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ = g₂ ≫ g i₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₁)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₂)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))

Tactic:
s.property _ _ _ _ _ h

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P g)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ = g₂ ≫ g i₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₁)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₂)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))

Tactic:
exact s.property _ _ _ _ _ h

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ = g₂ ≫ g i₂
⊢ (g₁ ≫ g i₁) ≫ inv f = (g₂ ≫ g i₂) ≫ inv f

Tactic:
replace h := h =≫ inv f
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : (g₁ ≫ g i₁) ≫ inv f = (g₂ ≫ g i₂) ≫ inv f
⊢ g₁ ≫ g i₁ ≫ inv f = g₂ ≫ g i₂ ≫ inv f

Tactic:
simp only [Category.assoc] at h

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ ≫ inv f = g₂ ≫ g i₂ ≫ inv f
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₁)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₂)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))

Tactic:
s.property _ _ _ _ _ h

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ ≫ inv f = g₂ ≫ g i₂ ≫ inv f
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₁)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (Z i₂)))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
        ((fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op W)))

Tactic:
exact s.property _ _ _ _ _ h

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
e : Subtype (Arrows.Compatible P g) ≃
  Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible P g)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
        (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    invFun :=
      fun (s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)) ↦
      Subtype.mk (p := Arrows.Compatible P g) (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
simp :
  Function.Bijective (α := P.obj (op Y)) (β :=
      Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
      (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f) ↔
    Function.Bijective (α := P.obj (op Y)) (β :=
      Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
      (((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
          Arrows.toCompatible P g) ∘
        (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
⊢ IsSheafFor P (Sieve.pullback f (Sieve.ofArrows Z g)).arrows ↔ IsSheafFor P (Sieve.ofArrows Z g).arrows

Tactic:
simp only [this, ← isSheafFor_iff_generate,
    isSheafFor_ofArrows_iff_bijective_toCompabible, ← e.bijective.of_comp_iff',
    ← Function.Bijective.of_comp_iff _ (P.mapIso (asIso f).symm.op).toEquiv.bijective]

Premises used: Equiv.bijective, CategoryTheory.Iso.toEquiv, CategoryTheory.Iso.op, CategoryTheory.Presieve.isSheafFor_iff_generate, Function.Bijective.of_comp_iff, Function.Bijective.of_comp_iff', CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso, CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
e : Subtype (Arrows.Compatible P g) ≃
  Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible P g)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
        (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    invFun :=
      fun (s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)) ↦
      Subtype.mk (p := Arrows.Compatible P g) (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Function.Bijective (α := P.obj (op Y)) (β :=
      Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
      (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f) ↔
    Function.Bijective (α := P.obj (op Y)) (β :=
      Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
      (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f)

Tactic:
Iff.rfl

Premises used: Iff.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)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
e : Subtype (Arrows.Compatible P g) ≃
  Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible P g)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
        (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    invFun :=
      fun (s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)) ↦
      Subtype.mk (p := Arrows.Compatible P g) (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h :
  Eq (α :=
    P.obj (op Y) → Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
    (((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
        Arrows.toCompatible P g) ∘
      (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
    (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f)
⊢ Function.Bijective (α := P.obj (op Y)) (β :=
      Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
      (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f) ↔
    Function.Bijective (α := P.obj (op Y)) (β :=
      Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
      (((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
          Arrows.toCompatible P g) ∘
        (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))

Tactic:
convert! Iff.rfl using 2

Premises used: Iff.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)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
e : Subtype (Arrows.Compatible P g) ≃
  Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible P g)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
        (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    invFun :=
      fun (s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)) ↦
      Subtype.mk (p := Arrows.Compatible P g) (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h :
  ∀ (x : P.obj (op Y)) (x_1 : ι),
    Eq.{w + 1} (α := P.obj (op (Z x_1)))
      ((↑((((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
                    Arrows.toCompatible P g) ∘
                  (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
                x) :
            (i : ι) → P.obj (op (Z i)))
          x_1 :
        P.obj (op (Z x_1)))
      ((↑(Arrows.toCompatible P (fun (i : ι) ↦ g i ≫ inv f) x) : (i : ι) → P.obj (op (Z i))) x_1 : P.obj (op (Z x_1)))
⊢ Eq (α :=
    P.obj (op Y) → Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f))
    (((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
        Arrows.toCompatible P g) ∘
      (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
    (Arrows.toCompatible P fun (i : ι) ↦ g i ≫ inv f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
inst_1 : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun (i : ι) ↦ g i ≫ inv f
e : Subtype (Arrows.Compatible P g) ≃
  Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f) :=
  {
    toFun := fun (s : Subtype (Arrows.Compatible P g)) ↦
      Subtype.mk (p := Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)
        (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    invFun :=
      fun (s : Subtype (α := (i : ι) → P.obj (op (Z i))) (Arrows.Compatible P (B := Y) fun (i : ι) ↦ g i ≫ inv f)) ↦
      Subtype.mk (p := Arrows.Compatible P g) (fun (i : ι) ↦ (↑s : (i : ι) → P.obj (op (Z i))) i) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
x : P.obj (op Y)
x_1 : ι
⊢ Eq.{w + 1} (α := P.obj (op (Z x_1)))
    ((↑((((⇑e : (a : Subtype (Arrows.Compatible P g)) → Subtype (Arrows.Compatible P fun (i : ι) ↦ g i ≫ inv f)) ∘
                  Arrows.toCompatible P g) ∘
                (⇑(P.mapIso (asIso f).symm.op).toEquiv : (a : P.obj (op Y)) → P.obj (op X)))
              x) :
          (i : ι) → P.obj (op (Z i)))
        x_1 :
      P.obj (op (Z x_1)))
    ((↑(Arrows.toCompatible P (fun (i : ι) ↦ g i ≫ inv f) x) : (i : ι) → P.obj (op (Z i))) x_1 : P.obj (op (Z x_1)))

Tactic:
simp [e]
-- 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 :
  Eq (α := Z ⟶ (Over.map p).obj X) (g₁ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₁)
    (g₂ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₂)
⊢ Eq (α := Functor.obj (Over.forget B') Z ⟶ Functor.obj (Over.forget B') ((Over.map p).obj X))
    (Functor.map (Over.forget B') (g₁ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₁))
    (Functor.map (Over.forget B') (g₂ ≫ (fun (i : I) ↦ (Over.map p).map (f i)) i₂))

Tactic:
replace h := (Over.forget _).congr_map h
-- 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₂)
⊢ Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom

Tactic:
have := Over.w (f i₂)
-- 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 : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
dsimp : Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)).hom

Tactic:
dsimp at 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₂)
this : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
rw : Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂) ≫ X.hom
rw₁ rw₂ : Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₂ ≫ (Y i₂).hom
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom

Tactic:
rw [reassoc_of% h, this]