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 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)))

Tactic:
⟨F.map j.op t, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, Exists.intro, DFunLike.coe
-- 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 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
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)))
⊢ ∃ (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)))

Tactic:
refine ⟨F.map j.op t, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
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
⊢ 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)

Tactic:
ext W g

Premises used: CategoryTheory.GrothendieckTopology.W
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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_1 : V ⟶ U
W : C
g : W ⟶ V
⊢ (Sieve.pullback g_1 (imageSieve (FA := FA) (CA := CA) f s)).arrows g ↔
    Sieve.arrows
      (imageSieve (FA := FA) (CA := CA) f
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map g_1.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s))
      g

Tactic:
simp [imageSieve]

Premises used: CategoryTheory.Presheaf.imageSieve
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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))
⊢ imageSieve (FA := FA) (CA := CA) f s =
    (Subfunctor.range (whiskerRight f (forget A (FC := FA) (CC := CA)))).sieveOfSection s

Tactic:
rfl

Premises used: CategoryTheory.Subfunctor.sieveOfSection, Set.Mem, setOf, Set.range, rfl
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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))
⊢ imageSieve (FA := TypeCat.Fun) (whiskerRight f (forget A (FC := FA) (CC := CA))) s =
    imageSieve (FA := FA) (CA := CA) f s

Tactic:
rfl

Premises used: CategoryTheory.Presheaf.imageSieve, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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))
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
⊢ 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))
    ⊤

Tactic:
ext V i
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
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)))
⊢ 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:
simp only [Sieve.top_apply, iff_true, imageSieve_apply]

Premises used: CategoryTheory.Sieve.top_apply, iff_true, CategoryTheory.Presheaf.imageSieve_apply
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
⊢ ∃ (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:
⟨F.map i.op s, NatTrans.naturality_apply f i.op s⟩

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, Exists.intro, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
⊢ ∃ (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:
exact ⟨F.map i.op s, NatTrans.naturality_apply f i.op s⟩
-- 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f
U : Cᵒᵖ
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (G.obj U)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U))
    (imageSieve (FA := FA) (CA := CA) f s)

Tactic:
IsLocallySurjective.imageSieve_mem _

Premises used: CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem
-- 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
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
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f ↔
    Subfunctor.sheafify J (Subfunctor.range (whiskerRight f (forget A (FC := FA) (CC := CA)))) = ⊤

Tactic:
simp only [Subfunctor.ext_iff, funext_iff, Set.ext_iff, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]

Premises used: iff_true, funext_iff, Set.top_eq_univ, Set.mem_univ, CategoryTheory.Subfunctor.top_obj, Set.ext_iff, CategoryTheory.Subfunctor.ext_iff
-- 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
⊢ 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:
⟨fun H _ => H.imageSieve_mem, fun H => ⟨H _⟩⟩

Premises used: CategoryTheory.Presheaf.IsLocallySurjective.mk, CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem, Opposite.op, Iff.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)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
⊢ 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:
exact ⟨fun H _ => H.imageSieve_mem, fun H => ⟨H _⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
⊢ IsLocallySurjective J (FA := TypeCat.Fun) f ↔ Subfunctor.sheafify J (Subfunctor.range f) = ⊤

Tactic:
apply isLocallySurjective_iff_range_sheafify_eq_top

Premises used: CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_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)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
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)))) =
      ⊤
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f ↔
    IsLocallySurjective J (FA := TypeCat.Fun) (whiskerRight f (forget A (FC := FA) (CC := CA)))

Tactic:
simp only [isLocallySurjective_iff_range_sheafify_eq_top]

Premises used: CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_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)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
⊢ 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:
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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
H :
  ∀ (U : Cᵒᵖ),
    Function.Surjective.{w' + 1, w' + 1} (α := CA (F.obj U)) (β := CA (G.obj U))
      (⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U))
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (G.obj (op U))
obtain :
  ∀ (t : CA (F.obj (op 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))) t) ∈
      (J : (a : C) → Set (Sieve a)) U
⊢ imageSieve (FA := FA) (CA := CA) f s ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
obtain ⟨t, rfl⟩ := H _ s

Premises used: 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
H :
  ∀ (U : Cᵒᵖ),
    Function.Surjective.{w' + 1, w' + 1} (α := CA (F.obj U)) (β := CA (G.obj U))
      (⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U))
U : C
t : CA (F.obj (op U))
rw : ⊤ ∈ (J : (a : C) → Set (Sieve a)) 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))) t) ∈
    (J : (a : C) → Set (Sieve a)) U

Tactic:
rw [imageSieve_app]

Premises used: CategoryTheory.Presheaf.imageSieve_app
-- 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
H :
  ∀ (U : Cᵒᵖ),
    Function.Surjective.{w' + 1, w' + 1} (α := CA (F.obj U)) (β := CA (G.obj U))
      (⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U))
U : C
t : CA (F.obj (op U))
⊢ ⊤ ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
J.top_mem _

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
H :
  ∀ (U : Cᵒᵖ),
    Function.Surjective.{w' + 1, w' + 1} (α := CA (F.obj U)) (β := CA (G.obj U))
      (⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U))
U : C
t : CA (F.obj (op U))
⊢ ⊤ ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
exact J.top_mem _

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
inst_4 : IsIso f
H :
  ∀ (U : Cᵒᵖ),
    Function.Surjective.{w' + 1, w' + 1} (α := CA (F.obj U)) (β := CA (G.obj U))
      (⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U))
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f

Tactic:
apply isLocallySurjective_of_surjective

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_surjective
-- 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
inst_4 : IsIso f
U : Cᵒᵖ
H :
  Function.Bijective.{w' + 1, w' + 1} (α := CA (F.obj U)) (β := CA (G.obj U))
    (⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U))
⊢ Function.Surjective.{w' + 1, w' + 1} (α := CA (F.obj U)) (β := CA (G.obj U))
    (⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U))

Tactic:
apply Function.Bijective.surjective

Premises used: Function.Bijective.surjective
-- 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
inst_4 : IsIso f
U : Cᵒᵖ
H :
  IsIso.{w', w' + 1} (X := CA (F.obj U)) (Y := CA (G.obj U))
    (↾(⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U)))
⊢ Function.Bijective.{w' + 1, w' + 1} (α := CA (F.obj U)) (β := CA (G.obj U))
    (⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U))

Tactic:
rw [bijective_iff_isIso_ofHom]

Premises used: CategoryTheory.bijective_iff_isIso_ofHom
-- 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 G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
inst_4 : IsIso f
U : Cᵒᵖ
⊢ IsIso.{w', w' + 1} (X := CA (F.obj U)) (Y := CA (G.obj U))
    (↾(⇑(ConcreteCategory.hom (FC := FA) (CC := CA) (f.app U)) : (a : CA (F.obj U)) → CA (G.obj U)))

Tactic:
infer_instance