-- Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean
lemma isLocallySurjective_π_app_zero_of_isLocallySurjective_map  :
    Sheaf.IsLocallySurjective (c.π.app ⟨0⟩)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).val.obj (op X))
hh : EffectiveEpi (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0))
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ),
      ∃ x,
        (ConcreteCategory.hom ((c.π.app (op 0)).val.app (op X'))) x =
          (ConcreteCategory.hom ((F.obj (op 0)).val.map (op φ))) y

Tactic:
refine ⟨limit (preimageDiagram hF X y), limit.π (preimageDiagram hF X y) ⟨0⟩, hh,
  (coherentTopology C).yonedaEquiv (hc.lift (cone hF X y )),
  (?_ : (c.π.app (op 0)).val.app _ _ = _)⟩

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).val.obj (op X))
hh : EffectiveEpi (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0))
⊢ (c.π.app (op 0)).val.app (op (limit (CategoryTheory.coherentTopology.preimageDiagram hF X y)))
      ((coherentTopology C).yonedaEquiv (hc.lift (CategoryTheory.coherentTopology.cone hF X y))) =
    (ConcreteCategory.hom
        ((F.obj (op 0)).val.map (op (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0)))))
      y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).val.obj (op X))
hh : EffectiveEpi (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0))
⊢ ((coherentTopology C).yonedaEquiv.symm ((CategoryTheory.coherentTopology.preimageStruct hF X y).x 0)).val.app
      (op (limit (CategoryTheory.coherentTopology.preimageDiagram hF X y)))
      (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0)) =
    (ConcreteCategory.hom
        ((F.obj (op 0)).val.map (op (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0)))))
      y

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).val.obj (op X))
hh : EffectiveEpi (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0))
⊢ (c.π.app (op 0)).val.app (op (limit (CategoryTheory.coherentTopology.preimageDiagram hF X y)))
      ((coherentTopology C).yonedaEquiv (hc.lift (CategoryTheory.coherentTopology.cone hF X y))) =
    (ConcreteCategory.hom
        ((F.obj (op 0)).val.map (op (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0)))))
      y

Tactic:
simp only [← (coherentTopology C).yonedaEquiv_comp, Functor.const_obj_obj, cone,
  IsLimit.fac, NatTrans.ofOpSequence_app, (coherentTopology C).yonedaEquiv_comp,
  (coherentTopology C).yonedaEquiv_yoneda_map]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).val.obj (op X))
hh : EffectiveEpi (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0))
⊢ ((coherentTopology C).yonedaEquiv.symm ((CategoryTheory.coherentTopology.preimageStruct hF X y).x 0)).val.app
      (op (limit (CategoryTheory.coherentTopology.preimageDiagram hF X y)))
      (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0)) =
    (ConcreteCategory.hom
        ((F.obj (op 0)).val.map (op (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0)))))
      y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
⊢ ∀ (X : C) (y : ToType ((F.obj (op 0)).val.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ),
        ∃ x,
          (ConcreteCategory.hom ((c.π.app (op 0)).val.app (op X'))) x =
            (ConcreteCategory.hom ((F.obj (op 0)).val.map (op φ))) y

Tactic:
intro X y

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).val.obj (op X))
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ),
      ∃ x,
        (ConcreteCategory.hom ((c.π.app (op 0)).val.app (op X'))) x =
          (ConcreteCategory.hom ((F.obj (op 0)).val.map (op φ))) y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
⊢ Sheaf.IsLocallySurjective (c.π.app (op 0))

Tactic:
rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
⊢ ∀ (X : C) (y : ToType ((F.obj (op 0)).val.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ),
        ∃ x,
          (ConcreteCategory.hom ((c.π.app (op 0)).val.app (op X'))) x =
            (ConcreteCategory.hom ((F.obj (op 0)).val.map (op φ))) y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).val.obj (op X))
n : ℕ
⊢ EffectiveEpi ((CategoryTheory.coherentTopology.preimageDiagram hF X y).map (homOfLE ⋯).op)

Tactic:
simpa [preimageDiagram] using (preimageStruct hF X y).effectiveEpi n

Result:
no goals