-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation (R := R) t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ Eq (α := P.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) : (a : P.obj (op X)) → P.obj (op Y)) t : P.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (P.map
              ⋯.choose (p :=
                  fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf) ↦
                  ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf ⟶ X),
                    R g ∧ h ≫ g = f).op) :
          (a : P.obj (op (Exists.choose hf))) → P.obj (op Y))
        (x
          (⋯.choose (p :=
            fun (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf ⟶ X) ↦
            R g ∧
              ⋯.choose (p :=
                    fun
                      (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf) ↦
                    ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf ⟶ X),
                      R g ∧ h ≫ g = f) ≫
                  g =
                f))
          ⋯) :
      P.obj (op Y))
have rw : Eq (α := P.obj (op Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) : (a : P.obj (op X)) → P.obj (op Y)) t : P.obj (op Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (P.map
            sorry.choose (p :=
                fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf) ↦
                ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf ⟶ X),
                  R g ∧ h ≫ g = f).op) :
        (a : P.obj (op (Exists.choose hf))) → P.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (P.map
                sorry.choose (p :=
                    fun
                      (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf ⟶ X) ↦
                    R g ∧
                      sorry.choose (p :=
                            fun
                              (h :
                                Y ⟶
                                  Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f)
                                    hf) ↦
                            ∃ (g :
                              Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf ⟶
                                X),
                              R g ∧ h ≫ g = f) ≫
                          g =
                        f).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (Exists.choose hf))))
          t :
        (fun (X : Type w) ↦ X)
          (P.obj (op (Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) hf)))) :
    P.obj (op Y))
Tactic: rw [← ht _, ← comp_apply, ← Functor.map_comp, ← op_comp, hf.choose_spec.choose_spec.choose_spec.2]