-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PreservesLocallyBijective (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
H : Functor.{v_1, v_2, u_1, u_2} C D
F G : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst_3 : (X Y : A) → FunLike.{u_4 + 1, u_5 + 1, u_5 + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory.{u_5, v_3, u_3, u_4} A FA (CC := CA)
hH : CoverPreserving J K H
inst_5 : H.IsCoverDense K
inst_6 : IsLocallyInjective (FD := FA) (CD := CA) J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType.{u_5, v_3, u_3, u_4} (FC := FA) (CC := CA) (F.obj X)
h :
  Eq (α := CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X))
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
h₁ :
  Eq (α := CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) : (a : CA (G.obj X)) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X)) :
      CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
          (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
              (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
            b :
          CA (F.obj (Opposite.op (H.obj Z)))) :
      CA (G.obj (Opposite.op (H.obj Z))))
h₂ :
  Eq (α := CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) : (a : CA (G.obj X)) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) a : CA (G.obj X)) :
      CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) : (a : CA (G.obj X)) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X)) :
      CA (G.obj (Opposite.op (H.obj Z))))
⊢ Eq (α := CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
          (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
              (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
            a :
          CA (F.obj (Opposite.op (H.obj Z)))) :
      CA (G.obj (Opposite.op (H.obj Z))))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (Opposite.op (H.obj Z))) :
          (a : CA (F.obj (Opposite.op (H.obj Z)))) → CA (G.obj (Opposite.op (H.obj Z))))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map m.op) :
              (a : CA (F.obj X)) → CA (F.obj (Opposite.op (H.obj Z))))
            b :
          CA (F.obj (Opposite.op (H.obj Z)))) :
      CA (G.obj (Opposite.op (H.obj Z))))
have h₃ : Eq (α := CA (G.obj (Opposite.op (H.obj Z))))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) : (a : CA (G.obj X)) → CA (G.obj (Opposite.op (H.obj Z))))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X)) :
    CA (G.obj (Opposite.op (H.obj Z))))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map m.op) : (a : CA (G.obj X)) → CA (G.obj (Opposite.op (H.obj Z))))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app X) : (a : CA (F.obj X)) → CA (G.obj X)) b : CA (G.obj X)) :
    CA (G.obj (Opposite.op (H.obj Z))))
Tactic: rw [NatTrans.naturality_apply, NatTrans.naturality_apply, h]