-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
φ : F ⟶ G
p q : F.Elements
x : p ⟶ q
f : p.fst (β := fun (c : C) ↦ F.obj c) ⟶ q.fst (β := fun (c : C) ↦ F.obj c)
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj q.fst))
      (p.snd (β := fun (c : C) ↦ F.obj c)) =
    q.snd (β := fun (c : C) ↦ F.obj c)
⊢ Eq (α :=
    (fun (X : Type w) ↦ X)
      (G.obj
        (Sigma.fst (β := fun (c : C) ↦ G.obj c)
          (match (motive := F.Elements → G.Elements) q with
          | ⟨X, x⟩ =>
            Sigma.mk (β := fun (c : C) ↦ G.obj c) X
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
                  (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                x)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) :
          (a :
              (fun (X : Type w) ↦ X)
                (G.obj
                  (match (motive := F.Elements → G.Elements) p with
                    | ⟨X, x⟩ =>
                      ⟨X,
                        (ConcreteCategory.hom (φ.app X) :
                            (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                          x⟩).fst)) →
            (fun (X : Type w) ↦ X)
              (G.obj
                (match (motive := F.Elements → G.Elements) q with
                  | ⟨X, x⟩ =>
                    ⟨X,
                      (ConcreteCategory.hom (φ.app X) :
                          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                        x⟩).fst))
        (Sigma.snd (β := fun (c : C) ↦ G.obj c)
          (match (motive := F.Elements → G.Elements) p with
          | ⟨X, x⟩ =>
            Sigma.mk (β := fun (c : C) ↦ G.obj c) X
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
                  (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                x))) :
      (fun (X : Type w) ↦ X)
        (G.obj
          (Sigma.fst (β := fun (c : C) ↦ G.obj c)
            (match (motive := F.Elements → G.Elements) q with
            | ⟨X, x⟩ =>
              Sigma.mk (β := fun (c : C) ↦ G.obj c) X
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
                    (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                  x)))))
    (Sigma.snd (β := fun (c : C) ↦ G.obj c)
        (match (motive := F.Elements → G.Elements) q with
        | ⟨X, x⟩ =>
          Sigma.mk (β := fun (c : C) ↦ G.obj c) X
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
              x)) :
      G.obj
        (Sigma.fst (β := fun (c : C) ↦ G.obj c)
          (match (motive := F.Elements → G.Elements) q with
          | ⟨X, x⟩ =>
            Sigma.mk (β := fun (c : C) ↦ G.obj c) X
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
                  (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                x))))
have hb : Eq (α := G.obj (q.fst (β := fun (c : C) ↦ F.obj c)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (q.fst (β := fun (c : C) ↦ F.obj c))) :
        (a : F.obj q.fst) → G.obj q.fst)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj p.fst) → F.obj q.fst)
          (p.snd (β := fun (c : C) ↦ F.obj c)) :
        F.obj (q.fst (β := fun (c : C) ↦ F.obj c))) :
    G.obj (q.fst (β := fun (c : C) ↦ F.obj c)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj p.fst) → G.obj q.fst)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (p.fst (β := fun (c : C) ↦ F.obj c))) :
            (a : F.obj p.fst) → G.obj p.fst)
          (p.snd (β := fun (c : C) ↦ F.obj c)) :
        G.obj (p.fst (β := fun (c : C) ↦ F.obj c))) :
    G.obj (q.fst (β := fun (c : C) ↦ F.obj c)))
Tactic: have hb := φ.naturality_apply f p.2