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)
X Y : C
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
refine :
  ∀
    (H :
      ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f →
          Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
                (x f ⋯) :
              (fun (X : Type w) ↦ X) (P.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
                (x f ⋯) :
              (fun (X : Type w) ↦ X) (P.obj (op Z))))
    (Y₁ Y₂ Z : C) (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) (f₁ : Y₁ ⟶ Y) (f₂ : Y₂ ⟶ Y) (h₁ : singleton f f₁) (h₂ : singleton f 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 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 f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ x.Compatible (R := singleton f) ↔
    ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f →
        Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
              (x f ⋯) :
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
              (x f ⋯) :
            (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
refine ⟨fun H Z p₁ p₂ h ↦ H _ _ _ _ h, fun H Y₁ Y₂ Z g₁ g₂ f₁ 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_1 : C
f : X ⟶ Y_1
x : FamilyOfElements P (singleton f)
H :
  ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
    p₁ ≫ f = p₂ ≫ f →
      Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x f ⋯) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x f ⋯) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
Z Y_2 : C
g₁ : Z ⟶ X
Y : C
g₂ : Z ⟶ X
h : 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 X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f ⋯) :
      (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 X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f ⋯) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
H _ _ h
-- 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_1 : C
f : X ⟶ Y_1
x : FamilyOfElements P (singleton f)
H :
  ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
    p₁ ≫ f = p₂ ≫ f →
      Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x f ⋯) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
            (x f ⋯) :
          (fun (X : Type w) ↦ X) (P.obj (op Z)))
Z Y_2 : C
g₁ : Z ⟶ X
Y : C
g₂ : Z ⟶ X
h : 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 X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f ⋯) :
      (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 X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f ⋯) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
exact H _ _ h
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
Z : D
T : Presieve.{v₁, u₁} (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible (R := T)
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.map g₁ ≫ F.map f₁ = F.map g₂ ≫ F.map f₂

Tactic:
simp only [← F.map_comp, eq]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
Z : D
T : Presieve.{v₁, u₁} (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible (R := T)
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type w) ↦ X) ((F.op ⋙ P).obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.op ⋙ P).map g₁.op) :
          (a : (fun (X : Type w) ↦ X) ((F.op ⋙ P).obj (op Z₁))) → (fun (X : Type w) ↦ X) ((F.op ⋙ P).obj (op W)))
        (FamilyOfElements.functorPullback F (T := T) x f₁ h₁) :
      (fun (X : Type w) ↦ X) ((F.op ⋙ P).obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.op ⋙ P).map g₂.op) :
          (a : (fun (X : Type w) ↦ X) ((F.op ⋙ P).obj (op Z₂))) → (fun (X : Type w) ↦ X) ((F.op ⋙ P).obj (op W)))
        (FamilyOfElements.functorPullback F (T := T) x f₂ h₂) :
      (fun (X : Type w) ↦ X) ((F.op ⋙ P).obj (op W)))

Tactic:
exact h (F.map g₁) (F.map g₂) h₁ h₂ (by simp only [← F.map_comp, eq])

Premises used: CategoryTheory.Functor.map
-- 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
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
X : D
T : Presieve.{v₂, u₂} X
x : FamilyOfElements (F.op ⋙ P) T
Y : C
f : Y ⟶ F.obj X
h : Presieve.functorPushforward F T f
obtain : (Z : D) → (g : Z ⟶ X) → (h : Y ⟶ F.obj Z) → (h₁ : T g) → f = h ≫ F.map g → P.obj (op Y)
⊢ P.obj (op Y)

Tactic:
obtain ⟨Z, g, h, h₁, _⟩ := getFunctorPushforwardStructure h

Premises used: CategoryTheory.Presieve.getFunctorPushforwardStructure
-- 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
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
X : D
T : Presieve.{v₂, u₂} X
x : FamilyOfElements (F.op ⋙ P) T
Y : C
f : Y ⟶ F.obj X
h_1 : Presieve.functorPushforward F T f
Z : D
g : Z ⟶ X
h : Y ⟶ F.obj Z
h₁ : T g
fac : f = h ≫ F.map g
⊢ P.obj (op Y)

Tactic:
exact P.map h.op (x g h₁)

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, DFunLike.coe
-- 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
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.Compatible (R := S.arrows)
simp : ∀ (h : x.SieveCompatible), (FamilyOfElements.pullback f x).SieveCompatible
⊢ (FamilyOfElements.pullback f x).Compatible (R := (Sieve.pullback f S).arrows)

Tactic:
simp only [compatible_iff_sieveCompatible] at h ⊢

Premises used: CategoryTheory.Presieve.compatible_iff_sieveCompatible
-- 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
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
unfold :
  x ((f₂ ≫ f₁) ≫ f) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f₂.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op W))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
      (x (f₁ ≫ f) hf)
⊢ FamilyOfElements.pullback f x (f₂ ≫ f₁) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f₂.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op W))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
      (FamilyOfElements.pullback f x f₁ hf)

Tactic:
unfold FamilyOfElements.pullback

Premises used: CategoryTheory.Presieve.FamilyOfElements.pullback
-- 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
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
rw : x ((f₂ ≫ f₁) ≫ f) ⋯ = x (f₂ ≫ f₁ ≫ f) ⋯
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f₂.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op W))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
      (x (f₁ ≫ f) hf)

Tactic:
rw [← h (f₁ ≫ f) f₂ hf]

Premises used: CategoryTheory.CategoryStruct.comp
-- 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
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
e_f : (f₂ ≫ f₁) ≫ f = f₂ ≫ f₁ ≫ f
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = x (f₂ ≫ f₁ ≫ f) ⋯

Tactic:
congr 1
-- 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
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ (f₂ ≫ f₁) ≫ f = f₂ ≫ f₁ ≫ f

Tactic:
simp only [assoc]

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 : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
⊢ x.map (R := R) (𝟙 P) = x

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 U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
f : P ⟶ Q
g : Q ⟶ U
⊢ (x.map (R := R) f).map (R := R) g = x.map (R := R) (f ≫ g)

Tactic:
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
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible (R := R)
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
unfold :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (Q.obj (op Z₁))) → (fun (X : Type w) ↦ X) (Q.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z₁)) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Z₁))) → (fun (X : Type w) ↦ X) (Q.obj (op Z₁)))
            (x f₁ h₁) :
          (fun (X : Type w) ↦ X) (Q.obj (op Z₁))) :
      (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (Q.obj (op Z₂))) → (fun (X : Type w) ↦ X) (Q.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z₂)) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Z₂))) → (fun (X : Type w) ↦ X) (Q.obj (op Z₂)))
            (x f₂ h₂) :
          (fun (X : Type w) ↦ X) (Q.obj (op Z₂))) :
      (fun (X : Type w) ↦ X) (Q.obj (op W)))
⊢ Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (Q.obj (op Z₁))) → (fun (X : Type w) ↦ X) (Q.obj (op W)))
        (x.map (R := R) f f₁ h₁) :
      (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (Q.obj (op Z₂))) → (fun (X : Type w) ↦ X) (Q.obj (op W)))
        (x.map (R := R) f f₂ h₂) :
      (fun (X : Type w) ↦ X) (Q.obj (op W)))

Tactic:
unfold FamilyOfElements.map

Premises used: CategoryTheory.Presieve.FamilyOfElements.map
-- 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
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation (R := R) t
Y : C
g : Y ⟶ X
hg : R g
dsimp :
  Eq (α := Q.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g.op) : (a : Q.obj (op X)) → Q.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) : (a : P.obj (op X)) → Q.obj (op X)) t :
          Q.obj (op X)) :
      Q.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) : (a : P.obj (op Y)) → Q.obj (op Y)) (x g hg) :
      Q.obj (op Y))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g.op) :
        (a : (fun (X : Type w) ↦ X) (Q.obj (op X))) → (fun (X : Type w) ↦ X) (Q.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (Q.obj (op X)))
          t :
        (fun (X : Type w) ↦ X) (Q.obj (op X))) =
    x.map (R := R) f g hg

Tactic:
dsimp [FamilyOfElements.map]

Premises used: CategoryTheory.Presieve.FamilyOfElements.map
-- 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
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation (R := R) t
Y : C
g : Y ⟶ X
hg : R g
change :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X) ≫ Q.map g.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (Q.obj (op Y)))
        t :
      (fun (X : Type w) ↦ X) (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) : (a : P.obj (op Y)) → Q.obj (op Y)) (x g hg) :
      Q.obj (op Y))
⊢ Eq (α := Q.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g.op) : (a : Q.obj (op X)) → Q.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) : (a : P.obj (op X)) → Q.obj (op X)) t :
          Q.obj (op X)) :
      Q.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) : (a : P.obj (op Y)) → Q.obj (op Y)) (x g hg) :
      Q.obj (op Y))

Tactic:
change (f.app _ ≫ Q.map _) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.NatTrans.app
-- 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
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation (R := R) t
Y : C
g : Y ⟶ X
hg : R g
rw :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op ≫ f.app (op Y)) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (Q.obj (op Y)))
        t :
      (fun (X : Type w) ↦ X) (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) : (a : P.obj (op Y)) → Q.obj (op Y)) (x g hg) :
      Q.obj (op Y))
rw₁ :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) : (a : P.obj (op Y)) → Q.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) : (a : P.obj (op X)) → P.obj (op Y)) t : P.obj (op Y)) :
      Q.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) : (a : P.obj (op Y)) → Q.obj (op Y)) (x g hg) :
      Q.obj (op Y))
rw₂ rw₃ :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) : (a : P.obj (op Y)) → Q.obj (op Y)) (x g hg) :
      Q.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) : (a : P.obj (op Y)) → Q.obj (op Y)) (x g hg) :
      Q.obj (op Y))
⊢ Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X) ≫ Q.map g.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (Q.obj (op Y)))
        t :
      (fun (X : Type w) ↦ X) (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) : (a : P.obj (op Y)) → Q.obj (op Y)) (x g hg) :
      Q.obj (op Y))

Tactic:
rw [← f.naturality, comp_apply, h g hg]

Premises used: CategoryTheory.comp_apply, CategoryTheory.NatTrans.naturality
-- 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
h : ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t
obtain : ∀ (t : P.obj (op X)) (ht : x.IsAmalgamation (R := R) t), x.Compatible (R := R)
⊢ x.Compatible (R := R)

Tactic:
obtain ⟨t, ht⟩ := h
-- 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
t : P.obj (op X)
ht : x.IsAmalgamation (R := R) t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
rw :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₂ ≫ f₂).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → P.obj (op Z))
        t :
      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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f₂.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y₂)))
            t :
          (fun (X : Type w) ↦ X) (P.obj (op Y₂))) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ 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 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 f₂ h₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
rw [← ht _ h₁, ← ht _ h₂, ← comp_apply, ← Functor.map_comp, ← op_comp, comm]

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
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation (R := R) t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (g₂ ≫ f₂).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → P.obj (op Z))
        t :
      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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f₂.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y₂)))
            t :
          (fun (X : Type w) ↦ X) (P.obj (op Y₂))) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

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 : C
R₁ R₂ : Presieve.{v₁, u₁} X
h : R₁ ≤ R₂
x : FamilyOfElements P R₂
t : P.obj (op X)
ht : x.IsAmalgamation (R := R₂) t
⊢ (FamilyOfElements.restrict (R₁ := R₁) (R₂ := R₂) h x).IsAmalgamation (R := R₁) t

Tactic:
fun Y f hf =>
  ht f (h Y _ hf)

Premises used: CategoryTheory.Presieve.FamilyOfElements.restrict, CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation
-- 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 : FamilyOfElements P (singleton f)
y : P.obj (op Y)
⊢ x.IsAmalgamation (R := singleton f) y ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
        y =
      x f ⋯

Tactic:
⟨fun H ↦ H _ _, ?_⟩

Premises used: CategoryTheory.Presieve.singleton.mk, Iff.intro
-- 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 : FamilyOfElements P (singleton f)
y : P.obj (op Y)
refine :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
        y =
      x f ⋯ →
    x.IsAmalgamation (R := singleton f) y
⊢ x.IsAmalgamation (R := singleton f) y ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
        y =
      x f ⋯

Tactic:
refine ⟨fun H ↦ H _ _, ?_⟩
-- 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_1 : C
f : X ⟶ Y_1
x : FamilyOfElements P (singleton f)
y : P.obj (op Y_1)
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y_1))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      y =
    x f ⋯
Y : C
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y_1))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      y =
    x f ⋯

Tactic:
H
-- 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_1 : C
f : X ⟶ Y_1
x : FamilyOfElements P (singleton f)
y : P.obj (op Y_1)
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y_1))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      y =
    x f ⋯
Y : C
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y_1))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      y =
    x f ⋯

Tactic:
exact H