-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (hypothesis)
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
h_1 : discretePresieve δ g
x : ε
h_2 : ∀ (y : ε), y = x
⊢ Eq (α := (fun (X : Type u) ↦ X) (S.obj (op ε)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map g.op) :
          (a : (fun (X : Type u) ↦ X) (S.obj (op δ))) → (fun (X : Type u) ↦ X) (S.obj (op ε)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map g₁.op) :
              (a : (fun (X : Type u) ↦ X) (S.obj (op β))) → (fun (X : Type u) ↦ X) (S.obj (op δ)))
            ((fun (x : Type u) (g : x ⟶ α) (hg : discretePresieve α g) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (↾fun (x : x) ↦ PUnit.unit))) :
                      (a : (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))) → (fun (X : Type u) ↦ X) (S.obj (op x)))
                    (f
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) g :
                          (a : (fun (X : Type u) ↦ X) x) → (fun (X : Type u) ↦ X) α)
                        (Classical.choose (p := fun (x_1 : x) ↦ ∀ (y : x), y = x_1) hg))) :
                  (fun (X : Type u) ↦ X) (S.obj (op x))))
              β f₁ hf₁) :
          (fun (X : Type u) ↦ X) (S.obj (op δ))) :
      (fun (X : Type u) ↦ X) (S.obj (op ε)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map g.op) :
          (a : (fun (X : Type u) ↦ X) (S.obj (op δ))) → (fun (X : Type u) ↦ X) (S.obj (op ε)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map g₂.op) :
              (a : (fun (X : Type u) ↦ X) (S.obj (op γ))) → (fun (X : Type u) ↦ X) (S.obj (op δ)))
            ((fun (x : Type u) (g : x ⟶ α) (hg : discretePresieve α g) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (↾fun (x : x) ↦ PUnit.unit))) :
                      (a : (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))) → (fun (X : Type u) ↦ X) (S.obj (op x)))
                    (f
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) g :
                          (a : (fun (X : Type u) ↦ X) x) → (fun (X : Type u) ↦ X) α)
                        (Classical.choose (p := fun (x_1 : x) ↦ ∀ (y : x), y = x_1) hg))) :
                  (fun (X : Type u) ↦ X) (S.obj (op x))))
              γ f₂ hf₂) :
          (fun (X : Type u) ↦ X) (S.obj (op δ))) :
      (fun (X : Type u) ↦ X) (S.obj (op ε)))
have this : Eq (α := (fun (X : Type u) ↦ X) α)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f₁ : (a : (fun (X : Type u) ↦ X) β) → (fun (X : Type u) ↦ X) α)
      (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf₁) :
    (fun (X : Type u) ↦ X) α)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f₂ : (a : (fun (X : Type u) ↦ X) γ) → (fun (X : Type u) ↦ X) α)
      (Classical.choose (p := fun (x : γ) ↦ ∀ (y : γ), y = x) hf₂) :
    (fun (X : Type u) ↦ X) α)
Tactic: have : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂) :=
        Classical.choose_spec hf₁ (g₁ <| g x) ▸
          Classical.choose_spec hf₂ (g₂ <| g x) ▸ ConcreteCategory.congr_hom h _