-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Sieves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
rw :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₁.op ≫ F.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
        s :
      F.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y₂)))
            s :
          (fun (X : Type w) ↦ X) (F.obj (op Y₂))) :
      (fun (X : Type w) ↦ X) (F.obj (op Z)))
rw₁ :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₁.op ≫ g₁.op)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
        s :
      F.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y₂)))
            s :
          (fun (X : Type w) ↦ X) (F.obj (op Y₂))) :
      (fun (X : Type w) ↦ X) (F.obj (op Z)))
rw₂ :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₁.op ≫ g₁.op)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
        s :
      F.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂.op ≫ F.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
        s :
      F.obj (op Z))
rw₃ :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₁.op ≫ g₁.op)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
        s :
      F.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂.op ≫ g₂.op)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
        s :
      F.obj (op Z))
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₁.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y₁)))
            s :
          (fun (X : Type w) ↦ X) (F.obj (op Y₁))) :
      (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y₂)))
            s :
          (fun (X : Type w) ↦ X) (F.obj (op Y₂))) :
      (fun (X : Type w) ↦ X) (F.obj (op Z)))
have rw₄ : Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g₁ ≫ f₁).op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
      s :
    F.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂.op ≫ g₂.op)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
      s :
    F.obj (op Z))
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp, ← op_comp, ← op_comp, e]