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 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))
⊢ imageSieve (FA := FA) (CA := CA) f s ∈ (J : (a : C) → Set (Sieve a)) U
have 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
Tactic: obtain ⟨t, rfl⟩ := H _ s
Cleared hypotheses: s
-- 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
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))
⊢ 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
have rw : ⊤ ∈ (J : (a : C) → Set (Sieve a)) U
Tactic: rw [imageSieve_app]
-- 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
inst_4 : IsIso f
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f
have 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))
Tactic: apply isLocallySurjective_of_surjective
-- 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
inst_4 : IsIso f
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))
have 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))
Tactic: apply Function.Bijective.surjective
-- 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
inst_4 : IsIso f
U : Cᵒᵖ
⊢ 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))
have 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)))
Tactic: rw [bijective_iff_isIso_ofHom]
-- 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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows j
t' : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₁.obj (op V))
ht' :
  Eq (α := CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₂.obj (op V))) t' :
      CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map i.op) : (a : CA (F₂.obj (op W))) → CA (F₂.obj (op V)))
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op W))) ↦
          Eq (α := CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op W)) :
                  (a : CA (F₂.obj (op W))) → CA (F₃.obj (op W)))
                t :
              CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op W)))
                s :
              CA (F₃.obj (op W))))
          H) :
      CA (F₂.obj (op V)))
⊢ (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s).arrows (i ≫ j)
have refine : Eq (α := CA (F₃.obj (op V)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
      t' :
    CA (F₃.obj (op V)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map (i ≫ j).op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V))) s :
    CA (F₃.obj (op V)))
Tactic: refine ⟨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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows j
t' : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₁.obj (op V))
ht' :
  Eq (α := CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₂.obj (op V))) t' :
      CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map i.op) : (a : CA (F₂.obj (op W))) → CA (F₂.obj (op V)))
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op W))) ↦
          Eq (α := CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op W)) :
                  (a : CA (F₂.obj (op W))) → CA (F₃.obj (op W)))
                t :
              CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op W)))
                s :
              CA (F₃.obj (op W))))
          H) :
      CA (F₂.obj (op V)))
⊢ Eq (α := CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
        t' :
      CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map (i ≫ j).op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
        s :
      CA (F₃.obj (op V)))
have rw : Eq (α := CA (F₃.obj (op V)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
      t' :
    CA (F₃.obj (op V)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map (j.op ≫ i.op)) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
      s :
    CA (F₃.obj (op V)))
Tactic: rw [op_comp, F₃.map_comp, NatTrans.comp_app, ConcreteCategory.comp_apply,
        ConcreteCategory.comp_apply, ht', NatTrans.naturality_apply, H.choose_spec]
-- 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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows j
t' : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₁.obj (op V))
ht' :
  Eq (α := CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₂.obj (op V))) t' :
      CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map i.op) : (a : CA (F₂.obj (op W))) → CA (F₂.obj (op V)))
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op W))) ↦
          Eq (α := CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op W)) :
                  (a : CA (F₂.obj (op W))) → CA (F₃.obj (op W)))
                t :
              CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op W)))
                s :
              CA (F₃.obj (op W))))
          H) :
      CA (F₂.obj (op V)))
rw :
  Eq (α := CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
        t' :
      CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map (j.op ≫ i.op)) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
        s :
      CA (F₃.obj (op V)))
⊢ Eq (α := CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
        t' :
      CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map (i ≫ j).op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
        s :
      CA (F₃.obj (op V)))
have rw₁ : Eq (α := CA (F₃.obj (op V)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
      t' :
    CA (F₃.obj (op V)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op ≫ F₃.map i.op) :
        (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
      s :
    CA (F₃.obj (op V)))
Tactic: rw [op_comp, F₃.map_comp, NatTrans.comp_app, ConcreteCategory.comp_apply,
        ConcreteCategory.comp_apply, ht', NatTrans.naturality_apply, H.choose_spec]
-- 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₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
⊢ imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s ∈ (J : (a : C) → Set (Sieve a)) U
have this : (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
    fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
    imageSieve (FA := FA) (CA := CA) f₁
      (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
        Eq (α := CA (F₃.obj (op x)))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) : (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
              t :
            CA (F₃.obj (op x)))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
              s :
            CA (F₃.obj (op x))))
        h)) ≤
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s
Tactic: have : (Sieve.bind (imageSieve f₂ s) fun _ _ h => imageSieve f₁ h.choose) ≤
        imageSieve (f₁ ≫ f₂) s := by
      rintro V i ⟨W, i, j, H, ⟨t', ht'⟩, rfl⟩
      refine ⟨t', ?_⟩
      rw [op_comp, F₃.map_comp, NatTrans.comp_app, ConcreteCategory.comp_apply,
        ConcreteCategory.comp_apply, ht', NatTrans.naturality_apply, H.choose_spec]
-- 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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
this :
  (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ≤
    imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s
⊢ imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s ∈ (J : (a : C) → Set (Sieve a)) U
have apply : (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
    fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
    imageSieve (FA := FA) (CA := CA) f₁
      (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
        Eq (α := CA (F₃.obj (op x)))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) : (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
              t :
            CA (F₃.obj (op x)))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
              s :
            CA (F₃.obj (op x))))
        h)) ∈
  (J : (a : C) → Set (Sieve a)) U
Tactic: apply J.superset_covering this
-- 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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
this :
  (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ≤
    imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s
⊢ (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ∈
    (J : (a : C) → Set (Sieve a)) U
have hS : imageSieve (FA := FA) (CA := CA) f₂ s ∈ (J : (a : C) → Set (Sieve a)) U
Tactic: apply J.bind_covering
-- 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₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
this :
  (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ≤
    imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) s
hS : imageSieve (FA := FA) (CA := CA) f₂ s ∈ (J : (a : C) → Set (Sieve a)) U
⊢ (Sieve.bind (imageSieve (FA := FA) (CA := CA) f₂ s).arrows
      fun (x : C) (x_1 : x ⟶ U) (h : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows x_1) ↦
      imageSieve (FA := FA) (CA := CA) f₁
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op x))) ↦
          Eq (α := CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op x)) :
                  (a : CA (F₂.obj (op x))) → CA (F₃.obj (op x)))
                t :
              CA (F₃.obj (op x)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map x_1.op) :
                  (a : CA (F₃.obj (op U))) → CA (F₃.obj (op x)))
                s :
              CA (F₃.obj (op x))))
          h)) ∈
    (J : (a : C) → Set (Sieve a)) U
have hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U⦄ (H : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows f),
  imageSieve (FA := FA) (CA := CA) f₁
      (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op Y))) ↦
        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)))
              t :
            CA (F₃.obj (op Y)))
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map f.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op Y)))
              s :
            CA (F₃.obj (op Y))))
        H) ∈
    (J : (a : C) → Set (Sieve a)) Y
Tactic: apply J.bind_covering
-- 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₂)
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op X))
⊢ imageSieve (FA := FA) (CA := CA) f₂ x ∈ (J : (a : C) → Set (Sieve a)) X
have refine : imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂) x ≤ imageSieve (FA := FA) (CA := CA) f₂ x
Tactic: refine J.superset_covering ?_ (imageSieve_mem J (f₁ ≫ f₂) x)
-- 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₃
⊢ 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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₃ ↔ IsLocallySurjective J (FA := FA) (CA := CA) f₂
have mp : IsLocallySurjective J (FA := FA) (CA := CA) 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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
mp : IsLocallySurjective J (FA := FA) (CA := CA) f₃ → IsLocallySurjective J (FA := FA) (CA := CA) f₂
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₃ ↔ IsLocallySurjective J (FA := FA) (CA := CA) f₂
have mpr : IsLocallySurjective J (FA := FA) (CA := CA) f₂ → IsLocallySurjective J (FA := FA) (CA := CA) f₃
Tactic: constructor