-- 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))
⊢ (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

Tactic:
change F.map _ (F.map _ _) = _

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))
⊢ 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

Proof state:
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✝))
h : Presheaf.imageSieve f y ∈ (coherentTopology C) U✝
⊢ Presheaf.imageSieve f y ∈ (regularTopology C) U✝

Tactic:
rw [coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily] at h

Result:
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✝))
h : ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
⊢ Presheaf.imageSieve f y ∈ (regularTopology C) U✝

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))
⊢ ((piComparison F fun x => op (Z x)) ≫ 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:
change ((PreservesProduct.iso F _).hom ≫ _) _ = _

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))
⊢ ((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'_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))
⊢ G.map (Sigma.ι Z a).op (G.map (Sigma.desc π).op y) = G.map (π a).op y

Tactic:
simp only [← FunctorToTypes.map_comp_apply, ← op_comp, Sigma.ι_desc]

Result:
no goals