-- 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
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 α
⊢ ∃ a, f.app (op X) a = x

Tactic:
let ht := (Types.productLimitCone (fun a ↦ F.obj ⟨Y a⟩)).isLimit

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 ⋯
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
⊢ ∃ 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 : α
⊢ f.app (op (Y a)) ((i.hom ≫ F.map (π a).op) y) = (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)

Tactic:
erw [IsLimit.map_π]

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 : α
⊢ f.app (op (Y a))
      (((Types.productLimitCone fun a => F.obj (op (Y a))).cone.π.app { as := a } ≫
          (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as)))).hom.app { as := a })
        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)
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
⊢ ∃ a, f.app (op X) a = x

Tactic:
let i : ((a : α) → (F.obj ⟨Y a⟩)) ≅ (F.obj ⟨X⟩) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht')
    (Discrete.natIso (fun _ ↦ (Iso.refl (F.obj ⟨_⟩))))

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 ⋯
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, f.app (op X) a = x