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
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
R : Sheaf.{v₂, v₃, u₂, u₃} K A
e : P ≅ obj (sheafToPresheaf K A) R
⊢ 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:
⟨_, ⟨_, rfl⟩, ⟨e.trans ((sheafToPresheaf _ _).mapIso
        ((G.sheafPushforwardContinuous A K J).objObjPreimageIso R).symm)⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.trans, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Functor.sheafPushforwardContinuous, CategoryTheory.Functor.mapIso, rfl, CategoryTheory.sheafToPresheaf
-- 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
R : Sheaf.{v₂, v₃, u₂, u₃} K A
e : P ≅ obj (sheafToPresheaf K A) R
⊢ 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:
exact ⟨_, ⟨_, rfl⟩, ⟨e.trans ((sheafToPresheaf _ _).mapIso
        ((G.sheafPushforwardContinuous A K J).objObjPreimageIso R).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
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
R : Sheaf.{v₁, v₃, u₁, u₃} J A
e : P ≅ obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) R
⊢ 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

Tactic:
⟨G.op ⋙ R.obj, ⟨(G.sheafPushforwardContinuous A K J).obj R, rfl⟩, ⟨e⟩⟩

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.FullSubcategory.obj, Nonempty.intro, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Functor.sheafPushforwardContinuous, CategoryTheory.Functor.obj, rfl
-- 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
R : Sheaf.{v₁, v₃, u₁, u₃} J A
e : P ≅ obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) R
⊢ 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

Tactic:
exact ⟨G.op ⋙ R.obj, ⟨(G.sheafPushforwardContinuous A K J).obj R, rfl⟩, ⟨e⟩⟩
-- 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
⊢ 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:
have h₁ : K.W (A := A) =
    ObjectProperty.isLocal (· ∈ Set.range (sheafToPresheaf J A ⋙
      ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op)).obj) := by
    rw [W_eq_isLocal_range_sheafToPresheaf_obj, ← ObjectProperty.isoClosure_isLocal]
    conv_rhs => rw [← ObjectProperty.isoClosure_isLocal]
    apply congr_arg
    ext P
    constructor
    · rintro ⟨_, ⟨R, rfl⟩, ⟨e⟩⟩
      exact ⟨_, ⟨_, rfl⟩, ⟨e.trans ((sheafToPresheaf _ _).mapIso
        ((G.sheafPushforwardContinuous A K J).objObjPreimageIso R).symm)⟩⟩
    · rintro ⟨_, ⟨R, rfl⟩, ⟨e⟩⟩
      exact ⟨G.op ⋙ R.obj, ⟨(G.sheafPushforwardContinuous A K J).obj R, rfl⟩, ⟨e⟩⟩
-- 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 (α := 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)
R : Sheaf.{v₁, v₃, u₁, u₃} J A
rw :
  Function.Bijective (α := Q ⟶ R.obj (P := Presheaf.IsSheaf J)) (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
      ((fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ∘
        map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op)) ↔
    Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦ f ≫ g
⊢ (Function.Bijective (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
      fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ↔
    Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦ f ≫ g

Tactic:
rw [← Function.Bijective.of_comp_iff _
      (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G Q R.obj R.property)]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.whiskerLeft_obj_map_bijective_of_isCoverDense, CategoryTheory.ObjectProperty.FullSubcategory.obj, Function.Bijective.of_comp_iff
-- 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 (α := 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)
R : Sheaf.{v₁, v₃, u₁, u₃} J A
⊢ Function.Bijective (α := Q ⟶ R.obj (P := Presheaf.IsSheaf J)) (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
      ((fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ∘
        map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op)) ↔
    Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦ f ≫ g

Tactic:
Function.Bijective.of_comp_iff'
      (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G P R.obj R.property)
        (fun g ↦ f ≫ g)

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.whiskerLeft_obj_map_bijective_of_isCoverDense, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.ObjectProperty.FullSubcategory.obj, Function.Bijective.of_comp_iff', CategoryTheory.CategoryStruct.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
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 (α := 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)
R : Sheaf.{v₁, v₃, u₁, u₃} J A
⊢ Function.Bijective (α := Q ⟶ R.obj (P := Presheaf.IsSheaf J)) (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
      ((fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ∘
        map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op)) ↔
    Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦ f ≫ g

Tactic:
exact Function.Bijective.of_comp_iff'
      (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G P R.obj R.property)
        (fun g ↦ f ≫ g)

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.whiskerLeft_obj_map_bijective_of_isCoverDense, CategoryTheory.ObjectProperty.FullSubcategory.obj, Function.Bijective.of_comp_iff', CategoryTheory.CategoryStruct.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
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 (α := 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)
⊢ ∀ (R : Sheaf.{v₁, v₃, u₁, u₃} J A),
    (Function.Bijective (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
        fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ↔
      Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦
        f ≫ g

Tactic:
have h₂ : ∀ (R : Sheaf J A),
    Function.Bijective (fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj) ↦ whiskerLeft G.op f ≫ g) ↔
      Function.Bijective (fun (g : Q ⟶ R.obj) ↦ f ≫ g) := fun R ↦ by
    rw [← Function.Bijective.of_comp_iff _
      (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G Q R.obj R.property)]
    exact Function.Bijective.of_comp_iff'
      (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G P R.obj R.property)
        (fun g ↦ f ≫ g)
-- 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 (α := 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)
h₂ :
  ∀ (R : Sheaf.{v₁, v₃, u₁, u₃} J A),
    (Function.Bijective (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
        fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ↔
      Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦
        f ≫ g
h :
  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
      (X := obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) P) (map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f) ↔
    ObjectProperty.isLocal
      (fun (x : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A)) (Set.range (obj (sheafToPresheaf J A))) x)
      f
⊢ MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f ↔ J.W f

Tactic:
rw [h₁, J.W_eq_isLocal_range_sheafToPresheaf_obj, MorphismProperty.inverseImage_iff]

Premises used: CategoryTheory.MorphismProperty.inverseImage_iff, CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj
-- 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 (α := 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)
h₂ :
  ∀ (R : Sheaf.{v₁, v₃, u₁, u₃} J A),
    (Function.Bijective (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
        fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ↔
      Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦
        f ≫ g
h :
  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
      (X := obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) P) (map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f) →
    ObjectProperty.isLocal
      (fun (x : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A)) (Set.range (obj (sheafToPresheaf J A))) x)
      f
h₃ :
  ObjectProperty.isLocal
      (fun (x : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A)) (Set.range (obj (sheafToPresheaf J A))) x)
      f →
    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
      (X := obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) P) (map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f)
⊢ 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
      (X := obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) P) (map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f) ↔
    ObjectProperty.isLocal
      (fun (x : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A) ↦
        Membership.mem (γ := Set (Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A)) (Set.range (obj (sheafToPresheaf J A))) x)
      f

Tactic:
constructor
-- 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 (α := 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)
h₂ :
  ∀ (R : Sheaf.{v₁, v₃, u₁, u₃} J A),
    (Function.Bijective (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
        fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ↔
      Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦
        f ≫ g
h :
  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
    (X := obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) P) (map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f)
R : Sheaf.{v₁, v₃, u₁, u₃} J A
⊢ Function.Bijective (β := P ⟶ obj (sheafToPresheaf J A) R) fun (g : Q ⟶ obj (sheafToPresheaf J A) R) ↦ f ≫ g

Tactic:
(h₂ R).1 (h _ ⟨R, rfl⟩)

Premises used: Exists.intro, Iff.mp, rfl
-- 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 (α := 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)
h₂ :
  ∀ (R : Sheaf.{v₁, v₃, u₁, u₃} J A),
    (Function.Bijective (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
        fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ↔
      Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦
        f ≫ g
h :
  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
    (X := obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) P) (map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f)
R : Sheaf.{v₁, v₃, u₁, u₃} J A
⊢ Function.Bijective (β := P ⟶ obj (sheafToPresheaf J A) R) fun (g : Q ⟶ obj (sheafToPresheaf J A) R) ↦ f ≫ g

Tactic:
exact (h₂ R).1 (h _ ⟨R, rfl⟩)

Premises used: Exists.intro, Iff.mp, rfl
-- 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 (α := 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)
h₂ :
  ∀ (R : Sheaf.{v₁, v₃, u₁, u₃} J A),
    (Function.Bijective (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
        fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ↔
      Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦
        f ≫ g
h :
  ObjectProperty.isLocal
    (fun (x : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A)) (Set.range (obj (sheafToPresheaf J A))) x)
    f
R : Sheaf.{v₁, v₃, u₁, u₃} J A
⊢ Function.Bijective (β :=
    obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) P ⟶ obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) R)
    fun
      (g :
        obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) Q ⟶
          obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) R) ↦
    map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f ≫ g

Tactic:
(h₂ R).2 (h _ ⟨R, rfl⟩)

Premises used: Iff.mpr, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, Exists.intro, rfl
-- 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 (α := 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)
h₂ :
  ∀ (R : Sheaf.{v₁, v₃, u₁, u₃} J A),
    (Function.Bijective (β := G.op ⋙ P ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J))
        fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.obj (P := Presheaf.IsSheaf J)) ↦ G.op.whiskerLeft f ≫ g) ↔
      Function.Bijective (β := P ⟶ R.obj (P := Presheaf.IsSheaf J)) fun (g : Q ⟶ R.obj (P := Presheaf.IsSheaf J)) ↦
        f ≫ g
h :
  ObjectProperty.isLocal
    (fun (x : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A) ↦
      Membership.mem (γ := Set (Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A)) (Set.range (obj (sheafToPresheaf J A))) x)
    f
R : Sheaf.{v₁, v₃, u₁, u₃} J A
⊢ Function.Bijective (β :=
    obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) P ⟶ obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) R)
    fun
      (g :
        obj (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) Q ⟶
          obj (sheafToPresheaf J A ⋙ obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) R) ↦
    map (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f ≫ g

Tactic:
exact (h₂ R).2 (h _ ⟨R, rfl⟩)

Premises used: Iff.mpr, Exists.intro, rfl