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
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
      Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)
    (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (𝟙 (op X))))) :
      (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
        Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)
    (𝟙 (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) :
      (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
        Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)
have h : ∀ (φ : Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)
  (Y : Over.{v, u} (unop (op X))),
  Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶ (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
    (NatTrans.app
        (TypeCat.Fun.toFun
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (𝟙 (op X)))))))
          φ)
        (op Y) :
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶ (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (𝟙 (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G))).toFun
          φ).app
      (op Y))
Tactic: ext φ ⟨Y⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
      Functor.op (Over.forget (unop (op Z))) ⋙ F ⟶ Functor.op (Over.forget (unop (op Z))) ⋙ G)
    (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (op f ≫ op g)))) :
      (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
        Functor.op (Over.forget (unop (op Z))) ⋙ F ⟶ Functor.op (Over.forget (unop (op Z))) ⋙ G)
    (↾(Over.map (Quiver.Hom.unop (op f))).op.whiskerLeft ≫ ↾(Over.map (Quiver.Hom.unop (op g))).op.whiskerLeft :
      (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
        Functor.op (Over.forget (unop (op Z))) ⋙ F ⟶ Functor.op (Over.forget (unop (op Z))) ⋙ G)
have h : ∀ (φ : Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)
  (W : Over.{v, u} (unop (op Z))),
  Eq (α :=
    (Functor.op (Over.forget (unop (op Z))) ⋙ F).obj (op W) ⟶ (Functor.op (Over.forget (unop (op Z))) ⋙ G).obj (op W))
    (NatTrans.app
        (TypeCat.Fun.toFun
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (op f ≫ op g))))))
          φ)
        (op W) :
      (Functor.op (Over.forget (unop (op Z))) ⋙ F).obj (op W) ⟶ (Functor.op (Over.forget (unop (op Z))) ⋙ G).obj (op W))
    ((TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾(Over.map (Quiver.Hom.unop (op f))).op.whiskerLeft ≫ ↾(Over.map (Quiver.Hom.unop (op g))).op.whiskerLeft))
          φ).app
      (op W))
Tactic: ext φ ⟨W⟩
-- 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 Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
h : Z ⟶ X
w : f ≫ g = h
α : (presheafHom F G).obj (op X)
⊢ Eq.{v' + 1} (α :=
    (Functor.op (Over.forget (unop (op Y))) ⋙ F).obj (op (Over.mk f)) ⟶
      (Functor.op (Over.forget (unop (op Y))) ⋙ G).obj (op (Over.mk f)))
    (NatTrans.app
      ((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)))
        α)
      (op (Over.mk f)))
    (α.app (op (Over.mk h)))
have subst : Eq.{v' + 1} (α :=
  (Functor.op (Over.forget (unop (op Y))) ⋙ F).obj (op (Over.mk f)) ⟶
    (Functor.op (Over.forget (unop (op Y))) ⋙ G).obj (op (Over.mk f)))
  (NatTrans.app
    ((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)))
      α)
    (op (Over.mk f)))
  (α.app (op (Over.mk (f ≫ g))))
Tactic: subst w
Cleared hypotheses: h, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫ ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₂)).app (op (Over.mk (𝟙 (unop (op X₂))))))
    (((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk (𝟙 (unop (op X₁))))) ≫ G.map (op f))
have dsimp : Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
  (F.map (op f) ≫
    ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₂)).app
      (op (Over.mk (𝟙 X₂))))
  (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app
      (op (Over.mk (𝟙 X₁))) ≫
    G.map (op f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₂)).app
        (op (Over.mk (𝟙 X₂))))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app
        (op (Over.mk (𝟙 X₁))) ≫
      G.map (op f))
have refine : Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
  (F.map (op f) ≫
    ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₂)).app
      (op (Over.mk (𝟙 X₂))))
  ((Functor.op (Over.forget (unop (op X₁))) ⋙ F).map (Quiver.Hom.op (Over.homMk f sorry)) ≫
    ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk f)))
Tactic: refine Eq.trans ?_ ((s.1 ⟨X₁⟩).naturality
          (Over.homMk f : Over.mk f ⟶ Over.mk (𝟙 X₁)).op)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₂)).app
        (op (Over.mk (𝟙 X₂))))
    ((Functor.op (Over.forget (unop (op X₁))) ⋙ F).map (Quiver.Hom.op (Over.homMk f ⋯)) ≫
      ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk f)))
have rw : Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
  (F.map (op f) ≫
    NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map f.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 X₂)))
        ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)))
      (op (Over.mk (𝟙 X₂))))
  ((Functor.op (Over.forget (unop (op X₁))) ⋙ F).map (Quiver.Hom.op (Over.homMk f sorry)) ≫
    ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk f)))
Tactic: rw [← s.2 f.op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map f.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 X₂)))
          ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)))
        (op (Over.mk (𝟙 X₂))))
    ((Functor.op (Over.forget (unop (op X₁))) ⋙ F).map (Quiver.Hom.op (Over.homMk f ⋯)) ≫
      ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk f)))
have dsimp : Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
  (F.map (op f) ≫
    NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map f.op) :
          (a : (Over.forget X₁).op ⋙ F ⟶ (Over.forget X₁).op ⋙ G) → (Over.forget X₂).op ⋙ F ⟶ (Over.forget X₂).op ⋙ G)
        ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)))
      (op (Over.mk (𝟙 X₂))))
  (F.map f.op ≫
    ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map f.op) :
            (a : (Over.forget X₁).op ⋙ F ⟶ (Over.forget X₁).op ⋙ G) → (Over.forget X₂).op ⋙ F ⟶ (Over.forget X₂).op ⋙ G)
          ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)))
        (op (Over.mk (𝟙 X₂))))
    (F.map f.op ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))
have rw : Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
  (F.map (op f) ≫
    ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))
  (F.map f.op ≫
    ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))
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
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
⊢ (fun (f : F ⟶ G) ↦
        (Subtype.mk (p := fun (x : (j : Cᵒᵖ) → (presheafHom F G).obj j) ↦ x ∈ (presheafHom F G).sections)
            (fun (x : Cᵒᵖ) ↦ Functor.whiskerLeft (Functor.op (Over.forget (unop x))) f) ⋯ :
          { x : (j : Cᵒᵖ) → (presheafHom F G).obj j // x ∈ (presheafHom F G).sections }))
      ((fun (s : (↑(presheafHom F G).sections : Type (max (max u v) v'))) ↦
          { app := fun (X : Cᵒᵖ) ↦ ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) X).app (op (Over.mk (𝟙 (unop X)))),
            naturality := ⋯ : NatTrans F G })
        s) =
    s
have dsimp : Subtype.mk (p := fun (x : (j : Cᵒᵖ) → Functor.op (Over.forget (unop j)) ⋙ F ⟶ Functor.op (Over.forget (unop j)) ⋙ G) ↦
    x ∈ (presheafHom F G).sections)
    (fun (x : Cᵒᵖ) ↦
      Functor.whiskerLeft (Functor.op (Over.forget (unop x)))
        {
          app := fun (X : Cᵒᵖ) ↦
            ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) X).app
              (op (Over.mk (𝟙 (unop X)))),
          naturality := sorry })
    sorry =
  s
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
⊢ Subtype.mk (p := fun (x : (j : Cᵒᵖ) → Functor.op (Over.forget (unop j)) ⋙ F ⟶ Functor.op (Over.forget (unop j)) ⋙ G) ↦
      x ∈ (presheafHom F G).sections)
      (fun (x : Cᵒᵖ) ↦
        Functor.whiskerLeft (Functor.op (Over.forget (unop x)))
          {
            app := fun (X : Cᵒᵖ) ↦
              ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) X).app
                (op (Over.mk (𝟙 (unop X)))),
            naturality := ⋯ })
      ⋯ =
    s
have a : ∀ (X : C) (Y : Over.{v, u} X),
  NatTrans.app
      ((↑(Subtype.mk (p :=
              fun (x : (j : Cᵒᵖ) → Functor.op (Over.forget (unop j)) ⋙ F ⟶ Functor.op (Over.forget (unop j)) ⋙ G) ↦
              x ∈ (presheafHom F G).sections)
              (fun (x : Cᵒᵖ) ↦
                Functor.whiskerLeft (Functor.op (Over.forget (unop x)))
                  {
                    app := fun (X : Cᵒᵖ) ↦
                      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) X).app
                        (op (Over.mk (𝟙 (unop X)))),
                    naturality := sorry })
              sorry) :
          (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G)
        (op X))
      (op Y) =
    ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y)
Tactic: ext ⟨X⟩ ⟨Y : Over X⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X : C
Y : Over.{v, u} X
⊢ NatTrans.app
      ((↑(Subtype.mk (p :=
              fun (x : (j : Cᵒᵖ) → Functor.op (Over.forget (unop j)) ⋙ F ⟶ Functor.op (Over.forget (unop j)) ⋙ G) ↦
              x ∈ (presheafHom F G).sections)
              (fun (x : Cᵒᵖ) ↦
                Functor.whiskerLeft (Functor.op (Over.forget (unop x)))
                  {
                    app := fun (X : Cᵒᵖ) ↦
                      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) X).app
                        (op (Over.mk (𝟙 (unop X)))),
                    naturality := ⋯ })
              ⋯) :
          (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G)
        (op X))
      (op Y) =
    ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y)
have H : (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.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.left)))
    ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X)) =
  (↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op Y.left)
Tactic: have H := s.2 Y.hom.op
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X : C
Y : Over.{v, u} X
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.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.left)))
      ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X)) =
    (↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op Y.left)
⊢ NatTrans.app
      ((↑(Subtype.mk (p :=
              fun (x : (j : Cᵒᵖ) → Functor.op (Over.forget (unop j)) ⋙ F ⟶ Functor.op (Over.forget (unop j)) ⋙ G) ↦
              x ∈ (presheafHom F G).sections)
              (fun (x : Cᵒᵖ) ↦
                Functor.whiskerLeft (Functor.op (Over.forget (unop x)))
                  {
                    app := fun (X : Cᵒᵖ) ↦
                      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) X).app
                        (op (Over.mk (𝟙 (unop X)))),
                    naturality := ⋯ })
              ⋯) :
          (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G)
        (op X))
      (op Y) =
    ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y)
have a : Eq (α := F.obj (op Y.left) ⟶ G.obj (op Y.left))
  (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op Y.left)).app
    (op (Over.mk (𝟙 Y.left))))
  (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y))
Tactic: dsimp at H ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X : C
Y : Over.{v, u} X
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.op) :
        (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) →
          (Over.forget Y.left).op ⋙ F ⟶ (Over.forget Y.left).op ⋙ G)
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)) =
    (↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op Y.left)
⊢ Eq (α := F.obj (op Y.left) ⟶ G.obj (op Y.left))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op Y.left)).app
      (op (Over.mk (𝟙 Y.left))))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y))
have a : Eq.{v' + 1} (α := F.obj (op Y.left) ⟶ G.obj (op Y.left))
  (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.op) :
          (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) →
            (Over.forget Y.left).op ⋙ F ⟶ (Over.forget Y.left).op ⋙ G)
        ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)))
      (op (Over.mk (𝟙 Y.left))) :
    (Functor.op (Over.forget Y.left) ⋙ F).obj (op (Over.mk (𝟙 Y.left))) ⟶
      (Functor.op (Over.forget Y.left) ⋙ G).obj (op (Over.mk (𝟙 Y.left))))
  (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y))
Tactic: rw [← 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)
⊢ x.IsAmalgamation (R := S.arrows) y ↔
    ∀ (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))))
have mp : x.IsAmalgamation (R := S.arrows) y →
  ∀ (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: constructor
-- 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)
mp :
  x.IsAmalgamation (R := S.arrows) y →
    ∀ (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))))
⊢ x.IsAmalgamation (R := S.arrows) y ↔
    ∀ (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))))
have mpr : (∀ (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))))) →
  x.IsAmalgamation (R := S.arrows) y
Tactic: constructor
-- 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 (α :=
    (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))))
have mp : 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)))
  (NatTrans.app
    ((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)
    (op (Over.mk (𝟙 Y))))
Tactic: rw [← h g hg]
-- 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 (α :=
    (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)))
    (NatTrans.app
      ((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)
      (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)))
  (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))))
Tactic: dsimp