awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
h₁ :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
          Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right)) S)
          (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯)),
    (f ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫ F.map I.f.op =
      (g ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫ F.map I.f.op
⊢ Eq (α := W ⟶ (StructuredArrow.proj (op X) G.op ⋙ F).obj j)
    (f ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j)
    (g ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j)

Tactic:
apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable j.hom.unop S.2)⟩

Premises used: Quiver.Hom.unop, CategoryTheory.StructuredArrow.hom, CategoryTheory.GrothendieckTopology.pullback_stable, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.cover_lift, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W_1 : A
f g : W_1 ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
            Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right))
              S)
            (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) :
        Sieve (unop j.right)).arrows
    i
⊢ f ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi : S.Arrow }.f.op =
    g ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi }.f.op

Tactic:
have eq := h (GrothendieckTopology.Cover.Arrow.mk _ (G.map i ≫ j.hom.unop) hi)
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W_1 : A
f g : W_1 ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
            Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right))
              S)
            (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) :
        Sieve (unop j.right)).arrows
    i
eq :
  f ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi : S.Arrow }.f.op =
    g ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi }.f.op
h₁ : (f ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op = (g ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op
⊢ (f ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫
      F.map
        { Y := W, f := i, hf := hi :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
                  Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right)))
                    ((J : (a : C) → Set (Sieve a)) (unop j.right)) S)
                  (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) }.f.op =
    (g ≫ NatTrans.app (Cone.π ((Functor.RightExtension.mk R α).coneAt (op X))) j) ≫
      F.map
        { Y := W, f := i, hf := hi :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
                  Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right)))
                    ((J : (a : C) → Set (Sieve a)) (unop j.right)) S)
                  (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) }.f.op

Tactic:
dsimp at eq ⊢
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W_1 : A
f g : W_1 ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
            Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right))
              S)
            (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) :
        Sieve (unop j.right)).arrows
    i
eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)
h₁ : f ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)
⊢ (f ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op = (g ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op

Tactic:
simp only [Category.assoc, ← NatTrans.naturality, Functor.comp_map, ← Functor.map_comp_assoc,
    Functor.op_map, Quiver.Hom.unop_op]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.op_map
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W_1 : A
f g : W_1 ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (unop j.right)) ↦
            Membership.mem (γ := Set (Sieve.{v_1, u_1} (unop j.right))) ((J : (a : C) → Set (Sieve a)) (unop j.right))
              S)
            (Sieve.functorPullback G (Sieve.pullback j.hom.unop (↑S : Sieve X))) ⋯) :
        Sieve (unop j.right)).arrows
    i
eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)
h₁ h₂ : g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)
⊢ f ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)

Tactic:
rw [reassoc_of% eq]
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf.{v_1, w', u_1, w} J A
rw :
  ∀ (X : D) (S : K.Cover X), Nonempty (IsLimit (S.multifork (Functor.obj G.op.ran (ℱ.obj (P := Presheaf.IsSheaf J)))))
⊢ Presheaf.IsSheaf K (Functor.obj G.op.ran (ℱ.obj (P := Presheaf.IsSheaf J)))

Tactic:
rw [Presheaf.isSheaf_iff_multifork]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_multifork
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf.{v_1, w', u_1, w} J A
X : D
S : K.Cover X
⊢ Nonempty (IsLimit (S.multifork (Functor.obj G.op.ran (ℱ.obj (P := Presheaf.IsSheaf J)))))

Tactic:
⟨RanIsSheafOfIsCocontinuous.isLimitMultifork ℱ.2
    (G.op.isPointwiseRightKanExtensionRanCounit ℱ.obj) S⟩

Premises used: CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounit, CategoryTheory.ObjectProperty.FullSubcategory.obj, Nonempty.intro, CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf.{v_1, w', u_1, w} J A
X : D
S : K.Cover X
⊢ Nonempty (IsLimit (S.multifork (Functor.obj G.op.ran (ℱ.obj (P := Presheaf.IsSheaf J)))))

Tactic:
exact ⟨RanIsSheafOfIsCocontinuous.isLimitMultifork ℱ.2
    (G.op.isPointwiseRightKanExtensionRanCounit ℱ.obj) S⟩
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
inst_5 : G.IsContinuous J K
F : Sheaf.{v_2, w', u_2, w} K A
apply :
  Eq (α :=
    obj (sheafToPresheaf K A) (obj (𝟭 (Sheaf.{v_2, w', u_2, w} K A)) F) ⟶
      obj (sheafToPresheaf K A) (obj (G.sheafPushforwardContinuous A J K ⋙ G.sheafPushforwardCocontinuous A J K) F))
    (CategoryStruct.comp (Y := obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (obj (sheafToPresheaf K A) F))
      (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (obj (sheafToPresheaf K A) F))
      (map G.op.ran (NatTrans.app (Iso.hom (Iso.symm (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K))) F) ≫
        NatTrans.app (Iso.hom (Iso.symm (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K)))
          (obj (G.sheafPushforwardContinuous A J K) F)))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)))
⊢ Eq (α :=
    (obj (𝟭 (Sheaf.{v_2, w', u_2, w} K A)) F).obj (P := Presheaf.IsSheaf K) ⟶
      (obj (G.sheafPushforwardContinuous A J K ⋙ G.sheafPushforwardCocontinuous A J K) F).obj (P := Presheaf.IsSheaf K))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.unit (G.sheafAdjunctionCocontinuous A J K)) F))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)))

Tactic:
apply ((G.op.ranAdjunction A).map_restrictFullyFaithful_unit_app
    (fullyFaithfulSheafToPresheaf K A) (fullyFaithfulSheafToPresheaf J A)
    (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm
    (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm F).trans

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso, CategoryTheory.Functor.ranAdjunction, CategoryTheory.Iso.symm, CategoryTheory.fullyFaithfulSheafToPresheaf, CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app, CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
inst_5 : G.IsContinuous J K
F : Sheaf.{v_2, w', u_2, w} K A
dsimp :
  Eq (α :=
    F.obj (P := Presheaf.IsSheaf K) ⟶
      (obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
        Presheaf.IsSheaf K))
    (CategoryStruct.comp (Y := obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)))
      (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) :
        obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) (F.obj (P := Presheaf.IsSheaf K)) ⟶
          obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (F.obj (P := Presheaf.IsSheaf K)))
      (CategoryStruct.comp (Y :=
        obj G.op.ran ((obj (G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J)))
        (map G.op.ran (NatTrans.app (Iso.inv (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K)) F) :
          obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)) ⟶
            obj G.op.ran ((obj (G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J)))
        (𝟙
            ((obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
              Presheaf.IsSheaf K)) :
          (obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
              Presheaf.IsSheaf K) ⟶
            (obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
              Presheaf.IsSheaf K))))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)))
⊢ Eq (α :=
    obj (sheafToPresheaf K A) (obj (𝟭 (Sheaf.{v_2, w', u_2, w} K A)) F) ⟶
      obj (sheafToPresheaf K A) (obj (G.sheafPushforwardContinuous A J K ⋙ G.sheafPushforwardCocontinuous A J K) F))
    (CategoryStruct.comp (Y := obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (obj (sheafToPresheaf K A) F))
      (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (obj (sheafToPresheaf K A) F))
      (map G.op.ran (NatTrans.app (Iso.hom (Iso.symm (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K))) F) ≫
        NatTrans.app (Iso.hom (Iso.symm (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K)))
          (obj (G.sheafPushforwardContinuous A J K) F)))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
inst_5 : G.IsContinuous J K
F : Sheaf.{v_2, w', u_2, w} K A
erw :
  NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) ≫
      𝟙 (obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K))) ≫
        𝟙
          ((obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
            Presheaf.IsSheaf K)) =
    NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K))
⊢ Eq (α :=
    F.obj (P := Presheaf.IsSheaf K) ⟶
      (obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
        Presheaf.IsSheaf K))
    (CategoryStruct.comp (Y := obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)))
      (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) :
        obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) (F.obj (P := Presheaf.IsSheaf K)) ⟶
          obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (F.obj (P := Presheaf.IsSheaf K)))
      (CategoryStruct.comp (Y :=
        obj G.op.ran ((obj (G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J)))
        (map G.op.ran (NatTrans.app (Iso.inv (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K)) F) :
          obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)) ⟶
            obj G.op.ran ((obj (G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J)))
        (𝟙
            ((obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
              Presheaf.IsSheaf K)) :
          (obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
              Presheaf.IsSheaf K) ⟶
            (obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
              Presheaf.IsSheaf K))))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)))

Tactic:
erw [Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
inst_5 : G.IsContinuous J K
F : Sheaf.{v_2, w', u_2, w} K A
change :
  NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) ≫
      𝟙 (obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K))) ≫
        𝟙 (obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K))) =
    NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K))
⊢ NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) ≫
      𝟙 (obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K))) ≫
        𝟙
          ((obj (G.sheafPushforwardCocontinuous A J K) (obj (G.sheafPushforwardContinuous A J K) F)).obj (P :=
            Presheaf.IsSheaf K)) =
    NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K))

Tactic:
change _ ≫ 𝟙 _ ≫ 𝟙 _ = _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
inst_5 : G.IsContinuous J K
F : Sheaf.{v_2, w', u_2, w} K A
⊢ NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) ≫
      𝟙 (obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K))) ≫
        𝟙 (obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K))) =
    NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K))

Tactic:
simp only [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
inst_5 : G.IsContinuous J K
inst_6 : HasWeakSheafify.{v_1, w', u_1, w} J A
inst_7 : HasWeakSheafify.{v_2, w', u_2, w} K A
F : Functor.{v_2, w', u_2, w} Dᵒᵖ A
adj₁ : Adjunction (C := Functor.{v_2, w', u_2, w} Dᵒᵖ A) (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) G.op.ran :=
  G.op.ranAdjunction A
adj₂ : Adjunction (C := Functor.{v_1, w', u_1, w} Cᵒᵖ A) (presheafToSheaf J A) (sheafToPresheaf J A) :=
  sheafificationAdjunction J A
adj₃ : Adjunction (C := Functor.{v_2, w', u_2, w} Dᵒᵖ A) (presheafToSheaf K A) (sheafToPresheaf K A) :=
  sheafificationAdjunction K A
adj₄ : Adjunction (C := Sheaf.{v_2, w', u_2, w} K A) (G.sheafPushforwardContinuous A J K)
  (G.sheafPushforwardCocontinuous A J K) :=
  G.sheafAdjunctionCocontinuous A J K
change :
  Eq (α :=
    obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F) ⟶
      obj (sheafToPresheaf J A) (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F))
    (adj₂.unit.app (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F) ≫
        map (sheafToPresheaf J A) (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) :
      obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F) ⟶
        obj (sheafToPresheaf J A) (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F))
    (map (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (adj₃.unit.app F) :
      obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F) ⟶
        obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (obj (presheafToSheaf K A ⋙ sheafToPresheaf K A) F))
⊢ Eq (α := G.op ⋙ F ⟶ (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J))
    (CategoryStruct.comp (Y := sheafify J (G.op ⋙ F)) (toSheafify J (G.op ⋙ F))
      (InducedCategory.Hom.hom (NatTrans.app (Iso.hom (G.pushforwardContinuousSheafificationCompatibility A J K)) F)))
    (G.op.whiskerLeft (toSheafify K F))

Tactic:
change adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
    (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) =
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F)

Premises used: CategoryTheory.Functor.op, Opposite, CategoryTheory.Adjunction.leftAdjointUniq, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.Functor.whiskeringLeft, CategoryTheory.Iso.hom, CategoryTheory.Adjunction.comp, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.sheafToPresheaf