awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op X))
S : Sieve.{v, u} X :=
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    equalizerSieve.{w', v', v, u', u, u_1} (FD := FA) (CD := CA) (F := F₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x)
          f hf))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x)
Y : C
f : Y ⟶ unop (op X)
hf :
  Sieve.arrows
    (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x))
    f
⊢ T f hf ∈ (J : (a : C) → Set (Sieve a)) Y
have refine_2 : Eq (α := CA (F₃.obj (op Y)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
          (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) :
                (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
              x)
            f hf) :
        CA (F₂.obj (op Y))) :
    CA (F₃.obj (op Y)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x :
        CA (F₂.obj (op Y))) :
    CA (F₃.obj (op Y)))
Tactic: apply equalizerSieve_mem J f₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (hypothesis)
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₃
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₁
have inst : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
Tactic: subst fac
Cleared hypotheses: f₃, fac, inst_4
-- 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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
⊢ IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂) ↔ IsLocallyInjective (FD := FA) (CD := CA) J f₂
have mp : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂) → IsLocallyInjective (FD := FA) (CD := CA) J f₂
Tactic: constructor
-- 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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
mp : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂) → IsLocallyInjective (FD := FA) (CD := CA) J f₂
⊢ IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂) ↔ IsLocallyInjective (FD := FA) (CD := CA) J f₂
have mpr : IsLocallyInjective (FD := FA) (CD := CA) J f₂ → IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
Tactic: constructor
-- 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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
⊢ IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂) ↔ IsLocallySurjective J (FA := FA) (CA := CA) f₁
have mp : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂) → IsLocallySurjective J (FA := FA) (CA := CA) f₁
Tactic: constructor
-- 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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
mp : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂) → IsLocallySurjective J (FA := FA) (CA := CA) f₁
⊢ IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂) ↔ IsLocallySurjective J (FA := FA) (CA := CA) f₁
have mpr : IsLocallySurjective J (FA := FA) (CA := CA) f₁ → IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
Tactic: constructor
-- 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₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F₁ ⟶ F₂
X : C
s : F₂.obj (op X)
hs : Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) s
⊢ imageSieve (FA := TypeCat.Fun) (Subfunctor.toRangeSheafify J f)
      (Subtype.mk (p := fun (x : F₂.obj (op X)) ↦
        Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) x) s hs) ∈
    (J : (a : C) → Set (Sieve a)) X
have refine : (Subfunctor.range f).sieveOfSection s ≤
  imageSieve (FA := TypeCat.Fun) (Subfunctor.toRangeSheafify J f)
    (Subtype.mk (p := fun (x : F₂.obj (op X)) ↦
      Membership.mem (γ := Set (F₂.obj (op X))) ((Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)) x) s hs)
Tactic: refine J.superset_covering ?_ hs
-- 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 : Cᵒᵖ ⥤ Type (max u v)
⊢ Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))) ≫
      J.sheafifyLift (Subfunctor.toRangeSheafify J (J.toSheafify F)) ⋯ =
    𝟙 (Subfunctor.toFunctor (F := J.sheafify F) (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))))
have rw : Eq (α :=
  Subfunctor.toFunctor (F := J.sheafify F) (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))) ⟶ J.sheafify F)
  (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))) ≫
    CategoryStruct.comp (Y :=
      Subfunctor.toFunctor (F := J.sheafify F) (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))))
      (J.sheafifyLift (Subfunctor.toRangeSheafify J (J.toSheafify F)) sorry)
      (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F)))))
  (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))))
Tactic: rw [← cancel_mono (Subfunctor.ι _), Category.id_comp, Category.assoc]
-- 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 : Cᵒᵖ ⥤ Type (max u v)
⊢ Eq (α :=
    Subfunctor.toFunctor (F := J.sheafify F) (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))) ⟶ J.sheafify F)
    (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))) ≫
      CategoryStruct.comp (Y :=
        Subfunctor.toFunctor (F := J.sheafify F) (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))))
        (J.sheafifyLift (Subfunctor.toRangeSheafify J (J.toSheafify F)) ⋯)
        (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F)))))
    (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))) ≫ 𝟙 (J.sheafify F))
have e_a : CategoryStruct.comp (Y :=
    Subfunctor.toFunctor (F := J.sheafify F) (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))))
    (J.sheafifyLift (Subfunctor.toRangeSheafify J (J.toSheafify F)) sorry)
    (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F)))) =
  𝟙 (J.sheafify F)
Tactic: congr 1
-- 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)
P : Cᵒᵖ ⥤ Type (max u v)
U : C
x : ToType (FC := TypeCat.Fun) ((J.plusObj P).obj (op U))
⊢ imageSieve (FA := TypeCat.Fun) (J.toPlus P) x ∈ (J : (a : C) → Set (Sieve a)) U
have obtain : ∀ (S : J.Cover U) (x : Meq (FD := TypeCat.Fun) P S),
  imageSieve (FA := TypeCat.Fun) (G := J.plusObj P) (J.toPlus P) (Plus.mk (FD := TypeCat.Fun) x) ∈
    (J : (a : C) → Set (Sieve a)) U
Tactic: obtain ⟨S, x, rfl⟩ := exists_rep x
Cleared hypotheses: x
-- 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)
P : Cᵒᵖ ⥤ Type (max u v)
U : C
S : J.Cover U
x : Meq (FD := TypeCat.Fun) P S
⊢ imageSieve (FA := TypeCat.Fun) (G := J.plusObj P) (J.toPlus P) (Plus.mk (FD := TypeCat.Fun) x) ∈
    (J : (a : C) → Set (Sieve a)) U
have refine : ∀ (Y : C) (f : Y ⟶ U) (hf : (↑S : Sieve U).arrows f),
  Eq (α := (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (J.toPlus P) (op Y)) :
          (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op Y))) →
            (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf }) :
      (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((J.plusObj P).map f.op) :
          (a : (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op U))) →
            (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
        (Plus.mk (FD := TypeCat.Fun) x) :
      (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
Tactic: refine J.superset_covering (fun Y f hf => ⟨x.1 ⟨Y, f, hf⟩, ?_⟩) S.2
-- 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)
P : Cᵒᵖ ⥤ Type (max u v)
U : C
S : J.Cover U
x : Meq (FD := TypeCat.Fun) P S
Y : C
f : Y ⟶ U
hf : (↑S : Sieve U).arrows f
⊢ Eq (α := (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (J.toPlus P) (op Y)) :
          (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op Y))) →
            (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf }) :
      (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((J.plusObj P).map f.op) :
          (a : (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op U))) →
            (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
        (Plus.mk (FD := TypeCat.Fun) x) :
      (fun (X : Type (max u v)) ↦ X) ((J.plusObj P).obj (op Y)))
have rw : ∃ (W : J.Cover Y) (h1 : W ⟶ ⊤) (h2 : W ⟶ (J.pullback f).obj S),
  Meq.refine (FD := TypeCat.Fun)
      (Meq.mk (FD := TypeCat.Fun) ⊤
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf : S.Arrow }))
      h1 =
    (x.pullback (FD := TypeCat.Fun) f).refine (FD := TypeCat.Fun) h2
Tactic: rw [toPlus_eq_mk, res_mk_eq_mk_pullback, eq_mk_iff_exists]
-- 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)
P : Cᵒᵖ ⥤ Type (max u v)
U : C
S : J.Cover U
x : Meq (FD := TypeCat.Fun) P S
Y : C
f : Y ⟶ U
hf : (↑S : Sieve U).arrows f
⊢ ∃ (W : J.Cover Y) (h1 : W ⟶ ⊤) (h2 : W ⟶ (J.pullback f).obj S),
    Meq.refine (FD := TypeCat.Fun)
        (Meq.mk (FD := TypeCat.Fun) ⊤
          ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf : S.Arrow }))
        h1 =
      (x.pullback (FD := TypeCat.Fun) f).refine (FD := TypeCat.Fun) h2
have refine : Meq.refine (FD := TypeCat.Fun) (T := ⊤)
    (Meq.mk (FD := TypeCat.Fun) ⊤ ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf }))
    (homOfLE sorry) =
  (x.pullback (FD := TypeCat.Fun) f).refine (FD := TypeCat.Fun) (𝟙 (S.pullback f))
Tactic: refine ⟨S.pullback f, homOfLE le_top, 𝟙 _, ?_⟩
-- 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)
P : Cᵒᵖ ⥤ Type (max u v)
U : C
S : J.Cover U
x : Meq (FD := TypeCat.Fun) P S
Y : C
f : Y ⟶ U
hf : (↑S : Sieve U).arrows f
⊢ Meq.refine (FD := TypeCat.Fun) (T := ⊤)
      (Meq.mk (FD := TypeCat.Fun) ⊤ ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf }))
      (homOfLE ⋯) =
    (x.pullback (FD := TypeCat.Fun) f).refine (FD := TypeCat.Fun) (𝟙 (S.pullback f))
have h : ∀ (Z : C) (g : Z ⟶ Y) (hg : (↑(S.pullback f) : Sieve Y).arrows g),
  (↑(Meq.refine (FD := TypeCat.Fun) (T := ⊤)
            (Meq.mk (FD := TypeCat.Fun) ⊤
              ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf : S.Arrow }))
            (homOfLE sorry)) :
        (I : (S.pullback f).Arrow) → ToType (P.obj (op I.Y)))
      { Y := Z, f := g, hf := hg } =
    (↑((x.pullback (FD := TypeCat.Fun) f).refine (FD := TypeCat.Fun) (𝟙 (S.pullback f))) :
        (I : (S.pullback f).Arrow) → ToType (P.obj (op I.Y)))
      { Y := Z, f := g, hf := hg : (S.pullback f).Arrow }
Tactic: ext ⟨Z, g, hg⟩
-- 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)
P : Cᵒᵖ ⥤ Type (max u v)
⊢ IsLocallySurjective J (FA := TypeCat.Fun) (G := J.sheafify P) (J.toPlus P ≫ J.plusMap (J.toPlus P))
have rw : IsLocallySurjective J (FA := TypeCat.Fun) (G := J.sheafify P) (J.toPlus P ≫ J.toPlus (J.plusObj P))
Tactic: rw [GrothendieckTopology.plusMap_toPlus]
-- 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)
D : Type u_2
inst_4 : Category.{v_1, u_2} D
FD : D → D → Type u_3
CD : D → Type (max u v)
inst_5 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_6 : ConcreteCategory D FD (CC := CD)
P : Functor.{v, v_1, u, u_2} Cᵒᵖ D
inst_7 : HasWeakSheafify.{v, v_1, u, u_2} J D
inst_8 : J.HasSheafCompose (forget D (FC := FD) (CC := CD))
inst_9 : J.PreservesSheafification (forget D (FC := FD) (CC := CD))
⊢ IsLocallySurjective J (FA := FD) (CA := CD) (G := sheafify J P) (toSheafify J P)
have rw : IsLocallySurjective J (FA := TypeCat.Fun) (G := 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 [isLocallySurjective_iff_whisker_forget,
    ← sheafComposeIso_hom_fac, ← toSheafify_plusPlusIsoSheafify_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (hypothesis)
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₁ F₂ F₃ : Sheaf.{v, v', u, u'} J A
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst_4 : IsIso φ
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ
have this : IsIso φ.hom
Tactic: have : IsIso φ.hom := (inferInstance : IsIso ((sheafToPresheaf J A).map φ))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f.hom ↔ IsIso (imageι f)
have rw : IsIso (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι ↔
  IsIso (C := Sheaf J (Type w)) (X := image f) (Y := G) { hom := (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι }
Tactic: rw [Sheaf.imageι, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top',
    Subfunctor.eq_top_iff_isIso]
-- 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₁_1 F₂_1 F₃ : Sheaf.{v, v', u, u'} J A
φ_1 : F₁_1 ⟶ F₂_1
ψ : F₂_1 ⟶ F₃
inst_4 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst_5 : IsLocallySurjective (FA := TypeCat.Fun) φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
⊢ f₁ = f₂
have h₁ : ∀ (X : Cᵒᵖ) (x : F₂.obj (P := Presheaf.IsSheaf J).obj X),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app X)).toFun x
Tactic: ext X x
-- 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₁_1 F₂_1 F₃ : Sheaf.{v, v', u, u'} J A
φ_1 : F₁_1 ⟶ F₂_1
ψ : F₂_1 ⟶ F₃
inst_4 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst_5 : IsLocallySurjective (FA := TypeCat.Fun) φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj (P := Presheaf.IsSheaf J).obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app X)).toFun x
have h₁ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄,
  (Presheaf.imageSieve (FA := TypeCat.Fun) φ.hom x).arrows f →
    Eq (α := (fun (X : Type w) ↦ X) (Z.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
            (a : (fun (X : Type w) ↦ X) (Z.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (Z.obj.obj (op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app X)).toFun x) :
        (fun (X : Type w) ↦ X) (Z.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
            (a : (fun (X : Type w) ↦ X) (Z.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (Z.obj.obj (op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app X)).toFun x) :
        (fun (X : Type w) ↦ X) (Z.obj (P := Presheaf.IsSheaf J).obj (op Y)))
Tactic: apply (((isSheaf_iff_isSheaf_of_type _ _).1 Z.2).isSeparated _
      (Presheaf.imageSieve_mem J φ.hom x)).ext