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
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)))
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)))
⊢ 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 ≫ (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)))
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)))
erw₃ :
  F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map (Z₁.hom.op ≫ (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 (Over.Hom.left φ ≫ Z₁.hom).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)))
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)))
erw₃ :
  F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map (Z₁.hom.op ≫ (Over.Hom.left φ).op) ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
erw₄ :
  F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map (Over.Hom.left φ ≫ Z₁.hom).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 ≫ (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
c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) :=
  { pt := F.obj (op Y),
    π :=
      {
        app := fun (x_1 : (Sieve.pullback g S).arrows.categoryᵒᵖ) ↦
          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)
            x_1 with
          | op { obj := Z, property := hZ } =>
            F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))),
        naturality := ⋯ } }
⊢ ∃ (φ : F.obj (op Y) ⟶ G.obj (op Y)),
    ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)), φ ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
have h : ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)),
  (hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
Tactic: use (hG g).lift c
-- 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
hx : x.Compatible (R := S.arrows)
⊢ ∃! t : (presheafHom F G).obj (op X), x.IsAmalgamation (R := S.arrows) t
have hex : ∃ (x_1 : (presheafHom F G).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1
Tactic: apply existsUnique_of_exists_of_unique
-- 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
hx : x.Compatible (R := S.arrows)
hex : ∃ (x_1 : (presheafHom F G).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1
⊢ ∃! t : (presheafHom F G).obj (op X), x.IsAmalgamation (R := S.arrows) t
have hunique : ∀ (y₁ y₂ : (presheafHom F G).obj (op X)),
  x.IsAmalgamation (R := S.arrows) y₁ → x.IsAmalgamation (R := S.arrows) y₂ → y₁ = y₂
Tactic: apply existsUnique_of_exists_of_unique
-- 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
hx : x.Compatible (R := S.arrows)
Y₁ Y₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
⊢ (Functor.op (Over.forget (unop (op X))) ⋙ F).map (op φ) ≫ app hG x hx (unop (op Y₂)).hom =
    app hG x hx (unop (op Y₁)).hom ≫ (Functor.op (Over.forget (unop (op X))) ⋙ G).map (op φ)
have apply : ∀ (j : (Sieve.pullback Y₂.hom S).arrows.categoryᵒᵖ),
  ((Functor.op (Over.forget (unop (op X))) ⋙ F).map (op φ) ≫ app hG x hx (unop (op Y₂)).hom) ≫
      (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app j =
    (app hG x hx (unop (op Y₁)).hom ≫ (Functor.op (Over.forget (unop (op X))) ⋙ G).map (op φ)) ≫
      (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app j
Tactic: apply (hG Y₂.hom).hom_ext
-- 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
hx : x.Compatible (R := S.arrows)
Y₁ Y₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y₁) ⟶
      ((Sieve.pullback Y₂.hom S).arrows.diagram.op ⋙ G).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y₂.left) ↦
            (Sieve.pullback Y₂.hom S).arrows f.hom) Z hZ)))
    (((Functor.op (Over.forget (unop (op X))) ⋙ F).map (op φ) ≫ app hG x hx (unop (op Y₂)).hom) ≫
      (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y₂.left) ↦
            (Sieve.pullback Y₂.hom S).arrows f.hom) Z hZ)))
    ((app hG x hx (unop (op Y₁)).hom ≫ (Functor.op (Over.forget (unop (op X))) ⋙ G).map (op φ)) ≫
      (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y₂.left) ↦
            (Sieve.pullback Y₂.hom S).arrows f.hom) Z hZ)))
have dsimp : (F.map (Over.Hom.left φ).op ≫ app hG x hx Y₂.hom) ≫ G.map Z.hom.op =
  (app hG x hx Y₁.hom ≫ G.map (Over.Hom.left φ).op) ≫ G.map Z.hom.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
hx : x.Compatible (R := S.arrows)
Y₁ Y₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ (F.map (Over.Hom.left φ).op ≫ app hG x hx Y₂.hom) ≫ G.map Z.hom.op =
    (app hG x hx Y₁.hom ≫ G.map (Over.Hom.left φ).op) ≫ G.map Z.hom.op
have rw : F.map (Over.Hom.left φ).op ≫ F.map Z.hom.op ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
  app hG x hx Y₁.hom ≫ G.map (Z.hom ≫ Over.Hom.left φ).op
Tactic: rw [assoc, assoc, app_cond hG x hx Y₂.hom Z.hom hZ, ← G.map_comp, ← op_comp]
-- 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
hx : x.Compatible (R := S.arrows)
Y₁ Y₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ F.map (Over.Hom.left φ).op ≫ F.map Z.hom.op ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
    app hG x hx Y₁.hom ≫ G.map (Z.hom ≫ Over.Hom.left φ).op
have rw : Eq (α := F.obj (op Y₁.left) ⟶ G.obj (op Z.left))
  (F.map ((Over.Hom.left φ).op ≫ Z.hom.op) ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))))
  (F.map ((Over.Hom.left φ).op ≫ Z.hom.op) ≫ (x ((Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom) sorry).app (op (Over.mk (𝟙 Z.left))))
Tactic: rw [app_cond hG x hx Y₁.hom (Z.hom ≫ φ.left) (by simpa using hZ),
            ← F.map_comp_assoc, op_comp]
-- 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
hx : x.Compatible (R := S.arrows)
Y₁ Y₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ Eq (α := F.obj (op Y₁.left) ⟶ G.obj (op Z.left))
    (F.map ((Over.Hom.left φ).op ≫ Z.hom.op) ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))))
    (F.map ((Over.Hom.left φ).op ≫ Z.hom.op) ≫ (x ((Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom) ⋯).app (op (Over.mk (𝟙 Z.left))))
have e_a : Z.hom ≫ Y₂.hom = (Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom
Tactic: congr 3
-- 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
hx : x.Compatible (R := S.arrows)
⊢ ∃ (x_1 : (presheafHom F G).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1
have hex : x.IsAmalgamation (R := S.arrows)
  { app := fun (Y : (Over.{v, u} (unop (op X)))ᵒᵖ) ↦ app hG x hx (unop Y).hom, naturality := sorry }
Tactic: refine ⟨
      { app := fun Y => app hG x hx Y.unop.hom
        naturality := by
          rintro ⟨Y₁ : Over X⟩ ⟨Y₂ : Over X⟩ ⟨φ : Y₂ ⟶ Y₁⟩
          apply (hG Y₂.hom).hom_ext
          rintro ⟨Z : Over Y₂.left, hZ⟩
          dsimp
          rw [assoc, assoc, app_cond hG x hx Y₂.hom Z.hom hZ, ← G.map_comp, ← op_comp]
          rw [app_cond hG x hx Y₁.hom (Z.hom ≫ φ.left) (by simpa using hZ),
            ← F.map_comp_assoc, op_comp]
          congr 3
          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
hx : x.Compatible (R := S.arrows)
⊢ x.IsAmalgamation (R := S.arrows)
    { app := fun (Y : (Over.{v, u} (unop (op X)))ᵒᵖ) ↦ app hG x hx (unop Y).hom, naturality := ⋯ }
have hex : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
  Eq.{v' + 1} (α :=
    (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)))
    (NatTrans.app { app := fun (Y : (Over.{v, u} (unop (op X)))ᵒᵖ) ↦ app hG x hx (unop Y).hom, naturality := sorry }
      (op (Over.mk g)))
    ((x g hg).app (op (Over.mk (𝟙 Y))))
Tactic: rw [PresheafHom.isAmalgamation_iff _ _ hx]
-- 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
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ Eq.{v' + 1} (α :=
    (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)))
    (NatTrans.app { app := fun (Y : (Over.{v, u} (unop (op X)))ᵒᵖ) ↦ app hG x hx (unop Y).hom, naturality := ⋯ }
      (op (Over.mk g)))
    ((x g hg).app (op (Over.mk (𝟙 Y))))
have hex : app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))
Tactic: dsimp
-- 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
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))
have H : app hG x hx g ≫ G.map (Quiver.Hom.op (𝟙 Y)) = F.map (Quiver.Hom.op (𝟙 Y)) ≫ (x (𝟙 Y ≫ g) sorry).app (op (Over.mk (𝟙 Y)))
Tactic: have H := app_cond hG x hx g (𝟙 _) (by simpa using hg)
-- 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
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g ≫ G.map (Quiver.Hom.op (𝟙 Y)) = F.map (Quiver.Hom.op (𝟙 Y)) ≫ (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))
have H₁ : app hG x hx g = (x (𝟙 Y ≫ g) sorry).app (op (Over.mk (𝟙 Y)))
Tactic: rw [op_id, G.map_id, comp_id, F.map_id, id_comp] 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
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ Eq (α := F.obj (op Y) ⟶ G.obj (op Y))
    ((x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y))) :
      (Functor.op (Over.forget (unop (op Y))) ⋙ F).obj (op (Over.mk (𝟙 Y))) ⟶
        (Functor.op (Over.forget (unop (op Y))) ⋙ G).obj (op (Over.mk (𝟙 Y))))
    ((x g hg).app (op (Over.mk (𝟙 Y))))
have e_self : 𝟙 Y ≫ g = g
Tactic: congr
-- 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
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : x.IsAmalgamation (R := S.arrows) y₁
hy₂ : x.IsAmalgamation (R := S.arrows) y₂
⊢ y₁ = y₂
have hy₃ : ∀ (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))))
Tactic: rw [PresheafHom.isAmalgamation_iff _ _ hx] at hy₁ hy₂
Cleared hypotheses: hy₁, hy₂
-- 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
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : x.IsAmalgamation (R := S.arrows) y₁
hy₂ : x.IsAmalgamation (R := S.arrows) y₂
hy₃ :
  ∀ (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₁ = y₂
have hy₄ : ∀ (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))))
Tactic: rw [PresheafHom.isAmalgamation_iff _ _ hx] at hy₁ hy₂
Cleared hypotheses: hy₁, hy₂