awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ_1 : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ'_1 : Sheaf K (Type v)
α : G.op ⋙ ℱ_1 ⟶ G.op ⋙ ℱ'_1.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : D
x : ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.inv X ≫ appHom i.hom X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x
have h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
  Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.inv X ≫ appHom i.hom X)).toFun x) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
Tactic: apply Functor.IsCoverDense.ext G
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Dᵒᵖ
f : X ⟶ Y
⊢ ℱ.map f ≫ appHom α (unop Y) = appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f
have h : ∀ (x : ℱ.obj X),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ appHom α (unop Y))).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ appHom α (unop Y))).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun x
have h : ∀ ⦃Y_1 : C⦄ (f_1 : G.obj Y_1 ⟶ unop Y),
  Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f_1.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (unop Y)))) →
            (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y_1))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ appHom α (unop Y))).toFun x) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f_1.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (unop Y)))) →
            (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y_1))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun
          x) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y_1))))
Tactic: apply Functor.IsCoverDense.ext G
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ unop Y
⊢ Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y'))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (unop Y)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y'))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ appHom α (unop Y))).toFun x) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y'))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (unop Y)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y'))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun
          x) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y'))))
have h : Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op) :
        (a : ℱ'.obj.obj (op (unop Y))) → ℱ'.obj.obj (op (G.obj Y')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop Y)) : (a : ℱ.obj Y) → ℱ'.obj.obj Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f) : (a : ℱ.obj X) → ℱ.obj Y) x : ℱ.obj Y) :
        ℱ'.obj (P := Presheaf.IsSheaf K).obj Y) :
    ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (f ≫ f'.op)) :
        (a : ℱ'.obj.obj X) → ℱ'.obj.obj (op (G.obj Y')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X)) : (a : ℱ.obj X) → ℱ'.obj.obj X) x :
        ℱ'.obj (P := Presheaf.IsSheaf K).obj X) :
    ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
Tactic: simp only [TypeCat.Fun.toFun_apply, types_comp_apply, ← map_comp_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ unop Y
⊢ Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op) :
          (a : ℱ'.obj.obj (op (unop Y))) → ℱ'.obj.obj (op (G.obj Y')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop Y)) : (a : ℱ.obj Y) → ℱ'.obj.obj Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f) : (a : ℱ.obj X) → ℱ.obj Y) x : ℱ.obj Y) :
          ℱ'.obj (P := Presheaf.IsSheaf K).obj Y) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (f ≫ f'.op)) :
          (a : ℱ'.obj.obj X) → ℱ'.obj.obj (op (G.obj Y')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X)) : (a : ℱ.obj X) → ℱ'.obj.obj X) x :
          ℱ'.obj (P := Presheaf.IsSheaf K).obj X) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
have h : Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y')) :
        (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y'))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f'.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (unop Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y'))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f) : (a : ℱ.obj X) → ℱ.obj Y) x : ℱ.obj Y) :
        (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y')))) :
    (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y')) :
        (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y'))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (f ≫ f'.op)) :
            (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (unop X)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y'))))
          x :
        (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y')))) :
    (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y')))
Tactic: rw [appHom_restrict, appHom_restrict]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
⊢ (coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).map f ≫ presheafHom (homOver α (unop Y)) =
    presheafHom (homOver α (unop X)) ≫
      (coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) (ℱ'.obj (P := Presheaf.IsSheaf K))).map f
have w : ∀ (U : Dᵒᵖ) (x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).map f ≫ presheafHom (homOver α (unop Y))).app U)).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((presheafHom (homOver α (unop X)) ≫
                (coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) (ℱ'.obj (P := Presheaf.IsSheaf K))).map f).app
            U)).toFun
      x
Tactic: ext U x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).map f ≫ presheafHom (homOver α (unop Y))).app U)).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((presheafHom (homOver α (unop X)) ≫
                (coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) (ℱ'.obj (P := Presheaf.IsSheaf K))).map f).app
            U)).toFun
      x
have w : Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
      (f.unop ≫ x) :
    (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
  (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
        x :
    unop Y ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (unop U)))
Tactic: change
      appHom (homOver α (unop Y)) (unop U) (f.unop ≫ x) =
        f.unop ≫ appHom (homOver α (unop X)) (unop U) x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
⊢ Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
        (f.unop ≫ x) :
      (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    (f.unop ≫
        (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
              (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
          x :
      unop Y ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (unop U)))
have w : Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
  (f.unop ≫
    (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
      x)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
      (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
        (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
    (f.unop ≫ x))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
⊢ Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
        x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
      (f.unop ≫ x))
have w : Membership.mem (γ := Set (Sieve.{v_2, u_2} (unop U))) ((K : (a : D) → Set (Sieve a)) (unop U))
  (Sieve.coverByImage G (unop U))
Tactic: apply sheaf_eq_amalgamation
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
w :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (unop U))) ((K : (a : D) → Set (Sieve a)) (unop U))
    (Sieve.coverByImage G (unop U))
⊢ Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
        x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
      (f.unop ≫ x))
have w₁ : (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).Compatible (R := Sieve.arrows (Sieve.coverByImage G (unop U)))
Tactic: apply sheaf_eq_amalgamation
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
w :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (unop U))) ((K : (a : D) → Set (Sieve a)) (unop U))
    (Sieve.coverByImage G (unop U))
w₁ :
  (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).Compatible (R := Sieve.arrows (Sieve.coverByImage G (unop U)))
⊢ Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
        x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
      (f.unop ≫ x))
have w₂ : (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).IsAmalgamation (R := Sieve.arrows (Sieve.coverByImage G (unop U)))
  (f.unop ≫
    (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
      x)
Tactic: apply sheaf_eq_amalgamation
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop Y))).map f'.op) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop Y))).obj (op Y')))
      (f.unop ≫
        (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
              (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
          x) =
    pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x) f' hf'
have w : (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
        x) ≫
    ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op =
  (((f.unop ≫ x) ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫
    ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op
Tactic: dsimp