-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : G.obj X) ↦
            {
              arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
                ∃ (a : F.obj (Opposite.op Y)),
                  Eq (α := G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
                      G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                          (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                        a :
                      G.obj (Opposite.op Y)),
              downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) }) :
        (a : G.obj X) → (Functor.sieves C).obj X)
      x)
    f
⊢ Sieve.arrows
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : G.obj X) ↦
            {
              arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
                ∃ (a : F.obj (Opposite.op Y)),
                  Eq (α := G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
                      G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                          (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                        a :
                      G.obj (Opposite.op Y)),
              downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) }) :
        (a : G.obj X) → (Functor.sieves C).obj X)
      x)
    f
have choose : ∀
  (a :
    (Z : C) →
      (g : Z ⟶ Y) →
        (hg :
            (Sieve.pullback f
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X) :
                      (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) →
                        (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
                    x)).arrows
              g) →
          (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z)))
  (ha :
    ∀ (Z : C) (g : Z ⟶ Y)
      (hg :
        (Sieve.pullback f
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X) :
                  (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) →
                    (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
                x)).arrows
          g),
      Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (g ≫ f).op) :
              (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
                (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Z)) :
              (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))) →
                (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
            (a Z g hg) :
          (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))),
  Sieve.arrows
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : G.obj X) ↦
            {
              arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
                ∃ (a : F.obj (Opposite.op Y)),
                  Eq (α := G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
                      G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                          (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                        a :
                      G.obj (Opposite.op Y)),
              downward_closed := sorry : Sieve.{v, u} (Opposite.unop X) }) :
        (a : G.obj X) → (Functor.sieves C).obj X)
      x)
    f
Tactic: choose a ha using fun Z (g : Z ⟶ Y) (hg : (Sieve.pullback f ((χ m).app X x)).arrows g) => hg