-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
X : Cᵒᵖ
x : G.obj X
Y Z : C
f : Y ⟶ Opposite.unop X
⊢ (fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
        ∃ (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))),
          Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map 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 Y)))
                x :
              (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                  (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
                    (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
                a :
              (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))))
      Y f →
    ∀ (g : Z ⟶ Y),
      (fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
          ∃ (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))),
            Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map 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 Y)))
                  x :
                (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                    (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
                      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
                  a :
                (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))))
        Z (g ≫ f)
have this : ∀ (a : F.obj (Opposite.op Y))
  (ha :
    Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map 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 Y)))
          x :
        (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
            (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
              (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
          a :
        (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))))
  (g : Z ⟶ Y),
  (fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
      ∃ (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))),
        Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map 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 Y)))
              x :
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
                  (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
              a :
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y))))
    Z (g ≫ f)
Tactic: ⟨a, ha⟩