Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, 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 ⋯
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 : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
⊢ (ConcreteCategory.hom (f.app (op (Z a))))
      ((ConcreteCategory.hom (F.map (Sigma.ι Z a).op))
        ((ConcreteCategory.hom (F.map (opCoproductIsoProduct Z).inv))
          ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
            ((ConcreteCategory.hom (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

Goal state after:
case e'_2
C : Type u_1
inst✝⁴ : Category.{v_1, 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 ⋯
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 : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
⊢ (ConcreteCategory.hom (F.map (Sigma.ι Z a).op))
      ((ConcreteCategory.hom (F.map (opCoproductIsoProduct Z).inv))
        ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
          ((ConcreteCategory.hom (Types.productIso fun a ↦ F.obj (op (Z a))).inv) x))) =
    x a

case e'_3
C : Type u_1
inst✝⁴ : Category.{v_1, 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 ⋯
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 : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
⊢ (ConcreteCategory.hom (G.map (Sigma.ι Z a).op)) ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y) =
    (ConcreteCategory.hom (G.map (π a).op)) y