-- 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
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
              ⋯.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
                  ⋯.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).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))
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
                ⋯.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).op ≫
              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 : (fun (X : Type w) ↦ X) (P.obj (op X))) → P.obj (op Y))
        t :
      P.obj (op Y))
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
              (⋯.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).op ≫
                ⋯.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 : (fun (X : Type w) ↦ X) (P.obj (op X))) → P.obj (op Y))
        t :
      P.obj (op Y))
⊢ 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) ≫
                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))) → P.obj (op Y))
      t :
    P.obj (op Y))
Tactic: rw [← ht _, ← comp_apply, ← Functor.map_comp, ← op_comp, hf.choose_spec.choose_spec.choose_spec.2]