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
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
⊢ (adj₁.comp adj₂).unit.app F ≫
      map (sheafToPresheaf J A ⋙ G.op.ran) (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) =
    (adj₃.comp adj₄).unit.app F

Tactic:
have eq := (adj₁.comp adj₂).unit_leftAdjointUniq_hom_app (adj₃.comp adj₄) F
-- 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
eq :
  (adj₁.comp adj₂).unit.app F ≫
      map (sheafToPresheaf J A ⋙ G.op.ran) (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) =
    (adj₃.comp adj₄).unit.app F
⊢ Eq (α :=
    obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F ⟶
      obj (sheafToPresheaf J A ⋙ G.op.ran) (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F))
    (adj₁.unit.app F ≫
      CategoryStruct.comp (Y :=
        obj ((obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ presheafToSheaf J A) ⋙ sheafToPresheaf J A ⋙ G.op.ran) F)
        (map G.op.ran (adj₂.unit.app (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F)))
        (map G.op.ran (map (sheafToPresheaf J A) (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F))))
    (adj₃.unit.app F ≫ map (sheafToPresheaf K A) (adj₄.unit.app (obj (presheafToSheaf K A) F)))

Tactic:
rw [Adjunction.comp_unit_app, Adjunction.comp_unit_app, comp_map,
    Category.assoc] at eq

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.comp_unit_app
-- 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
eq :
  Eq (α :=
    obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F ⟶
      obj (sheafToPresheaf J A ⋙ G.op.ran) (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F))
    (adj₁.unit.app F ≫
      CategoryStruct.comp (Y :=
        obj ((obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ presheafToSheaf J A) ⋙ sheafToPresheaf J A ⋙ G.op.ran) F)
        (map G.op.ran (adj₂.unit.app (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F)))
        (map G.op.ran (map (sheafToPresheaf J A) (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F))))
    (adj₃.unit.app F ≫ map (sheafToPresheaf K A) (adj₄.unit.app (obj (presheafToSheaf K A) F)))
⊢ Eq (α :=
    obj (presheafToSheaf K A ⋙ sheafToPresheaf K A) F ⟶
      obj G.op.ran (obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F))))
    (map (sheafToPresheaf K A) (adj₄.unit.app (obj (presheafToSheaf K A) F)) :
      obj (sheafToPresheaf K A) (obj (presheafToSheaf K A) F) ⟶
        obj (sheafToPresheaf K A)
          (obj (G.sheafPushforwardContinuous A J K ⋙ G.sheafPushforwardCocontinuous A J K)
            (obj (presheafToSheaf K A) F)))
    (adj₁.unit.app (obj (presheafToSheaf K A ⋙ sheafToPresheaf K A) F))

Tactic:
G.sheafAdjunctionCocontinuous_unit_app_hom A J K ((presheafToSheaf K A).obj F)

Premises used: CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom, CategoryTheory.presheafToSheaf, CategoryTheory.Functor.rightKanExtension, CategoryTheory.Functor.obj
-- 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
eq :
  Eq (α :=
    obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F ⟶
      obj (sheafToPresheaf J A ⋙ G.op.ran) (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F))
    (adj₁.unit.app F ≫
      CategoryStruct.comp (Y :=
        obj ((obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ presheafToSheaf J A) ⋙ sheafToPresheaf J A ⋙ G.op.ran) F)
        (map G.op.ran (adj₂.unit.app (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F)))
        (map G.op.ran (map (sheafToPresheaf J A) (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F))))
    (adj₃.unit.app F ≫ map (sheafToPresheaf K A) (adj₄.unit.app (obj (presheafToSheaf K A) F)))
⊢ Eq (α :=
    obj (presheafToSheaf K A ⋙ sheafToPresheaf K A) F ⟶
      obj G.op.ran (obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F))))
    (map (sheafToPresheaf K A) (adj₄.unit.app (obj (presheafToSheaf K A) F)) :
      obj (sheafToPresheaf K A) (obj (presheafToSheaf K A) F) ⟶
        obj (sheafToPresheaf K A)
          (obj (G.sheafPushforwardContinuous A J K ⋙ G.sheafPushforwardCocontinuous A J K)
            (obj (presheafToSheaf K A) F)))
    (adj₁.unit.app (obj (presheafToSheaf K A ⋙ sheafToPresheaf K A) F))

Tactic:
exact G.sheafAdjunctionCocontinuous_unit_app_hom A J K ((presheafToSheaf K A).obj F)

Premises used: CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom, CategoryTheory.presheafToSheaf, CategoryTheory.Functor.obj
-- 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
a :
  Eq (α :=
    obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F ⟶
      (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J))
    (CategoryStruct.comp (Y := sheafify J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F))
      (toSheafify J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F))
      (InducedCategory.Hom.hom (NatTrans.app (Iso.hom (G.pushforwardContinuousSheafificationCompatibility A J K)) F)))
    (G.op.whiskerLeft (toSheafify K F))
⊢ Eq (α :=
    (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ presheafToSheaf J A) F).obj (P := Presheaf.IsSheaf J) ⟶
      (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (NatTrans.app (Iso.hom (G.pushforwardContinuousSheafificationCompatibility A J K)) F))
    (sheafifyLift J (G.op.whiskerLeft (toSheafify K F)) ⋯)

Tactic:
apply sheafifyLift_unique

Premises used: CategoryTheory.sheafifyLift_unique
-- 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
⊢ Eq (α :=
    obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F ⟶
      (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J))
    (CategoryStruct.comp (Y := sheafify J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F))
      (toSheafify J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F))
      (InducedCategory.Hom.hom (NatTrans.app (Iso.hom (G.pushforwardContinuousSheafificationCompatibility A J K)) F)))
    (G.op.whiskerLeft (toSheafify K F))

Tactic:
apply toSheafify_pullbackSheafificationCompatibility

Premises used: CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
U : C
S : Sieve.{v₁, u₁} U
hS : S ∈ (J : (a : C) → Set (Sieve a)) U
⊢ Membership.mem (γ := Set (Sieve.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) U)))
    ((J : (a : C) → Set (Sieve a)) (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) U)) (Sieve.functorPushforward (𝟭 C) S)

Tactic:
simpa using hS
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} A
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : CoverPreserving J K F
G : Functor.{v₂, v₃, u₂, u₃} D A
hG : CoverPreserving K L G
U : C
S : Sieve.{v₁, u₁} U
hS : S ∈ (J : (a : C) → Set (Sieve a)) U
rw :
  Membership.mem (γ := Set (Sieve.{v₃, u₃} ((F ⋙ G).obj U))) ((L : (a : A) → Set (Sieve a)) ((F ⋙ G).obj U))
    (Sieve.functorPushforward G (Sieve.functorPushforward F S))
⊢ Membership.mem (γ := Set (Sieve.{v₃, u₃} ((F ⋙ G).obj U))) ((L : (a : A) → Set (Sieve a)) ((F ⋙ G).obj U))
    (Sieve.functorPushforward (F ⋙ G) S)

Tactic:
rw [Sieve.functorPushforward_comp]

Premises used: CategoryTheory.Sieve.functorPushforward_comp
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} A
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : CoverPreserving J K F
G : Functor.{v₂, v₃, u₂, u₃} D A
hG : CoverPreserving K L G
U : C
S : Sieve.{v₁, u₁} U
hS : S ∈ (J : (a : C) → Set (Sieve a)) U
⊢ Membership.mem (γ := Set (Sieve.{v₃, u₃} ((F ⋙ G).obj U))) ((L : (a : A) → Set (Sieve a)) ((F ⋙ G).obj U))
    (Sieve.functorPushforward G (Sieve.functorPushforward F S))

Tactic:
hG.cover_preserve (hF.cover_preserve hS)

Premises used: Set.Mem, CategoryTheory.CoverPreserving.cover_preserve
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} A
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : CoverPreserving J K F
G : Functor.{v₂, v₃, u₂, u₃} D A
hG : CoverPreserving K L G
U : C
S : Sieve.{v₁, u₁} U
hS : S ∈ (J : (a : C) → Set (Sieve a)) U
⊢ Membership.mem (γ := Set (Sieve.{v₃, u₃} ((F ⋙ G).obj U))) ((L : (a : A) → Set (Sieve a)) ((F ⋙ G).obj U))
    (Sieve.functorPushforward G (Sieve.functorPushforward F S))

Tactic:
exact hG.cover_preserve (hF.cover_preserve hS)

Premises used: CategoryTheory.CoverPreserving.cover_preserve
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
h : x.Compatible (R := T)
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
apply : (g₁ ≫ h₁) ≫ G.map f₁ = (g₂ ≫ h₂) ≫ G.map f₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (g₁ ≫ h₁).op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj X₁)))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op W)))
        (x f₁ hf₁) :
      (fun (X : Type w) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (g₂ ≫ h₂).op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj X₂)))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op W)))
        (x f₂ hf₂) :
      (fun (X : Type w) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op W)))

Tactic:
apply hG.compatible ℱ h _ _ hf₁ hf₂

Premises used: CategoryTheory.CompatiblePreserving.compatible
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
h : x.Compatible (R := T)
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
⊢ (g₁ ≫ h₁) ≫ G.map f₁ = (g₂ ≫ h₂) ≫ G.map f₂

Tactic:
simpa using eq
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
h : x.Compatible (R := T)
Y : C
f : Y ⟶ Z
hf : T f
rcases :
  ∀ (X : C) (g : X ⟶ Z) (f' : G.obj Y ⟶ G.obj X) (hg : T g) (eq : G.map f = f' ≫ G.map g),
    (FunctorPushforwardStructure.casesOn (S := T) (motive := fun (x : FunctorPushforwardStructure G T (G.map f)) ↦
        ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))) (FunctorPushforwardStructure.mk (S := T) X g f' hg eq)
        fun (Z_1 : C) (g : Z_1 ⟶ Z) (h : G.obj Y ⟶ G.obj Z_1) (h₁ : T g) (fac : G.map f = h ≫ G.map g) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map h.op) :
            (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj Z_1)))) →
              (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          (x g h₁)) =
      x f hf
⊢ (FunctorPushforwardStructure.casesOn (S := T) (motive := fun (x : FunctorPushforwardStructure G T (G.map f)) ↦
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))) (getFunctorPushforwardStructure (S := T) ⋯)
      fun (Z_1 : C) (g : Z_1 ⟶ Z) (h : G.obj Y ⟶ G.obj Z_1) (h₁ : T g) (fac : G.map f = h ≫ G.map g) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map h.op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj Z_1)))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
        (x g h₁)) =
    x f hf

Tactic:
rcases getFunctorPushforwardStructure (image_mem_functorPushforward G T hf) with
    ⟨X, g, f', hg, eq⟩

Premises used: CategoryTheory.Presieve.image_mem_functorPushforward, CategoryTheory.Presieve.getFunctorPushforwardStructure
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
h : x.Compatible (R := T)
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
⊢ f' ≫ G.map g = 𝟙 (G.obj Y) ≫ G.map f

Tactic:
simp [eq]
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
h : x.Compatible (R := T)
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
⊢ (FunctorPushforwardStructure.casesOn (S := T) (motive := fun (x : FunctorPushforwardStructure G T (G.map f)) ↦
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))) (FunctorPushforwardStructure.mk (S := T) X g f' hg eq)
      fun (Z_1 : C) (g : Z_1 ⟶ Z) (h : G.obj Y ⟶ G.obj Z_1) (h₁ : T g) (fac : G.map f = h ≫ G.map g) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map h.op) :
          (a : (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj Z_1)))) → (fun (X : Type w) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
        (x g h₁)) =
    x f hf

Tactic:
simpa using hG.compatible ℱ h f' (𝟙 _) hg hf (by simp [eq])

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CompatiblePreserving.compatible
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
compatible :
  ∀ (ℱ : Sheaf K (Type u_1)) {Z : C} {T : Presieve.{v₁, u₁} Z}
    {x : FamilyOfElements (F.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T},
    x.Compatible (R := T) →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ F.obj Y₁) (f₂ : X ⟶ F.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂),
        f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂ →
          Eq (α := (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
                  (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₁)))) →
                    (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
                (x g₁ hg₁) :
              (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
                  (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₂)))) →
                    (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
                (x g₂ hg₂) :
              (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
⊢ CompatiblePreserving K F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (F.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
compatible :
  ∀ (X' : C) (e : F.obj X' ≅ X),
    Eq (α := (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
            (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₁)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
          (x g₁ hg₁) :
        (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
            (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₂)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
          (x g₂ hg₂) :
        (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
          (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₁)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
        (x g₁ hg₁) :
      (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
          (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₂)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
        (x g₂ hg₂) :
      (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))

Tactic:
obtain ⟨X', e⟩ := hF f₁