-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F.obj (op V))
ht :
  Eq (α := CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op V)) : (a : CA (F.obj (op V))) → CA (G.obj (op V))) t :
      CA (G.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s :
      CA (G.obj (op V)))
j : W ⟶ V
rw :
  Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (i.op ≫ j.op)) : (a : CA (G.obj (op U))) → CA (G.obj (op W)))
        s :
      CA (G.obj (op W)))
rw₁ :
  Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op ≫ G.map j.op) :
          (a : CA (G.obj (op U))) → CA (G.obj (op W)))
        s :
      CA (G.obj (op W)))
rw₂ :
  Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map j.op) : (a : CA (G.obj (op V))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map i.op) : (a : CA (G.obj (op U))) → CA (G.obj (op V))) s :
          CA (G.obj (op V))) :
      CA (G.obj (op W)))
⊢ Eq (α := CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
          CA (F.obj (op W))) :
      CA (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map (j ≫ i).op) : (a : CA (G.obj (op U))) → CA (G.obj (op W))) s :
      CA (G.obj (op W)))
have rw₃ : Eq (α := CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op W)) : (a : CA (F.obj (op W))) → CA (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.map j.op) : (a : CA (F.obj (op V))) → CA (F.obj (op W))) t :
        CA (F.obj (op W))) :
    CA (G.obj (op W)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (G.map j.op) : (a : CA (G.obj (op V))) → CA (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f.app (op V)) : (a : CA (F.obj (op V))) → CA (G.obj (op V))) t :
        CA (G.obj (op V))) :
    CA (G.obj (op W)))
Tactic: rw [op_comp, G.map_comp, ConcreteCategory.comp_apply, ← ht, NatTrans.naturality_apply f]