-- 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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₂
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve (FA := FA) (CA := CA) f₂ s).arrows j
t' : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₁.obj (op V))
ht' :
  Eq (α := CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₂.obj (op V))) t' :
      CA (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map i.op) : (a : CA (F₂.obj (op W))) → CA (F₂.obj (op V)))
        (Exists.choose (p := fun (t : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op W))) ↦
          Eq (α := CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op W)) :
                  (a : CA (F₂.obj (op W))) → CA (F₃.obj (op W)))
                t :
              CA (F₃.obj (op W)))
            ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op W)))
                s :
              CA (F₃.obj (op W))))
          H) :
      CA (F₂.obj (op V)))
rw :
  Eq (α := CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
        t' :
      CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map (j.op ≫ i.op)) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
        s :
      CA (F₃.obj (op V)))
rw₁ :
  Eq (α := CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
        t' :
      CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op ≫ F₃.map i.op) :
          (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
        s :
      CA (F₃.obj (op V)))
rw₂ :
  Eq (α := CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op V) ≫ f₂.app (op V)) :
          (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
        t' :
      CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op ≫ F₃.map i.op) :
          (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
        s :
      CA (F₃.obj (op V)))
⊢ Eq (α := CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₃.obj (op V)))
        t' :
      CA (F₃.obj (op V)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map (i ≫ j).op) : (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
        s :
      CA (F₃.obj (op V)))
have rw₃ : Eq (α := CA (F₃.obj (op V)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op V)) : (a : CA (F₂.obj (op V))) → CA (F₃.obj (op V)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op V)) : (a : CA (F₁.obj (op V))) → CA (F₂.obj (op V))) t' :
        CA (F₂.obj (op V))) :
    CA (F₃.obj (op V)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map j.op ≫ F₃.map i.op) :
        (a : CA (F₃.obj (op U))) → CA (F₃.obj (op V)))
      s :
    CA (F₃.obj (op V)))
Tactic: rw [op_comp, F₃.map_comp, NatTrans.comp_app, ConcreteCategory.comp_apply,
        ConcreteCategory.comp_apply, ht', NatTrans.naturality_apply, H.choose_spec]