-- Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean
lemma regularTopology.isLocallySurjective_sheaf_of_types [Preregular C] [FinitaryPreExtensive C]
    {F G : Cᵒᵖ ⥤ Type w} (f : F ⟶ G) [PreservesFiniteProducts F] [PreservesFiniteProducts G]
      (h : Presheaf.IsLocallySurjective (coherentTopology C) f) :
        Presheaf.IsLocallySurjective (regularTopology C) f where
  imageSieve_mem y

Proof state:
case h.e'_2.h.h.e'_1
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this : f.app (op (Z a)) (x a) = G.map (π a).op y
e_1✝ : (forget (Type w)).obj (G.obj (op (Z a))) = G.obj (op (Z a))
⊢ ((PreservesProduct.iso F fun x => op (Z x)).hom ≫ Pi.π (fun b => F.obj (op (Z b))) a)
      ((PreservesProduct.iso F fun a => op (Z a)).inv ((Types.productIso fun a => F.obj (op (Z a))).inv x)) =
    x a

Tactic:
have := Types.productIso_hom_comp_eval (fun a ↦ F.obj (op (Z a))) a

Result:
case h.e'_2.h.h.e'_1
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝¹ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this✝ : f.app (op (Z a)) (x a) = G.map (π a).op y
e_1✝ : (forget (Type w)).obj (G.obj (op (Z a))) = G.obj (op (Z a))
this : ((Types.productIso fun a => F.obj (op (Z a))).hom ≫ fun f => f a) = Pi.π (fun a => F.obj (op (Z a))) a
⊢ ((PreservesProduct.iso F fun x => op (Z x)).hom ≫ Pi.π (fun b => F.obj (op (Z b))) a)
      ((PreservesProduct.iso F fun a => op (Z a)).inv ((Types.productIso fun a => F.obj (op (Z a))).inv x)) =
    x a

Proof state:
case h.e'_2.h.h.e'_1
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝¹ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this✝ : f.app (op (Z a)) (x a) = G.map (π a).op y
e_1✝ : (forget (Type w)).obj (G.obj (op (Z a))) = G.obj (op (Z a))
this : (fun f => f a) = (Types.productIso fun a => F.obj (op (Z a))).inv ≫ Pi.π (fun a => F.obj (op (Z a))) a
⊢ ((PreservesProduct.iso F fun x => op (Z x)).hom ≫ Pi.π (fun b => F.obj (op (Z b))) a)
      ((PreservesProduct.iso F fun a => op (Z a)).inv ((Types.productIso fun a => F.obj (op (Z a))).inv x)) =
    x a

Tactic:
simp only [types_comp_apply, inv_hom_id_apply, congrFun this x]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.a
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
⊢ ∀ (j : (Discrete α)ᵒᵖ),
    (ConcreteCategory.hom ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app j))
        ((ConcreteCategory.hom (f.app (op (∐ Z)))) (i'.hom x)) =
      (ConcreteCategory.hom ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app j))
        ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y)

Tactic:
intro ⟨⟨a⟩⟩

Result:
case intro.intro.intro.intro.intro.a
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
⊢ (ConcreteCategory.hom ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app (op { as := a })))
      ((ConcreteCategory.hom (f.app (op (∐ Z)))) (i'.hom x)) =
    (ConcreteCategory.hom ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app (op { as := a })))
      ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y)

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
⊢ Presheaf.imageSieve f y ∈ (regularTopology C) U✝

Tactic:
rw [mem_sieves_iff_hasEffectiveEpi]

Result:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π