-- 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 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)
x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π

Tactic:
let i' : ((a : α) → (F.obj ⟨Z a⟩)) ≅ (F.obj ⟨∐ Z⟩) := (Types.productIso _).symm ≪≫
  (PreservesProduct.iso F _).symm ≪≫ F.mapIso (opCoproductIsoProduct _).symm

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)
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
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π

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)
x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π

Tactic:
let _ : Fintype α := Fintype.ofFinite _

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)
x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯
x✝ : Fintype α := Fintype.ofFinite α
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π

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
a : α
this : f.app (op (Z a)) (x a) = G.map (π a).op y
⊢ (ConcreteCategory.hom (f.app (op (Z a))))
      ((ConcreteCategory.hom (F.map (Sigma.ι Z a).op))
        (F.map (opCoproductIsoProduct Z).inv
          ((PreservesProduct.iso F fun a => op (Z a)).inv ((Types.productIso fun a => F.obj (op (Z a))).inv x)))) =
    (ConcreteCategory.hom (G.map (Sigma.ι Z a).op)) ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y)

Tactic:
convert this

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))
⊢ (ConcreteCategory.hom (F.map (Sigma.ι Z a).op))
      (F.map (opCoproductIsoProduct Z).inv
        ((PreservesProduct.iso F fun a => op (Z a)).inv ((Types.productIso fun a => F.obj (op (Z a))).inv x))) =
    x a

case h.e'_3.h
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))
⊢ (ConcreteCategory.hom (G.map (Sigma.ι Z a).op)) ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y) =
    G.map (π a).op y