awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : e.functor.IsCocontinuous J K
inst_3 : e.inverse.IsCocontinuous K J
⊢ IsDenseSubsite K J e.inverse

Tactic:
have : e.symm.functor.IsCocontinuous K J := inferInstanceAs (e.inverse.IsCocontinuous _ _)
  have : e.symm.inverse.IsCocontinuous J K := inferInstanceAs (e.functor.IsCocontinuous _ _)
  isDenseSubsite_functor_of_isCocontinuous _ _ e.symm

Premises used: CategoryTheory.Equivalence.isDenseSubsite_functor_of_isCocontinuous, _private.0.CategoryTheory.Equivalence.isDenseSubsite_inverse_of_isCocontinuous._proof_1, _private.0.CategoryTheory.Equivalence.isDenseSubsite_inverse_of_isCocontinuous._proof_2, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : IsDenseSubsite K J e.inverse
rw : IsDenseSubsite J (e.inverse.inducedTopology J) e.functor
⊢ IsDenseSubsite J K e.functor

Tactic:
rw [e.eq_inducedTopology_of_isDenseSubsite J K]

Premises used: CategoryTheory.Equivalence.eq_inducedTopology_of_isDenseSubsite
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : IsDenseSubsite K J e.inverse
⊢ IsDenseSubsite J (e.inverse.inducedTopology J) e.functor

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : IsDenseSubsite K J e.inverse
X : Sheaf.{v₁, v₃, u₁, u₃} J A
h :
  ∀ (x : Dᵒᵖ),
    NatTrans.app
        (InducedCategory.Hom.hom
          (map (sheafCongr.functor J K e A) (NatTrans.app (Iso.hom (sheafCongr.unitIso J K e A)) X) ≫
            NatTrans.app (Iso.hom (sheafCongr.counitIso J K e A)) (obj (sheafCongr.functor J K e A) X)))
        x =
      (InducedCategory.Hom.hom (𝟙 (obj (sheafCongr.functor J K e A) X))).app x
⊢ map (sheafCongr.functor J K e A) (NatTrans.app (Iso.hom (sheafCongr.unitIso J K e A)) X) ≫
      NatTrans.app (Iso.hom (sheafCongr.counitIso J K e A)) (obj (sheafCongr.functor J K e A) X) =
    𝟙 (obj (sheafCongr.functor J K e A) X)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : IsDenseSubsite K J e.inverse
X : Sheaf.{v₁, v₃, u₁, u₃} J A
x : Dᵒᵖ
⊢ NatTrans.app
      (InducedCategory.Hom.hom
        (map (sheafCongr.functor J K e A) (NatTrans.app (Iso.hom (sheafCongr.unitIso J K e A)) X) ≫
          NatTrans.app (Iso.hom (sheafCongr.counitIso J K e A)) (obj (sheafCongr.functor J K e A) X)))
      x =
    (InducedCategory.Hom.hom (𝟙 (obj (sheafCongr.functor J K e A) X))).app x

Tactic:
simp [← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : IsDenseSubsite K J e.inverse
inst_4 : HasSheafify.{v₂, v₃, u₂, u₃} K A
⊢ HasSheafify.{v₁, v₃, u₁, u₃} J A

Tactic:
HasSheafify.mk' J A (transportSheafificationAdjunction J K e A)

Premises used: CategoryTheory.HasSheafify.mk', CategoryTheory.Equivalence.transportSheafificationAdjunction
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
A : Type u_1
inst_3 : Category.{v_1, u_1} A
B : Type u_2
inst_4 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_5 : K.HasSheafCompose F
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
change : Presheaf.IsSheaf K ((e.inverse.op ⋙ P) ⋙ F)
⊢ Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F)

Tactic:
change Presheaf.IsSheaf K ((_ ⋙ _) ⋙ _)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Presheaf.IsSheaf
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
A : Type u_1
inst_3 : Category.{v_1, u_1} A
B : Type u_2
inst_4 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_5 : K.HasSheafCompose F
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
hP₁ : Presheaf.IsSheaf K (e.inverse.op ⋙ P)
⊢ Presheaf.IsSheaf K ((e.inverse.op ⋙ P) ⋙ F)

Tactic:
apply HasSheafCompose.isSheaf

Premises used: CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
A : Type u_1
inst_3 : Category.{v_1, u_1} A
B : Type u_2
inst_4 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_5 : K.HasSheafCompose F
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf K (e.inverse.op ⋙ P)

Tactic:
e.inverse.op_comp_isSheaf K J ⟨P, hP⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Functor.op_comp_isSheaf, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
A : Type u_1
inst_3 : Category.{v_1, u_1} A
B : Type u_2
inst_4 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_5 : K.HasSheafCompose F
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf K (e.inverse.op ⋙ P)

Tactic:
exact e.inverse.op_comp_isSheaf K J ⟨P, hP⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Functor.op_comp_isSheaf, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
A : Type u_1
inst_3 : Category.{v_1, u_1} A
B : Type u_2
inst_4 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_5 : K.HasSheafCompose F
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F)

Tactic:
have hP' : Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F) := by
      change Presheaf.IsSheaf K ((_ ⋙ _) ⋙ _)
      apply HasSheafCompose.isSheaf
      exact e.inverse.op_comp_isSheaf K J ⟨P, hP⟩
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
A : Type u_1
inst_3 : Category.{v_1, u_1} A
B : Type u_2
inst_4 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_5 : K.HasSheafCompose F
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
hP' : Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F)
⊢ Presheaf.IsSheaf J (e.functor.op ⋙ e.inverse.op ⋙ P ⋙ F)

Tactic:
replace hP' : Presheaf.IsSheaf J (e.functor.op ⋙ e.inverse.op ⋙ P ⋙ F) :=
      e.functor.op_comp_isSheaf _ _ ⟨_, hP'⟩
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
A : Type u_1
inst_3 : Category.{v_1, u_1} A
B : Type u_2
inst_4 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_5 : K.HasSheafCompose F
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
hP' : Presheaf.IsSheaf J (e.functor.op ⋙ e.inverse.op ⋙ P ⋙ F)
⊢ Presheaf.IsSheaf J (P ⋙ F)

Tactic:
(Presheaf.isSheaf_of_iso_iff ((isoWhiskerRight e.op.unitIso.symm (P ⋙ F)))).mp hP'

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Presheaf.isSheaf_of_iso_iff, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Equivalence.op, CategoryTheory.Iso.symm, Iff.mp, CategoryTheory.Functor.isoWhiskerRight
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : IsDenseSubsite K J e.inverse
A : Type u_1
inst_3 : Category.{v_1, u_1} A
B : Type u_2
inst_4 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_5 : K.HasSheafCompose F
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
hP' : Presheaf.IsSheaf J (e.functor.op ⋙ e.inverse.op ⋙ P ⋙ F)
⊢ Presheaf.IsSheaf J (P ⋙ F)

Tactic:
exact (Presheaf.isSheaf_of_iso_iff ((isoWhiskerRight e.op.unitIso.symm (P ⋙ F)))).mp hP'

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Presheaf.isSheaf_of_iso_iff, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.op, CategoryTheory.Iso.symm, Iff.mp, CategoryTheory.Functor.isoWhiskerRight
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 :
  HasSheafify.{w, v₃, w, u₃} (C := SmallModel.{w, v₁, u₁} C)
    (inducedTopology (Equivalence.inverse (equivSmallModel C)) J) A
⊢ HasSheafify.{v₁, v₃, u₁, u₃} J A

Tactic:
(equivSmallModel C).hasSheafify J ((equivSmallModel C).inverse.inducedTopology J) A

Premises used: CategoryTheory.Functor.inducedTopology, CategoryTheory.Equivalence.hasSheafify, CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : EssentiallySmall.{w, v₁, u₁} C
inst_5 :
  HasSheafify.{w, v₃, w, u₃} (C := SmallModel.{w, v₁, u₁} C)
    (inducedTopology (Equivalence.inverse (equivSmallModel C)) J) A
inst_6 :
  HasSheafCompose.{w, v₃, v₄, w, u₃, u₄} (C := SmallModel.{w, v₁, u₁} C)
    (inducedTopology (Equivalence.inverse (equivSmallModel C)) J) F
⊢ J.HasSheafCompose F

Tactic:
(equivSmallModel C).hasSheafCompose J ((equivSmallModel C).inverse.inducedTopology J) F

Premises used: CategoryTheory.Functor.inducedTopology, CategoryTheory.Equivalence.hasSheafCompose, CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 :
  HasLimits
    (Sheaf.{w, v₃, w, u₃} (C := SmallModel.{w, v₁, u₁} C) (inducedTopology (Equivalence.inverse (equivSmallModel C)) J)
      A)
⊢ HasLimitsOfSize.{max v₃ w, max v₃ w, max u₁ v₃, max (max (max u₃ u₁) v₃) v₁} (Sheaf.{v₁, v₃, u₁, u₃} J A)

Tactic:
Adjunction.has_limits_of_equivalence ((equivSmallModel C).sheafCongr J
    ((equivSmallModel C).inverse.inducedTopology J) A).functor

Premises used: CategoryTheory.Functor.inducedTopology, CategoryTheory.Adjunction.has_limits_of_equivalence, CategoryTheory.Equivalence.functor, CategoryTheory.Equivalence.sheafCongr, CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : EssentiallySmall.{w, v₁, u₁} C
inst_5 :
  HasSheafify.{w, v₃, w, u₃} (C := SmallModel.{w, v₁, u₁} C)
    (inducedTopology (Equivalence.inverse (equivSmallModel C)) J) A
inst_6 :
  HasSheafCompose.{w, v₃, v₄, w, u₃, u₄} (C := SmallModel.{w, v₁, u₁} C)
    (inducedTopology (Equivalence.inverse (equivSmallModel C)) J) F
inst_7 :
  HasColimits
    (Sheaf.{w, v₃, w, u₃} (C := SmallModel.{w, v₁, u₁} C) (inducedTopology (Equivalence.inverse (equivSmallModel C)) J)
      A)
⊢ HasColimitsOfSize.{max v₃ w, max v₃ w, max u₁ v₃, max (max (max u₃ u₁) v₃) v₁} (Sheaf.{v₁, v₃, u₁, u₃} J A)

Tactic:
Adjunction.has_colimits_of_equivalence ((equivSmallModel C).sheafCongr J
    ((equivSmallModel C).inverse.inducedTopology J) A).functor

Premises used: CategoryTheory.Functor.inducedTopology, CategoryTheory.Equivalence.functor, CategoryTheory.Equivalence.sheafCongr, CategoryTheory.Adjunction.has_colimits_of_equivalence, CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
h :
  ∀ ⦃P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A⦄ (f : P ⟶ Q),
    MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f ↔ J.W f
⊢ Eq (α := MorphismProperty (Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A))
    (MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op)) J.W

Tactic:
ext P Q f
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
rw :
  Eq (α := MorphismProperty (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
    (ObjectProperty.isLocal
      (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x))
    (ObjectProperty.isLocal fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
        (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)
⊢ Eq (α := MorphismProperty (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) K.W
    (ObjectProperty.isLocal fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
        (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)

Tactic:
rw [W_eq_isLocal_range_sheafToPresheaf_obj, ← ObjectProperty.isoClosure_isLocal]

Premises used: CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj, CategoryTheory.ObjectProperty.isoClosure_isLocal
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
rw :
  ObjectProperty.isLocal
    (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
        (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)
| ObjectProperty.isLocal fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
    Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
      (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x

Tactic:
rw [← ObjectProperty.isoClosure_isLocal]

Premises used: CategoryTheory.ObjectProperty.isoClosure_isLocal
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
conv_rhs :
  Eq (α := MorphismProperty (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
    (ObjectProperty.isLocal
      (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x))
    (ObjectProperty.isLocal
      (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
          (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x))
⊢ Eq (α := MorphismProperty (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
    (ObjectProperty.isLocal
      (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x))
    (ObjectProperty.isLocal fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
        (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)

Tactic:
conv_rhs => rw [← ObjectProperty.isoClosure_isLocal]

Premises used: CategoryTheory.ObjectProperty.isoClosure_isLocal
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
h :
  Eq (α := ObjectProperty (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
    (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x)
    (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
        (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)
⊢ Eq (α := MorphismProperty (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
    (ObjectProperty.isLocal
      (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x))
    (ObjectProperty.isLocal
      (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
          (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
h :
  ∀ (P : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A),
    ObjectProperty.isoClosure
        (fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
          Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x)
        P ↔
      ObjectProperty.isoClosure
        (fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
          Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
            (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)
        P
⊢ Eq (α := ObjectProperty (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
    (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x)
    (ObjectProperty.isoClosure fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
        (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)

Tactic:
ext P
-- Module: Mathlib.CategoryTheory.Sites.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
A : Type u₃
inst_2 : Category.{v₃, u₃} A
inst_3 : G.IsCoverDense J
inst_4 : G.Full
inst_5 : G.IsContinuous K J
inst_6 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
P_1 Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P_1 ⟶ Q
P : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A
h :
  ObjectProperty.isoClosure
      (fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x)
      P →
    ObjectProperty.isoClosure
      (fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
          (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)
      P
h₁ :
  ObjectProperty.isoClosure
      (fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
          (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)
      P →
    ObjectProperty.isoClosure
      (fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x)
      P
⊢ ObjectProperty.isoClosure
      (fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A)) (Set.range (obj (sheafToPresheaf K A))) x)
      P ↔
    ObjectProperty.isoClosure
      (fun (x : Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A))
          (Set.range (obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))) x)
      P

Tactic:
constructor