awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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)
⊢ CategoryStruct.comp (Y := J.sheafify F) (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))))) =
    J.toSheafify F ≫ 𝟙 (J.sheafify F)

Tactic:
simp [Subfunctor.toRangeSheafify]

Premises used: CategoryTheory.Subfunctor.toRangeSheafify
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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)
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)) ⋯)
        (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F)))))
    (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))))
⊢ 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))))

Tactic:
rw [← cancel_mono (Subfunctor.ι _), Category.id_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Subfunctor.ι, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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))))

Tactic:
Eq.trans ?_ (Category.comp_id _)

Premises used: CategoryTheory.Category.comp_id, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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)
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)) ⋯)
      (Subfunctor.ι (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F)))) =
    𝟙 (J.sheafify F)
⊢ 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))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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)
⊢ 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)))) =
    𝟙 (J.sheafify F)

Tactic:
exact J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [Subfunctor.toRangeSheafify])

Premises used: CategoryTheory.GrothendieckTopology.sheafify_hom_ext, CategoryTheory.GrothendieckTopology.sheafify_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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))
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
⊢ imageSieve (FA := TypeCat.Fun) (J.toPlus P) x ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
obtain ⟨S, x, rfl⟩ := exists_rep x

Premises used: CategoryTheory.GrothendieckTopology.Plus.exists_rep, rfl
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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

Tactic:
J.superset_covering (fun Y f hf => ⟨x.1 ⟨Y, f, hf⟩, ?_⟩) S.2

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, Exists.intro, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk, Subtype.val, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
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)))
⊢ 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:
refine J.superset_covering (fun Y f hf => ⟨x.1 ⟨Y, f, hf⟩, ?_⟩) S.2
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
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
⊢ 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:
rw [toPlus_eq_mk, res_mk_eq_mk_pullback, eq_mk_iff_exists]

Premises used: CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk, CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback, CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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

Tactic:
⟨S.pullback f, homOfLE le_top, 𝟙 _, ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.GrothendieckTopology.Cover.pullback, le_top, CategoryTheory.homOfLE, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
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 ⋯) =
    (x.pullback (FD := TypeCat.Fun) f).refine (FD := TypeCat.Fun) (𝟙 (S.pullback 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

Tactic:
refine ⟨S.pullback f, homOfLE le_top, 𝟙 _, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
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 ⋯)) :
          (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 }
⊢ 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))

Tactic:
ext ⟨Z, g, hg⟩
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
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 ⋯)) :
        (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:
simpa using x.2 { fst.hf := hf, snd.hf := S.1.downward_closed hf g, r.g₁ := g, r.g₂ := 𝟙 Z, .. }

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.GrothendieckTopology.Cover.Relation.mk, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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)
rw : IsLocallySurjective J (FA := TypeCat.Fun) (G := J.sheafify P) (J.toPlus P ≫ J.toPlus (J.plusObj P))
⊢ IsLocallySurjective J (FA := TypeCat.Fun) (G := J.sheafify P) (J.toPlus P ≫ J.plusMap (J.toPlus P))

Tactic:
rw [GrothendieckTopology.plusMap_toPlus]

Premises used: CategoryTheory.GrothendieckTopology.plusMap_toPlus
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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.toPlus (J.plusObj P))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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))
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)))
⊢ IsLocallySurjective J (FA := FD) (CA := CD) (G := sheafify J P) (toSheafify J P)

Tactic:
rw [isLocallySurjective_iff_whisker_forget,
    ← sheafComposeIso_hom_fac, ← toSheafify_plusPlusIsoSheafify_hom]

Premises used: CategoryTheory.sheafComposeIso_hom_fac, CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.toSheafify_plusPlusIsoSheafify_hom
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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 := 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:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₂ : Sheaf.{v, v', u, u'} J A
φ : F₁ ⟶ F₂
⊢ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (F := obj (sheafToPresheaf J A) F₁)
      (map (sheafToPresheaf J A) φ) ↔
    IsLocallySurjective (FA := FA) (CA := CA) φ

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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 : IsLocallySurjective (FA := FA) (CA := CA) φ
inst_5 : IsLocallySurjective (FA := FA) (CA := CA) ψ
⊢ IsLocallySurjective (FA := FA) (CA := CA) (φ ≫ ψ)

Tactic:
Presheaf.isLocallySurjective_comp J φ.hom ψ.hom

Premises used: CategoryTheory.Presheaf.isLocallySurjective_comp, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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 φ
⊢ IsIso φ.hom

Tactic:
have : IsIso φ.hom := (inferInstance : IsIso ((sheafToPresheaf J A).map φ))
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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 φ
this : IsIso φ.hom
⊢ IsLocallySurjective (FA := FA) (CA := CA) φ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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₃
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallySurjective.{v, u, w, w + 1, w, w} (C := C) (J := J) (FA := TypeCat.Fun) (F₁ := F) (F₂ := image f)
    { hom := Subfunctor.toRangeSheafify J f.hom }

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
inst_5 : IsLocallySurjective (FA := FA) (CA := CA) φ
⊢ IsLocallySurjective (FA := TypeCat.Fun) (F₁ := obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F₁)
    (map (sheafCompose J (forget A (FC := FA) (CC := CA))) φ)

Tactic:
(Presheaf.isLocallySurjective_iff_whisker_forget J φ.hom).1 inferInstance

Premises used: CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.Functor.whiskerRight, Iff.mp, CategoryTheory.InducedCategory.Hom.hom