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
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
⊢ MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f ↔ J.W f
have 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
Tactic: rw [h₁, J.W_eq_isLocal_range_sheafToPresheaf_obj, MorphismProperty.inverseImage_iff]
-- 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)
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
⊢ 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
have 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
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 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
⊢ 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
have 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)
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 Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
⊢ K.W (G.op.whiskerLeft f) ↔ J.W f
have rw : K.W (G.op.whiskerLeft f) ↔ MorphismProperty.inverseImage K.W (obj (whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op) f
Tactic: rw [← W_inverseImage_whiskeringLeft J K G]
-- 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
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : J.W f
⊢ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F) f
have hf₁ : K.W (G.op.whiskerLeft f)
Tactic: rw [← J.W_whiskerLeft_iff (G := G) (K := K)] at hf
Cleared hypotheses: hf
-- 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
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
⊢ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F) f
have this : K.W (whiskerRight (G.op.whiskerLeft f) F)
Tactic: have := K.W_of_preservesSheafification F (whiskerLeft G.op f) hf
-- 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
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this : K.W (whiskerRight (G.op.whiskerLeft f) F)
⊢ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F) f
have this₁ : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
Tactic: rw [whiskerRight_left] at this
Cleared hypotheses: this
-- 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
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
⊢ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F) f
have this₁ : K.W (G.op.whiskerLeft (whiskerRight f F))
Tactic: haveI := K.W.of_postcomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_inv _) <|
      K.W.of_precomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_hom _) this
-- 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
B : Type u₄
inst_3 : Category.{v₄, u₄} B
F : Functor.{v₃, v₄, u₃, u₄} A B
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : EssSurj (C := Sheaf.{v₁, v₄, u₁, u₄} J B) (G.sheafPushforwardContinuous B K J)
inst_8 : EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_9 : K.PreservesSheafification F
P Q : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this_1 : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
this : K.W (G.op.whiskerLeft (whiskerRight f F))
⊢ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F) f
have rwa : ∀ (this : J.W (whiskerRight f F)), MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ A B) F) f
Tactic: rwa [K.W_whiskerLeft_iff (G := G) (J := J) (f := whiskerRight f F)] at this
Cleared hypotheses: this
-- 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)
inst_7 : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst_8 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_9 : ConcreteCategory.{u_2, v₃, u₃, u_1} A FA (CC := CA)
inst_10 : WEqualsLocallyBijective.{u_2, v₃, v₂, u₃, u₂, u_1} K A (FA := FA) (CA := CA)
hG : CoverPreserving K J G
X Y : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : X ⟶ Y
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
have rw : K.W (G.op.whiskerLeft f) ↔
  Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
Tactic: rw [← W_whiskerLeft_iff J K G f, ← Presheaf.isLocallyInjective_whisker_iff K J G f hG,
      ← Presheaf.isLocallySurjective_whisker_iff K J G f hG, W_iff_isLocallyBijective]
-- 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)
inst_7 : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst_8 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_9 : ConcreteCategory.{u_2, v₃, u₃, u_1} A FA (CC := CA)
inst_10 : WEqualsLocallyBijective.{u_2, v₃, v₂, u₃, u₂, u_1} K A (FA := FA) (CA := CA)
hG : CoverPreserving K J G
X Y : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : X ⟶ Y
rw :
  K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
have rw₁ : K.W (G.op.whiskerLeft f) ↔
  Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
    Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
Tactic: rw [← W_whiskerLeft_iff J K G f, ← Presheaf.isLocallyInjective_whisker_iff K J G f hG,
      ← Presheaf.isLocallySurjective_whisker_iff K J G f hG, W_iff_isLocallyBijective]
-- 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)
inst_7 : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst_8 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_9 : ConcreteCategory.{u_2, v₃, u₃, u_1} A FA (CC := CA)
inst_10 : WEqualsLocallyBijective.{u_2, v₃, v₂, u₃, u₂, u_1} K A (FA := FA) (CA := CA)
hG : CoverPreserving K J G
X Y : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : X ⟶ Y
rw :
  K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₁ :
  K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
      Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
have rw₂ : K.W (G.op.whiskerLeft f) ↔
  Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
    Presheaf.IsLocallySurjective K (FA := FA) (CA := CA) (G.op.whiskerLeft f)
Tactic: rw [← W_whiskerLeft_iff J K G f, ← Presheaf.isLocallyInjective_whisker_iff K J G f hG,
      ← Presheaf.isLocallySurjective_whisker_iff K J G f hG, W_iff_isLocallyBijective]
-- 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)
inst_7 : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst_8 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_9 : ConcreteCategory.{u_2, v₃, u₃, u_1} A FA (CC := CA)
inst_10 : WEqualsLocallyBijective.{u_2, v₃, v₂, u₃, u₂, u_1} K A (FA := FA) (CA := CA)
hG : CoverPreserving K J G
X Y : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : X ⟶ Y
rw :
  K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₁ :
  K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
      Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₂ :
  K.W (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
      Presheaf.IsLocallySurjective K (FA := FA) (CA := CA) (G.op.whiskerLeft f)
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
have rw₃ : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
    Presheaf.IsLocallySurjective K (FA := FA) (CA := CA) (G.op.whiskerLeft f) ↔
  Presheaf.IsLocallyInjective (FD := FA) (CD := CA) K (G.op.whiskerLeft f) ∧
    Presheaf.IsLocallySurjective K (FA := FA) (CA := CA) (G.op.whiskerLeft f)
Tactic: rw [← W_whiskerLeft_iff J K G f, ← Presheaf.isLocallyInjective_whisker_iff K J G f hG,
      ← Presheaf.isLocallySurjective_whisker_iff K J G f hG, W_iff_isLocallyBijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.GlobalSections (goal)
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
j : Cᵒᵖ
⊢ (ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj c.pt ⟶ F.obj) → c.pt ⟶ (Γ J A).obj F) c.π ≫ F.coneΓ.π.app j = c.π.app j
have suffices : Functor.map (Functor.const Cᵒᵖ) ((ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj c.pt ⟶ F.obj) → c.pt ⟶ (Γ J A).obj F) c.π) ≫
    F.coneΓ.π =
  c.π
Tactic: suffices h : ((Functor.const Cᵒᵖ).map (ΓHomEquiv c.π)) ≫ F.coneΓ.π = c.π from congr_app h j
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.GlobalSections (goal)
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
⊢ Functor.map (Functor.const Cᵒᵖ) f ≫ F.coneΓ.π = c.π
have w : ∀ (j : Cᵒᵖ), (Functor.map (Functor.const Cᵒᵖ) f ≫ F.coneΓ.π).app j = c.π.app j
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.GlobalSections (hypothesis)
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
c : Cone (F.obj (P := Presheaf.IsSheaf J))
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
⊢ f = (ΓHomEquiv : (a : (Functor.const Cᵒᵖ).obj c.pt ⟶ F.obj) → c.pt ⟶ (Γ J A).obj F) c.π
have hf₁ : Functor.map (Functor.const Cᵒᵖ) f ≫ F.coneΓ.π = c.π
Tactic: replace hf : ((Functor.const Cᵒᵖ).map f) ≫ F.coneΓ.π = c.π := by ext j; exact hf j
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.GlobalSections (goal)
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 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F G : Sheaf.{v, v₂, u, u₂} J A
f : F ⟶ G
U : Cᵒᵖ
⊢ Eq (α := Functor.obj (Γ J A) F ⟶ G.obj (P := Presheaf.IsSheaf J).obj U) (Functor.map (Γ J A) f ≫ G.ΓRes U)
    (F.ΓRes U ≫ f.hom.app U)
have refine : Eq (α := Functor.obj (Γ J A) F ⟶ G.obj (P := Presheaf.IsSheaf J).obj U) (Functor.map (Γ J A) f ≫ G.ΓRes U)
  (NatTrans.app
    ((Equiv.symm ΓHomEquiv : (a : (Γ J A).1 F ⟶ (Γ J A).obj G) → (Functor.const Cᵒᵖ).obj ((Γ J A).1 F) ⟶ G.obj)
      (𝟙 (Functor.obj (Γ J A) F) ≫ Functor.map (Γ J A) f))
    U)
Tactic: refine .trans ?_ <| congr_app (ΓHomEquiv_naturality_right_symm _ _) U