awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
h : x.IsAmalgamation (R := S.arrows) y
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ Eq (α := F.obj (op Y) ⟶ G.obj (op Y))
    (y.app (op (Over.mk g)) :
      (Functor.op (Over.forget X) ⋙ F).obj (op (Over.mk g)) ⟶ (Functor.op (Over.forget X) ⋙ G).obj (op (Over.mk g)))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
        y)
      (op (Over.mk (𝟙 Y))))
have mp : Eq (α := F.obj (op Y) ⟶ G.obj (op Y))
  (y.app (op (Over.mk g)) :
    (Functor.op (Over.forget X) ⋙ F).obj (op (Over.mk g)) ⟶ (Functor.op (Over.forget X) ⋙ G).obj (op (Over.mk g)))
  (y.app (op (Over.mk g)))
Tactic: rw [presheafHom_map_app_op_mk_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
h :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
        (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X))) →
          (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y)))
      y =
    x g hg
have mpr : (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
      (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
    y =
  x g hg
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
h :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
        (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
      y =
    x g hg
have mpr : ∀ (W : Over.{v, u} Y),
  NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
        y)
      (op W) =
    (x g hg).app (op W)
Tactic: ext ⟨W : Over Y⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
h :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over.{v, u} Y
⊢ NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
        y)
      (op W) =
    (x g hg).app (op W)
have mpr : Eq (α :=
  (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk (W.hom ≫ g))) ⟶
    (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk (W.hom ≫ g))))
  ((x (W.hom ≫ g) sorry).app (op (Over.mk (𝟙 W.left)))) ((x g hg).app (op W))
Tactic: refine (h W.left (W.hom ≫ g) (S.downward_closed hg _)).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
h :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over.{v, u} Y
H :
  Eq (α := (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Quiver.Hom.op (𝟙 W.left))) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
        (x (W.hom ≫ g) ⋯) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map W.hom.op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
        (x g hg) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk (W.hom ≫ g))) ⟶
      (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk (W.hom ≫ g))))
    ((x (W.hom ≫ g) ⋯).app (op (Over.mk (𝟙 W.left)))) ((x g hg).app (op W))
have H₁ : x (W.hom ≫ g) sorry =
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map W.hom.op) :
      (a : (presheafHom F G).obj (op Y)) → (presheafHom F G).obj (op W.left))
    (x g hg)
Tactic: simp only [op_id, Functor.map_id, id_apply] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
h :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over.{v, u} Y
H :
  x (W.hom ≫ g) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map W.hom.op) :
        (a : (presheafHom F G).obj (op Y)) → (presheafHom F G).obj (op W.left))
      (x g hg)
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk (W.hom ≫ g))) ⟶
      (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk (W.hom ≫ g))))
    ((x (W.hom ≫ g) ⋯).app (op (Over.mk (𝟙 W.left)))) ((x g hg).app (op W))
have mpr : Eq (α :=
  (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk (W.hom ≫ g))) ⟶
    (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk (W.hom ≫ g))))
  ((x g hg).app (op (Over.mk W.hom))) ((x g hg).app (op W))
Tactic: rw [H, presheafHom_map_app _ _ W.hom (by simp)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ Eq.{v' + 1} (α :=
    Functor.obj (C := (Sieve.pullback g S).arrows.categoryᵒᵖ)
        (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y)))
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₁
            hZ₁)) ⟶
      ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₂
            hZ₂)))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := (Sieve.pullback g S).arrows.categoryᵒᵖ)
        (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y)))
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₂
            hZ₂)))
      (Functor.map (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y)))
        (op { hom := f }))
      (match (motive :=
        (x : (Sieve.pullback g S).arrows.categoryᵒᵖ) →
          Functor.obj (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y))) x ⟶
            ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj x)
        op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₂
            hZ₂) with
      | op { obj := Z, property := hZ } =>
        F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left)))))))
    (CategoryStruct.comp (Y :=
      ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₁
            hZ₁)))
      (match (motive :=
        (x : (Sieve.pullback g S).arrows.categoryᵒᵖ) →
          Functor.obj (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y))) x ⟶
            ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj x)
        op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₁
            hZ₁) with
      | op { obj := Z, property := hZ } =>
        F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))))
      (((Sieve.pullback g S).arrows.diagram.op ⋙ G).map (op { hom := f })))
have dsimp : 𝟙 (F.obj (op Y)) ≫ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
  (F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left)))) ≫ G.map (Over.Hom.left f).op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ 𝟙 (F.obj (op Y)) ≫ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    (F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left)))) ≫ G.map (Over.Hom.left f).op
have rw : F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
  F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
Tactic: rw [id_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
have H : Eq (α := (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
        (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₁.left))) →
          (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
      (x (Z₁.hom ≫ g) hZ₁) :
    (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Quiver.Hom.op (𝟙 Z₂.left))) :
        (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left))) →
          (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
      (x (Z₂.hom ≫ g) hZ₂) :
    (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
Tactic: have H := hx f.left (𝟙 _) hZ₁ hZ₂ (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H :
  Eq (α := (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₁.left))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
        (x (Z₁.hom ≫ g) hZ₁) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Quiver.Hom.op (𝟙 Z₂.left))) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
        (x (Z₂.hom ≫ g) hZ₂) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
have H₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
      (a : (presheafHom F G).obj (op Z₁.left)) → (presheafHom F G).obj (op Z₂.left))
    (x (Z₁.hom ≫ g) hZ₁) =
  x (Z₂.hom ≫ g) hZ₂
Tactic: simp only [op_id, Functor.map_id, id_apply] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
        (a : (presheafHom F G).obj (op Z₁.left)) → (presheafHom F G).obj (op Z₂.left))
      (x (Z₁.hom ≫ g) hZ₁) =
    x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
have H' : (Functor.op (Over.forget (unop (op Z₁.left))) ⋙ F).map φ.op ≫
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
  (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ (Functor.op (Over.forget (unop (op Z₁.left))) ⋙ G).map φ.op
Tactic: have H' := (x (Z₁.hom ≫ g) hZ₁).naturality φ.op
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
        (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
          (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
      (x (Z₁.hom ≫ g) hZ₁) =
    x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
have erw : F.map Z₂.hom.op ≫
    NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
          (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
            (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
        (x (Z₁.hom ≫ g) hZ₁))
      (op (Over.mk (𝟙 Z₂.left))) =
  F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
Tactic: erw [← H, ← H', presheafHom_map_app_op_mk_id, ← F.map_comp_assoc,
              ← op_comp, Over.w f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
        (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
          (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
      (x (Z₁.hom ≫ g) hZ₁) =
    x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
erw :
  F.map Z₂.hom.op ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
            (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
              (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
          (x (Z₁.hom ≫ g) hZ₁))
        (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
have erw₁ : F.map Z₂.hom.op ≫
    NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
          (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
            (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
        (x (Z₁.hom ≫ g) hZ₁))
      (op (Over.mk (𝟙 Z₂.left))) =
  F.map Z₁.hom.op ≫ F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
Tactic: erw [← H, ← H', presheafHom_map_app_op_mk_id, ← F.map_comp_assoc,
              ← op_comp, Over.w f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
        (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
          (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
      (x (Z₁.hom ≫ g) hZ₁) =
    x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
erw :
  F.map Z₂.hom.op ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
            (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
              (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
          (x (Z₁.hom ≫ g) hZ₁))
        (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
erw₁ :
  F.map Z₂.hom.op ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
            (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
              (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
          (x (Z₁.hom ≫ g) hZ₁))
        (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
have erw₂ : F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
  F.map Z₁.hom.op ≫ F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
Tactic: erw [← H, ← H', presheafHom_map_app_op_mk_id, ← F.map_comp_assoc,
              ← op_comp, Over.w f]