-- 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:
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:
constructor

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) f →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))

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)
⊢ (∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))) →
    Presheaf.IsLocallySurjective (extensiveTopology C) f

Proof state:
case mpr.intro
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 ∈ (extensiveTopology C) X

Tactic:
convert (extensiveTopology C).top_mem' X

Result:
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 = ⊤

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 = ⊤

Tactic:
rw [← Sieve.id_mem_iff_eq_top]

Result:
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)

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) (whiskerRight f (forget D)) →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))

Tactic:
exact fun h _ ↦ surjective_of_isLocallySurjective_sheaf_of_types (whiskerRight f (forget D)) h

Result:
no goals

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)
⊢ (∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))) →
    Presheaf.IsLocallySurjective (extensiveTopology C) f

Tactic:
intro h

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)))
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) f

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)))
X : C
y : ToType (G.obj (op X))
⊢ Presheaf.imageSieve f y ∈ (extensiveTopology C) X

Tactic:
obtain ⟨x, hx⟩ := h X y

Result:
case mpr.intro
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 ∈ (extensiveTopology C) X