awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
X : C
S : Sieve.{v₁, u₁} X
mp :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
      (Sieve.functorPushforward e.functor S) →
    S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
      (Sieve.functorPushforward e.functor S) ↔
    S ∈ (J : (a : C) → Set (Sieve a)) X
have mpr : S ∈ (J : (a : C) → Set (Sieve a)) X →
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
    (Sieve.functorPushforward e.functor S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
X : C
S : Sieve.{v₁, u₁} X
H :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
    (Sieve.functorPushforward e.functor S)
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X
have mp : Sieve.functorPullback e.functor (Sieve.functorPushforward e.functor S) ≤ S
Tactic: refine J.superset_covering ?_ (e.functor.cover_lift J K H)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
X : C
S : Sieve.{v₁, u₁} X
H :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
    (Sieve.functorPushforward e.functor S)
⊢ Sieve.functorPullback e.functor (Sieve.functorPushforward e.functor S) ≤ S
have mp : S ≤ S
Tactic: rw [(Sieve.fullyFaithfulFunctorGaloisCoinsertion e.functor X).u_l_eq S]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
X : C
S : Sieve.{v₁, u₁} X
H : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Membership.mem (γ := Set (Sieve.{v₂, u₂} (e.functor.obj X))) ((K : (a : D) → Set (Sieve a)) (e.functor.obj X))
    (Sieve.functorPushforward e.functor S)
have mpr : Sieve.functorPullback e.inverse (Sieve.pullback (e.unitInv.app X) S) ≤ Sieve.functorPushforward e.functor S
Tactic: refine K.superset_covering ?_
        (e.inverse.cover_lift K J (J.pullback_stable (e.unitInv.app X) H))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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 K e.functor
have rw : IsDenseSubsite J (e.inverse.inducedTopology J) e.functor
Tactic: rw [e.eq_inducedTopology_of_isDenseSubsite J K]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ 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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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)
have change : Presheaf.IsSheaf K ((e.inverse.op ⋙ P) ⋙ F)
Tactic: change Presheaf.IsSheaf K ((_ ⋙ _) ⋙ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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)
have hP₁ : Presheaf.IsSheaf K (e.inverse.op ⋙ P)
Tactic: apply HasSheafCompose.isSheaf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (hypothesis)
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 J (P ⋙ F)
have hP' : 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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (hypothesis)
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 (P ⋙ F)
have hP'₁ : 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'⟩
Cleared hypotheses: hP'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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)
⊢ Eq (α := MorphismProperty (Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A))
    (MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op)) J.W
have 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
Tactic: ext P Q f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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)
have 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)
Tactic: rw [W_eq_isLocal_range_sheafToPresheaf_obj, ← ObjectProperty.isoClosure_isLocal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
| 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
have 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)
Tactic: rw [← ObjectProperty.isoClosure_isLocal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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))
    (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)
have 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))
Tactic: conv_rhs => rw [← ObjectProperty.isoClosure_isLocal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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))
    (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))
have 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)
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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 (α := 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)
have 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
Tactic: ext P
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (hypothesis)
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
⊢ MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f ↔ J.W f
have 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)
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⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (goal)
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
have 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
Tactic: rw [← Function.Bijective.of_comp_iff _
      (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G Q R.obj R.property)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Equivalence (hypothesis)
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)
⊢ MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f ↔ J.W f
have 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
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)