awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h :
  ∀ {X : C} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)),
    P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)
ι : Type (max u v)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u v)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v, u} (X i))) (P.precoverage.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
F : (i : ι) → PreZeroHypercover (E.X i) := fun (i : ι) ↦ { I₀ := σ i, X := Y i, f := g i }
i : E.I₀
⊢ Membership.mem (γ := Set (Presieve.{v, u} (E.X i))) (P.precoverage.coverings (E.X i)) (F i).presieve₀

Tactic:
exact hg i
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
R S : Presieve.{v, u} X
hR : R ∈ P.precoverage.coverings X
hS : S ∈ P.precoverage.coverings X
obtain :
  ∀ (E : PreZeroHypercover X) (hR : E.presieve₀ ∈ P.precoverage.coverings X),
    E.presieve₀ ⊔ S ∈ P.precoverage.coverings X
⊢ R ⊔ S ∈ P.precoverage.coverings X

Tactic:
obtain ⟨E, rfl⟩ := R.exists_eq_preZeroHypercover

Premises used: CategoryTheory.Presieve.exists_eq_preZeroHypercover, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
S : Presieve.{v, u} X
hS : S ∈ P.precoverage.coverings X
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
obtain :
  ∀ (F : PreZeroHypercover X) (hS : F.presieve₀ ∈ P.precoverage.coverings X),
    E.presieve₀ ⊔ F.presieve₀ ∈ P.precoverage.coverings X
⊢ E.presieve₀ ⊔ S ∈ P.precoverage.coverings X

Tactic:
obtain ⟨F, rfl⟩ := S.exists_eq_preZeroHypercover

Premises used: CategoryTheory.Presieve.exists_eq_preZeroHypercover, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
F : PreZeroHypercover X
hS : F.presieve₀ ∈ P.precoverage.coverings X
rw : (E.sum F).presieve₀ ∈ P.precoverage.coverings X
⊢ E.presieve₀ ⊔ F.presieve₀ ∈ P.precoverage.coverings X

Tactic:
rw [← PreZeroHypercover.presieve₀_sum]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_sum
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
F : PreZeroHypercover X
hS : F.presieve₀ ∈ P.precoverage.coverings X
rw : ∀ (hR : P.property E) (F : PreZeroHypercover X) (hS : P.property F), P.property (E.sum F)
⊢ (E.sum F).presieve₀ ∈ P.precoverage.coverings X

Tactic:
rw [PreZeroHypercover.presieve₀_mem_precoverage_iff] at hR hS ⊢

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : P.property E
F : PreZeroHypercover X
hS : P.property F
⊢ P.property (E.sum F)

Tactic:
h hR hS
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
Goal:
C : Type u
inst : Category.{v, u} C
P : PreZeroHypercoverFamily.{v, u} C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : P.property E
F : PreZeroHypercover X
hS : P.property F
⊢ P.property (E.sum F)

Tactic:
exact h hR hS
-- 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 : Presieve.{v₁, u₁} X
x y : FamilyOfElements P R
H h : ∀ (Z : C) (f : Z ⟶ X) (hf : R f), x f hf = y f hf
⊢ x = y

Tactic:
funext Z f hf
-- 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 : Presieve.{v₁, u₁} X
x y : FamilyOfElements P R
H : ∀ {Y : C} (f : Y ⟶ X) (hf : R f), x f hf = y f hf
Z : C
f : Z ⟶ X
hf : R f
⊢ x f hf = y f hf

Tactic:
H f hf
-- 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 : Presieve.{v₁, u₁} X
x y : FamilyOfElements P R
H : ∀ {Y : C} (f : Y ⟶ X) (hf : R f), x f hf = y f hf
Z : C
f : Z ⟶ X
hf : R f
⊢ x f hf = y f hf

Tactic:
exact H f hf
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
p : FamilyOfElements P R
φ : P ⟶ Q
Y : C
f : Y ⟶ X
hf : R f
⊢ p.map (R := R) φ f hf =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (op Y)) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (Q.obj (op Y)))
      (p f hf)

Tactic:
rfl

Premises used: CategoryTheory.Presieve.FamilyOfElements.map, rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
p : FamilyOfElements P R
φ : P ⟶ Q
R' : Presieve.{v₁, u₁} X
h : R' ≤ R
⊢ (restrict (R₁ := R') (R₂ := R) h p).map (R := R') φ = restrict (R₁ := R') (R₂ := R) h (p.map (R := R) φ)

Tactic:
rfl

Premises used: CategoryTheory.Presieve.FamilyOfElements.restrict, CategoryTheory.Presieve.FamilyOfElements.map, rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X_1 Y_1 : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
X Y : C
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
⊢ singleton f f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X_1 Y_1 : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
X Y : C
f : X ⟶ Y
x : P.obj (op X)
Z : C
g : Z ⟶ Y
hg : singleton f g
mk : X = X
⊢ Z = X

Tactic:
cases hg
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X_1 Y_1 : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
X Y : C
f : X ⟶ Y
x : P.obj (op X)
⊢ X = X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X_1 Y_1 : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
X Y : C
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
H :
  ∀ ⦃Y_2 : C⦄,
    (fun (x : P.obj (op X)) (Z : C) (g : Z ⟶ Y) (hg : singleton f g) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (eqToHom ⋯))) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
              x :
            (fun (X : Type w) ↦ X) (P.obj (op Z))))
        ((fun (x : FamilyOfElements P (singleton f)) ↦ x f ⋯) x) X f ⋯ =
      x f ⋯
⊢ (fun (x : P.obj (op X)) (Z : C) (g : Z ⟶ Y) (hg : singleton f g) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (eqToHom ⋯))) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            x :
          (fun (X : Type w) ↦ X) (P.obj (op Z))))
      ((fun (x : FamilyOfElements P (singleton f)) ↦ x f ⋯) x) =
    x

Tactic:
ext _ _ ⟨rfl⟩

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X_1 Y_1 : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
X Y_2 : C
f : X ⟶ Y_2
x : FamilyOfElements P (singleton f)
Y : C
⊢ (fun (x : P.obj (op X)) (Z : C) (g : Z ⟶ Y_2) (hg : singleton f g) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (eqToHom ⋯))) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            x :
          (fun (X : Type w) ↦ X) (P.obj (op Z))))
      ((fun (x : FamilyOfElements P (singleton f)) ↦ x f ⋯) x) X f ⋯ =
    x f ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X_1 Y_1 : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
X Y : C
f : X ⟶ Y
x : P.obj (op X)
⊢ (fun (x : FamilyOfElements P (singleton f)) ↦ x f ⋯)
      ((fun (x : P.obj (op X)) (Z : C) (g : Z ⟶ Y) (hg : singleton f g) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (eqToHom ⋯))) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
              x :
            (fun (X : Type w) ↦ X) (P.obj (op Z))))
        x) =
    x

Tactic:
simp
-- 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 : X ⟶ Y
x : P.obj (op X)
⊢ ((singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f)) x f ⋯ = x

Tactic:
simp [singletonEquiv_symm_apply]

Premises used: CategoryTheory.Presieve.FamilyOfElements.singletonEquiv_symm_apply
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
inst_1 : R.HasPairwisePullbacks
mp : x.Compatible (R := R) → x.PullbackCompatible (R := R)
mpr : x.PullbackCompatible (R := R) → x.Compatible (R := R)
⊢ x.Compatible (R := R) ↔ x.PullbackCompatible (R := R)

Tactic:
constructor
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
inst_1 : R.HasPairwisePullbacks
t : x.Compatible (R := R)
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
mp : Eq (α := Limits.pullback f₁ f₂ ⟶ X) (pullback.fst f₁ f₂ ≫ f₁) (pullback.snd f₁ f₂ ≫ f₂)
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback f₁ f₂))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst f₁ f₂))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback f₁ f₂))))
        (x f₁ hf₁) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback f₁ f₂))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd f₁ f₂))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback f₁ f₂))))
        (x f₂ hf₂) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback f₁ f₂))))

Tactic:
apply t
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
inst_1 : R.HasPairwisePullbacks
t : x.Compatible (R := R)
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ HasPullback f₁ f₂

Tactic:
haveI := HasPairwisePullbacks.has_pullbacks hf₁ hf₂
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
inst_1 : R.HasPairwisePullbacks
t : x.Compatible (R := R)
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
this : HasPullback f₁ f₂
⊢ Eq (α := Limits.pullback f₁ f₂ ⟶ X) (pullback.fst f₁ f₂ ≫ f₁) (pullback.snd f₁ f₂ ≫ f₂)

Tactic:
apply pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
inst_1 : R.HasPairwisePullbacks
t : x.PullbackCompatible (R := R)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ HasPullback f₁ f₂

Tactic:
haveI := HasPairwisePullbacks.has_pullbacks hf₁ hf₂
-- 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₁ R₂ : Presieve.{v₁, u₁} X
h : R₁ ≤ R₂
x : FamilyOfElements P R₂
⊢ x.Compatible (R := R₂) → (FamilyOfElements.restrict (R₁ := R₁) (R₂ := R₂) h x).Compatible (R := R₁)

Tactic:
fun q _ _ _ g₁ g₂ _ _ h₁ h₂ comm => q g₁ g₂ (h _ _ h₁) (h _ _ h₂) comm

Premises used: CategoryTheory.Presieve.FamilyOfElements.restrict, CategoryTheory.Presieve.FamilyOfElements.Compatible
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
hx : x.Compatible (R := R)
Y₁ : C
_ :
  ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁)
    (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁)
    (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
_
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
hx : x.Compatible (R := R)
Y₁ Y₂ : C
_ :
  ∀ ⦃Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁)
    (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ ∀ ⦃Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁)
    (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
_
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
hx : x.Compatible (R := R)
Y₁ Y₂ Z : C
_ :
  ∀ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ ∀ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
_
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
hx : x.Compatible (R := R)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
_ :
  ∀ (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ ∀ (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
_
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
hx : x.Compatible (R := R)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
_ :
  ∀ ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ ∀ ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
_
-- 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 : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
hx : x.Compatible (R := R)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
_ :
  ∀ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ ∀ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      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 Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₁ h₁) :
          (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 Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x.sieveExtend (R := R) f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
_