awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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 (generate R).arrows
t : x.SieveCompatible
⊢ (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).sieveExtend (R := R) = x
have h : ∀ (x_1 : C) (x_2 : x_1 ⟶ X) (h : (generate R).arrows x_2),
  (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) sorry x).sieveExtend (R := R) x_2 h = x x_2 h
Tactic: funext _ _ h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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 (generate R).arrows
t : x.SieveCompatible
x_1 : C
x_2 : x_1 ⟶ X
h : (generate R).arrows x_2
⊢ (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).sieveExtend (R := R) x_2 h = x x_2 h
have h₁ : x
    (sorry.choose (p :=
        fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
        ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
          R g ∧ h_1 ≫ g = x_2) ≫
      sorry.choose (p := fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X) ↦
        R g ∧
          sorry.choose (p :=
                fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
                ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
                  R g ∧ h_1 ≫ g = x_2) ≫
              g =
            x_2))
    sorry =
  x x_2 h
Tactic: apply (t _ _ _).symm.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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 (generate R).arrows
t : x.SieveCompatible
x_1 : C
x_2 : x_1 ⟶ X
h : (generate R).arrows x_2
⊢ x
      (⋯.choose (p :=
          fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
          ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
            R g ∧ h_1 ≫ g = x_2) ≫
        ⋯.choose (p :=
          fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X) ↦
          R g ∧
            ⋯.choose (p :=
                  fun
                    (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
                  ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
                    R g ∧ h_1 ≫ g = x_2) ≫
                g =
              x_2))
      ⋯ =
    x x_2 h
have h₁ : sorry.choose (p := fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
      ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
        R g ∧ h_1 ≫ g = x_2) ≫
    sorry.choose (p := fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X) ↦
      R g ∧
        sorry.choose (p :=
              fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
              ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
                R g ∧ h_1 ≫ g = x_2) ≫
            g =
          x_2) =
  x_2
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible (R := (generate R).arrows)
t₂ : x₂.Compatible (R := (generate R).arrows)
h :
  FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₁ =
    FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₂
⊢ x₁ = x₂
have rw : (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) sorry x₁).sieveExtend (R := R) =
  (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) sorry x₂).sieveExtend (R := R)
Tactic: rw [← extend_restrict t₁, ← extend_restrict t₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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)
⊢ 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)))
have 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 sorry) :
            (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 sorry) :
            (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)))
Tactic: refine ⟨fun H Z p₁ p₂ h ↦ H _ _ _ _ h, fun H Y₁ Y₂ Z g₁ g₂ f₁ f₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ P.obj (op Y)
have obtain : (Z : D) → (g : Z ⟶ X) → (h : Y ⟶ F.obj Z) → (h₁ : T g) → f = h ≫ F.map g → P.obj (op Y)
Tactic: obtain ⟨Z, g, h, h₁, _⟩ := getFunctorPushforwardStructure h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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)
⊢ (FamilyOfElements.pullback f x).Compatible (R := (Sieve.pullback f S).arrows)
have simp : ∀ (h : x.SieveCompatible), (FamilyOfElements.pullback f x).SieveCompatible
Tactic: simp only [compatible_iff_sieveCompatible] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₁
⊢ 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)
have unfold : x ((f₂ ≫ f₁) ≫ f) sorry =
  (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: unfold FamilyOfElements.pullback
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₁
⊢ 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)
have rw : x ((f₂ ≫ f₁) ≫ f) sorry = x (f₂ ≫ f₁ ≫ f) sorry
Tactic: rw [← h (f₁ ≫ f) f₂ hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = x (f₂ ≫ f₁ ≫ f) ⋯
have e_f : (f₂ ≫ f₁) ≫ f = f₂ ≫ f₁ ≫ f
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₂
⊢ 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)))
have 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)))
Tactic: unfold FamilyOfElements.map
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₂
⊢ 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)))
have rwa : Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) : (a : P.obj (op Z₁)) → P.obj (op W)) (x f₁ h₁) :
        P.obj (op W)) :
    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)))
Tactic: rwa [← NatTrans.naturality_apply, ← NatTrans.naturality_apply, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₂
rwa :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) : (a : P.obj (op Z₁)) → P.obj (op W)) (x f₁ h₁) :
          P.obj (op W)) :
      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)))
        ((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)))
have rwa₁ : Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) : (a : P.obj (op Z₁)) → P.obj (op W)) (x f₁ h₁) :
        P.obj (op W)) :
    Q.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) : (a : P.obj (op Z₂)) → P.obj (op W)) (x f₂ h₂) :
        P.obj (op W)) :
    Q.obj (op W))
Tactic: rwa [← NatTrans.naturality_apply, ← NatTrans.naturality_apply, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ (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
have 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))
Tactic: dsimp [FamilyOfElements.map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ 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))
have 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))
Tactic: change (f.app _ ≫ Q.map _) _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ 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))
have 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))
Tactic: rw [← f.naturality, comp_apply, h g hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← f.naturality, comp_apply, h g hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← f.naturality, comp_apply, h g hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ x.Compatible (R := R)
have obtain : ∀ (t : P.obj (op X)) (ht : x.IsAmalgamation (R := R) t), x.Compatible (R := R)
Tactic: obtain ⟨t, ht⟩ := h
Cleared hypotheses: h