-- 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 Y : C
f : X ⟶ Y
simp_rw simp_rw₁ :
  (∀ (b : P.obj (op X)),
      FamilyOfElements.Compatible.{w, v₁, u₁} (P := P) (R := singleton f)
          (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f)) b) →
        ∃! t : P.obj (op Y),
          FamilyOfElements.IsAmalgamation (R := singleton f)
            (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f)) b)
            t) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f →
            Eq (α := P.obj (op Z))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) : (a : P.obj (op X)) → P.obj (op Z)) x :
                P.obj (op Z))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) : (a : P.obj (op X)) → P.obj (op Z)) x :
                P.obj (op Z))) →
        ∃! y : P.obj (op Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) : (a : P.obj (op Y)) → P.obj (op X)) y = x
simp_rw₂ :
  (∀ (b : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f →
            Eq (α := P.obj (op Z))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) : (a : P.obj (op X)) → P.obj (op Z))
                  (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f))
                      b f ⋯ :
                    P.obj (op X)) :
                P.obj (op Z))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) : (a : P.obj (op X)) → P.obj (op Z))
                  (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f))
                      b f ⋯ :
                    P.obj (op X)) :
                P.obj (op Z))) →
        ∃! t : P.obj (op Y),
          FamilyOfElements.IsAmalgamation (R := singleton f)
            (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f)) b)
            t) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f →
            Eq (α := P.obj (op Z))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) : (a : P.obj (op X)) → P.obj (op Z)) x :
                P.obj (op Z))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) : (a : P.obj (op X)) → P.obj (op Z)) x :
                P.obj (op Z))) →
        ∃! y : P.obj (op Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) : (a : P.obj (op Y)) → P.obj (op X)) y = x
⊢ (∀ (b : P.obj (op X)),
      FamilyOfElements.Compatible.{w, v₁, u₁} (P := P) (R := singleton f)
          (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f)) b) →
        ∃! t : P.obj (op Y),
          FamilyOfElements.IsAmalgamation (R := singleton f)
            (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f)) b)
            t) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f →
            Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) :
                    (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
                  x :
                (fun (X : Type w) ↦ X) (P.obj (op Z)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) :
                    (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
                  x :
                (fun (X : Type w) ↦ X) (P.obj (op Z)))) →
        ∃! y : (fun (X : Type w) ↦ X) (P.obj (op Y)),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
              y =
            x
have simp_rw₃ : (∀ (b : P.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f →
          Eq (α := P.obj (op Z))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) : (a : P.obj (op X)) → P.obj (op Z))
                (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f)) b
                    f sorry :
                  P.obj (op X)) :
              P.obj (op Z))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) : (a : P.obj (op X)) → P.obj (op Z))
                (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f)) b
                    f sorry :
                  P.obj (op X)) :
              P.obj (op Z))) →
      ∃! t : P.obj (op Y),
        Eq (α := P.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) : (a : P.obj (op Y)) → P.obj (op X)) t : P.obj (op X))
          (((FamilyOfElements.singletonEquiv P f).symm : (a : P.obj (op X)) → FamilyOfElements P (singleton f)) b f sorry :
            P.obj (op X))) ↔
  ∀ (x : P.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f →
          Eq (α := P.obj (op Z))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) : (a : P.obj (op X)) → P.obj (op Z)) x :
              P.obj (op Z))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) : (a : P.obj (op X)) → P.obj (op Z)) x :
              P.obj (op Z))) →
      ∃! y : P.obj (op Y),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) : (a : P.obj (op Y)) → P.obj (op X)) y = x
Tactic: simp_rw [FamilyOfElements.compatible_singleton_iff,
    FamilyOfElements.isAmalgamation_singleton_iff, FamilyOfElements.singletonEquiv_symm_apply_self]