-- Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean
lemma extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types [FinitaryPreExtensive C]
    {F G : Cᵒᵖ ⥤ Type w} (f : F ⟶ G) [PreservesFiniteProducts F] [PreservesFiniteProducts G]
      (h : Presheaf.IsLocallySurjective (extensiveTopology C) f) {X : C} :
        Function.Surjective (f.app (op X))

Proof state:
case intro.intro.intro.intro.intro.a
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : 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 f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom (G.map (π a).op)) (f.app (op X) (i.hom y)) = (ConcreteCategory.hom (G.map (π a).op)) x

Tactic:
rw [← (h' a).choose_spec]

Result:
case intro.intro.intro.intro.intro.a
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : 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 f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom (G.map (π a).op)) (f.app (op X) (i.hom y)) =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : 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 f x).arrows (π a)
⊢ ∃ a, f.app (op X) a = x

Tactic:
let y : (a : α) → (F.obj ⟨Y a⟩) := fun a ↦ (h' a).choose

Result:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : 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 f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯
⊢ ∃ a, f.app (op X) a = x

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
h : Presheaf.IsLocallySurjective (extensiveTopology C) f
X : C
x : G.obj (op X)
⊢ ∃ a, f.app (op X) a = x

Tactic:
replace h := h.1 x

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
h : Presheaf.imageSieve f x ∈ (extensiveTopology C) X
⊢ ∃ a, f.app (op X) a = x

Proof state:
case intro.intro.intro.intro.intro.a
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : 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 f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom (G.map (π a).op)) (f.app (op X) (i.hom y)) =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)

Tactic:
erw [← NatTrans.naturality_apply (φ := f)]

Result:
case intro.intro.intro.intro.intro.a
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : 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 f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom (f.app (op (Y a)))) ((ConcreteCategory.hom (F.map (π a).op)) (i.hom y)) =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)