-- Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean
lemma extensiveTopology.presheafIsLocallySurjective_iff [FinitaryPreExtensive C] {F G : Cᵒᵖ ⥤ D}
    (f : F ⟶ G) [PreservesFiniteProducts F] [PreservesFiniteProducts G]
      [PreservesFiniteProducts (forget D)] : Presheaf.IsLocallySurjective (extensiveTopology C) f ↔
        ∀ (X : C), Function.Surjective (f.app (op X))

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁴ : ConcreteCategory D FD
inst✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
h : ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) f

Tactic:
refine ⟨fun {X} y ↦ ?_⟩

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁴ : ConcreteCategory D FD
inst✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
h : ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))
X : C
y : ToType (G.obj (op X))
⊢ Presheaf.imageSieve f y ∈ (extensiveTopology C) X

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁴ : ConcreteCategory D FD
inst✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) f →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))

Tactic:
rw [Presheaf.isLocallySurjective_iff_whisker_forget (J := extensiveTopology C)]

Result:
case mp
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁴ : ConcreteCategory D FD
inst✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (whiskerRight f (forget D)) →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))

Proof state:
case h.e'_5
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁴ : ConcreteCategory D FD
inst✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
h : ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))
X : C
y : ToType (G.obj (op X))
x : CD (F.obj (op X))
hx : (ConcreteCategory.hom (f.app (op X))) x = y
⊢ (Presheaf.imageSieve f y).arrows (𝟙 X)

Tactic:
simpa [Presheaf.imageSieve] using ⟨x, hx⟩

Result:
no goals