awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
X : Cᵒᵖ
x : F.obj X
property : x ∈ G.obj X
⊢ ∀ ⦃a₂ : G.toFunctor.obj X⦄,
    Eq (α := F.obj X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
            (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property) :
          F.obj X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X) a₂ : F.obj X) →
      Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property = a₂
have this : ∀ (y : F.obj X) (property_1 : y ∈ G.obj X),
  Eq (α := F.obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
          (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property) :
        F.obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.ι.app X) : (a : G.toFunctor.obj X) → F.obj X)
          (Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) y property_1) :
        F.obj X) →
    Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) x property =
      Subtype.mk (p := fun (x : F.obj X) ↦ x ∈ G.obj X) y property_1
Tactic: ⟨y, _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (FC := TypeCat.Fun) (P.obj X)
h :
  Eq (α := (J.plusObj P).obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (J.toPlus P) X) : (a : P.obj X) → (J.plusObj P).obj X) x :
      (J.plusObj P).obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (J.toPlus P) X) : (a : P.obj X) → (J.plusObj P).obj X) y :
      (J.plusObj P).obj X)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := TypeCat.Fun) x y)
have h₁ : ∃ (W : J.Cover (unop X)) (h1 : W ⟶ ⊤) (h2 : W ⟶ ⊤),
  Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ x) h1 =
    Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ y) h2
Tactic: rw [toPlus_eq_mk, toPlus_eq_mk, eq_mk_iff_exists] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (FC := TypeCat.Fun) (P.obj X)
h :
  ∃ (W : J.Cover (unop X)) (h1 : W ⟶ ⊤) (h2 : W ⟶ ⊤),
    Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ x) h1 =
      Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ y) h2
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := TypeCat.Fun) x y)
have obtain : ∀ (W : J.Cover (unop X)) (h₁ h₂ : W ⟶ ⊤)
  (eq :
    Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ x) h₁ =
      Meq.refine (FD := TypeCat.Fun) (Meq.mk (FD := TypeCat.Fun) ⊤ y) h₂),
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := TypeCat.Fun) x y)
Tactic: obtain ⟨W, h₁, h₂, eq⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
⊢ IsLocallyInjective (FD := TypeCat.Fun) J (F₂ := J.sheafify P) (J.toPlus P ≫ J.plusMap (J.toPlus P))
have rw : IsLocallyInjective (FD := TypeCat.Fun) J (F₂ := J.sheafify P) (J.toPlus P ≫ J.toPlus (J.plusObj P))
Tactic: rw [GrothendieckTopology.plusMap_toPlus]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD_1 : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD_1 X) (CD_1 Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD_1)
J : GrothendieckTopology.{v, u} C
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
CD : D → Type (max u v)
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
P : Functor.{v, v', u, u'} Cᵒᵖ D
inst_6 : HasWeakSheafify.{v, v', u, u'} J D
inst_7 : J.HasSheafCompose (forget D (FC := FD) (CC := CD))
inst_8 : J.PreservesSheafification (forget D (FC := FD) (CC := CD))
⊢ IsLocallyInjective (FD := FD) (CD := CD) J (F₂ := sheafify J P) (toSheafify J P)
have rw : IsLocallyInjective (FD := TypeCat.Fun) J (F₂ := sheafify J P ⋙ forget D (FC := FD) (CC := CD))
  (CategoryStruct.comp (Y := sheafify J (P ⋙ forget D (FC := FD) (CC := CD)))
    (CategoryStruct.comp (Y := J.sheafify (P ⋙ forget D (FC := FD) (CC := CD)))
        (J.toSheafify (P ⋙ forget D (FC := FD) (CC := CD)))
        (Iso.hom (plusPlusIsoSheafify J (Type (max u v)) (FD := TypeCat.Fun) (P ⋙ forget D (FC := FD) (CC := CD)))) :
      P ⋙ forget D (FC := FD) (CC := CD) ⟶ sheafify J (P ⋙ forget D (FC := FD) (CC := CD)))
    (Iso.hom (sheafifyComposeIso J (forget D (FC := FD) (CC := CD)) P) :
      sheafify J (P ⋙ forget D (FC := FD) (CC := CD)) ⟶ sheafify J P ⋙ forget D (FC := FD) (CC := CD)))
Tactic: rw [← isLocallyInjective_forget_iff, ← sheafComposeIso_hom_fac,
    ← toSheafify_plusPlusIsoSheafify_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : IsIso φ
⊢ IsLocallyInjective (FD := FD) (CD := CD) φ
have change : Presheaf.IsLocallyInjective (FD := FD) (CD := CD) J (F₁ := Functor.obj (sheafToPresheaf J D) F₁)
  (Functor.map (sheafToPresheaf J D) φ)
Tactic: change Presheaf.IsLocallyInjective J ((sheafToPresheaf _ _).map φ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
⊢ Presieve.IsSeparated.{w, v, u} J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))
have h : Presieve.IsSheaf.{w, v, u} J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))
Tactic: apply Presieve.IsSheaf.isSeparated
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
⊢ Presieve.IsSheaf.{w, v, u} J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))
have h : Presheaf.IsSheaf J (F₁.obj (P := Presheaf.IsSheaf J) ⋙ forget D (FC := FD) (CC := CD))
Tactic: rw [← isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Sheaf.{v, v', u, u'} J D
φ : F₁ ⟶ F₂
inst_4 : GrothendieckTopology.HasSheafCompose.{v, v', w, u, u', w + 1} J (forget D (FC := FD) (CC := CD))
inst_5 : IsLocallyInjective (FD := FD) (CD := CD) φ
⊢ Mono φ
have hφ : ∀ (X : Cᵒᵖ),
  Function.Injective.{w + 1, w + 1} (α := CD (F₁.obj (P := Presheaf.IsSheaf J).obj X)) (β :=
    CD (F₂.obj (P := Presheaf.IsSheaf J).obj X))
    (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (φ.hom.app X)) : (a : CD (F₁.obj.obj X)) → CD (F₂.obj.obj X))
Tactic: apply mono_of_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F.obj (op V))
ht :
  Eq (α := CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op V)) : (a : CA (F.obj (op V))) → CA (G.obj (op V))) t :
      CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s :
      CA (G.obj (op V)))
j : W ⟶ V
⊢ ∃ (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F.obj (op W))),
    Eq (α := CA (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W))) t :
        CA (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (j ≫ i).op) : (a : CA (G.obj (op U))) → CA (G.obj (op W))) s :
        CA (G.obj (op W)))
have refine : Eq (α := CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
        CA (F.obj (op W))) :
    CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (j ≫ i).op) : (a : CA (G.obj (op U))) → CA (G.obj (op W))) s :
    CA (G.obj (op W)))
Tactic: refine ⟨F.map j.op t, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F.obj (op V))
ht :
  Eq (α := CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op V)) : (a : CA (F.obj (op V))) → CA (G.obj (op V))) t :
      CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s :
      CA (G.obj (op V)))
j : W ⟶ V
⊢ Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (j ≫ i).op) : (a : CA (G.obj (op U))) → CA (G.obj (op W))) s :
      CA (G.obj (op W)))
have rw : Eq (α := CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
        CA (F.obj (op W))) :
    CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (i.op ≫ j.op)) : (a : CA (G.obj (op U))) → CA (G.obj (op W))) s :
    CA (G.obj (op W)))
Tactic: rw [op_comp, G.map_comp, ConcreteCategory.comp_apply, ← ht, NatTrans.naturality_apply f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F.obj (op V))
ht :
  Eq (α := CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op V)) : (a : CA (F.obj (op V))) → CA (G.obj (op V))) t :
      CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s :
      CA (G.obj (op V)))
j : W ⟶ V
rw :
  Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (i.op ≫ j.op)) : (a : CA (G.obj (op U))) → CA (G.obj (op W)))
        s :
      CA (G.obj (op W)))
⊢ Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (j ≫ i).op) : (a : CA (G.obj (op U))) → CA (G.obj (op W))) s :
      CA (G.obj (op W)))
have rw₁ : Eq (α := CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
        CA (F.obj (op W))) :
    CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op ≫ G.map j.op) : (a : CA (G.obj (op U))) → CA (G.obj (op W)))
      s :
    CA (G.obj (op W)))
Tactic: rw [op_comp, G.map_comp, ConcreteCategory.comp_apply, ← ht, NatTrans.naturality_apply f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F.obj (op V))
ht :
  Eq (α := CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op V)) : (a : CA (F.obj (op V))) → CA (G.obj (op V))) t :
      CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s :
      CA (G.obj (op V)))
j : W ⟶ V
rw :
  Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (i.op ≫ j.op)) : (a : CA (G.obj (op U))) → CA (G.obj (op W)))
        s :
      CA (G.obj (op W)))
rw₁ :
  Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op ≫ G.map j.op) :
          (a : CA (G.obj (op U))) → CA (G.obj (op W)))
        s :
      CA (G.obj (op W)))
⊢ Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (j ≫ i).op) : (a : CA (G.obj (op U))) → CA (G.obj (op W))) s :
      CA (G.obj (op W)))
have rw₂ : Eq (α := CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
        CA (F.obj (op W))) :
    CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map j.op) : (a : CA (G.obj (op V))) → CA (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s :
        CA (G.obj (op V))) :
    CA (G.obj (op W)))
Tactic: rw [op_comp, G.map_comp, ConcreteCategory.comp_apply, ← ht, NatTrans.naturality_apply f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (G.obj (op U))
V : C
g : V ⟶ U
⊢ Sieve.pullback g (imageSieve (FA := FA) (CA := CA) f s) =
    imageSieve (FA := FA) (CA := CA) f
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map g.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s)
have h : ∀ ⦃W : C⦄ (g_1 : W ⟶ V),
  (Sieve.pullback g (imageSieve (FA := FA) (CA := CA) f s)).arrows g_1 ↔
    Sieve.arrows
      (imageSieve (FA := FA) (CA := CA) f
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map g.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s))
      g_1
Tactic: ext W g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F.obj (op U))
⊢ Eq (α := Sieve.{v, u} U)
    (imageSieve (FA := FA) (CA := CA) f
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op U)) : (a : CA (F.obj (op U))) → CA (G.obj (op U))) s))
    ⊤
have h : ∀ ⦃V : C⦄ (i : V ⟶ U),
  Sieve.arrows
      (imageSieve (FA := FA) (CA := CA) f
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op U)) : (a : CA (F.obj (op U))) → CA (G.obj (op U))) s))
      i ↔
    Sieve.arrows ⊤ i
Tactic: ext V i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F.obj (op U))
V : C
i : V ⟶ U
⊢ Sieve.arrows
      (imageSieve (FA := FA) (CA := CA) f
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op U)) : (a : CA (F.obj (op U))) → CA (G.obj (op U))) s))
      i ↔
    Sieve.arrows ⊤ i
have h : ∃ (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F.obj (op V))),
  Eq (α := CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op V)) : (a : CA (F.obj (op V))) → CA (G.obj (op V))) t :
      CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op U)) : (a : CA (F.obj (op U))) → CA (G.obj (op U))) s :
          CA (G.obj (op U))) :
      CA (G.obj (op V)))
Tactic: simp only [Sieve.top_apply, iff_true, imageSieve_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f ↔
    Subfunctor.sheafify J (Subfunctor.range (whiskerRight f (forget A (FC := FA) (CC := CA)))) = ⊤
have simp : IsLocallySurjective J (FA := FA) (CA := CA) f ↔
  ∀ (x : Cᵒᵖ) (x_1 : (G ⋙ forget A (FC := FA) (CC := CA)).obj x),
    x_1 ∈ (Subfunctor.sheafify J (Subfunctor.range (whiskerRight f (forget A (FC := FA) (CC := CA))))).obj x
Tactic: simp only [Subfunctor.ext_iff, funext_iff, Set.ext_iff, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f ↔
    IsLocallySurjective J (FA := TypeCat.Fun) (whiskerRight f (forget A (FC := FA) (CC := CA)))
have simp : Subfunctor.sheafify J (Subfunctor.range (whiskerRight f (forget A (FC := FA) (CC := CA)))) = ⊤ ↔
  Subfunctor.sheafify J
      (Subfunctor.range
        (whiskerRight (whiskerRight f (forget A (FC := FA) (CC := CA))) (forget (Type w') (FC := TypeCat.Fun)))) =
    ⊤
Tactic: simp only [isLocallySurjective_iff_range_sheafify_eq_top]