awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) (Presieve.ofArrows Y π)
have mpr : IsIso (X := sigmaObj.{0, v_1, u_1} Y) (Sigma.desc π)
Tactic: refine ⟨α, inferInstance, Y, π, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
⊢ Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f ↔
    ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
      ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
        ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
        Eq (α := CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
              x :
            CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X')))
              y :
            CD (G.obj (op X')))
have mp : Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f →
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
mp :
  Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f →
    ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
      ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
        ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
        Eq (α := CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
              x :
            CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X')))
              y :
            CD (G.obj (op X')))
⊢ Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f ↔
    ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
      ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
        ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
        Eq (α := CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
              x :
            CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X')))
              y :
            CD (G.obj (op X')))
have mpr : (∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))) →
  Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h :
  ∀ {U : C} (s : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))),
    Presheaf.imageSieve (FA := FD) (CA := CD) f s ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
X : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))
have h₁ : Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) X
Tactic: specialize h y
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
X : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))
h : Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) X
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))
have h₁ : ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π
Tactic: rw [regularTopology.mem_sieves_iff_hasEffectiveEpi] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
X : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))
h : ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))
have mp : ∀ (X' : C) (π : X' ⟶ X) (h : EffectiveEpi π) (h' : (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π),
  ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))
Tactic: obtain ⟨X', π, h, h'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h :
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
⊢ Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f
have mpr : ∀ {U : C} (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))),
  Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
Tactic: refine ⟨fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h :
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
U : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))
⊢ Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
have mpr : ∀ (X' : C) (π : X' ⟶ U) (h : EffectiveEpi π)
  (h' :
    ∃ (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op π)) : (a : CD (G.obj (op U))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))),
  Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
Tactic: obtain ⟨X', π, h, h'⟩ := h _ y
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h_1 :
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
U : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))
X' : C
π : X' ⟶ U
h : EffectiveEpi π
h' :
  ∃ (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op π)) : (a : CD (G.obj (op U))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))
⊢ Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
have mpr : ∃ (Y : C) (π : Y ⟶ U), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π
Tactic: rw [regularTopology.mem_sieves_iff_hasEffectiveEpi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_2 : PreservesFiniteProducts F
inst_3 : PreservesFiniteProducts G
h : Presheaf.IsLocallySurjective (extensiveTopology C) (FA := TypeCat.Fun) f
X : C
x : G.obj (op X)
⊢ ∃ (a : (fun (X : Type w) ↦ X) (F.obj (op X))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op X)))
        a =
      x
have h₁ : Presheaf.imageSieve (FA := TypeCat.Fun) f x ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X
Tactic: replace h := h.1 x
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_2 : PreservesFiniteProducts F
inst_3 : PreservesFiniteProducts G
X : C
x : G.obj (op X)
h : Presheaf.imageSieve (FA := TypeCat.Fun) f x ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X
⊢ ∃ (a : (fun (X : Type w) ↦ X) (F.obj (op X))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op X)))
        a =
      x
have h₁ : ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
  Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)
Tactic: rw [mem_sieves_iff_contains_colimit_cofan] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_2 : PreservesFiniteProducts F
inst_3 : PreservesFiniteProducts G
X : C
x : G.obj (op X)
h :
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)
⊢ ∃ (a : (fun (X : Type w) ↦ X) (F.obj (op X))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op X)))
        a =
      x
have obtain : ∀ (α : Type),
  Finite α →
    ∀ (Y : α → C) (π : (a : α) → Y a ⟶ X) (h : Nonempty (IsColimit (Cofan.mk X π)))
      (h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)),
      ∃ (a : (fun (X : Type w) ↦ X) (F.obj (op X))),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op X)))
            a =
          x
Tactic: obtain ⟨α, _, Y, π, h, h'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_2 : PreservesFiniteProducts F
inst_3 : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Y a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Y a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Y a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            x :
          (fun (X : Type w) ↦ X) (G.obj (op (Y a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
ht : IsLimit (J := Discrete α) (F := Discrete.functor fun (a : α) ↦ F.obj (op (Y a)))
  (LimitCone.cone (Types.productLimitCone fun (a : α) ↦ F.obj (op (Y a)))) :=
  LimitCone.isLimit (Types.productLimitCone fun (a : α) ↦ F.obj (op (Y a)))
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  ((Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm :
      (a : IsLimit (Cocone.op (Cofan.mk X π))) →
        IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))))
    h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht')
    (Discrete.natIso fun (x : Discrete α) ↦ Iso.refl (F.obj (op (Y x.as))))
⊢ ∃ (a : (fun (X : Type w) ↦ X) (F.obj (op X))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op X)))
        a =
      x
have refine : (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
      (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) i.hom :
          (a : (fun (X : Type w) ↦ X) ((a : α) → F.obj (op (Y a)))) → (fun (X : Type w) ↦ X) (F.obj (op X)))
        y :
      (fun (X : Type w) ↦ X) (F.obj (op X))) =
  x
Tactic: refine ⟨i.hom y, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_5 : PreservesFiniteProducts F
inst_6 : PreservesFiniteProducts G
inst_7 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f ↔
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := CD (G.obj (op X)))
        (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X))) : (a : CD (F.obj (op X))) → CD (G.obj (op X)))
have mp : Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f →
  ∀ (X : C),
    Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := CD (G.obj (op X)))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X))) : (a : CD (F.obj (op X))) → CD (G.obj (op X)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_5 : PreservesFiniteProducts F
inst_6 : PreservesFiniteProducts G
inst_7 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
mp :
  Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f →
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := CD (G.obj (op X)))
        (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X))) : (a : CD (F.obj (op X))) → CD (G.obj (op X)))
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f ↔
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := CD (G.obj (op X)))
        (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X))) : (a : CD (F.obj (op X))) → CD (G.obj (op X)))
have mpr : (∀ (X : C),
    Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := CD (G.obj (op X)))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X))) : (a : CD (F.obj (op X))) → CD (G.obj (op X)))) →
  Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_5 : PreservesFiniteProducts F
inst_6 : PreservesFiniteProducts G
inst_7 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f →
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := CD (G.obj (op X)))
        (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X))) : (a : CD (F.obj (op X))) → CD (G.obj (op X)))
have mp : Presheaf.IsLocallySurjective (extensiveTopology C) (FA := TypeCat.Fun)
    (Functor.whiskerRight f (forget D (FC := FD) (CC := CD))) →
  ∀ (X : C),
    Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := CD (G.obj (op X)))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X))) : (a : CD (F.obj (op X))) → CD (G.obj (op X)))
Tactic: rw [Presheaf.isLocallySurjective_iff_whisker_forget (J := extensiveTopology C)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
h : Presheaf.IsLocallySurjective (coherentTopology C) (FA := TypeCat.Fun) f
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
have h₁ : Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (coherentTopology C : (a : C) → Set (Sieve a)) U
Tactic: replace h := h.1 y
Cleared hypotheses: h