-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
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
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) α)
⊢ 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 simp_rw : Eq (α := S.obj (op ε))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (g ≫ g₁ ≫ ↾fun (x : β) ↦ PUnit.unit))) :
        (a : S.obj (op PUnit.{u + 1})) → S.obj (op ε))
      (f
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f₂ : (a : γ) → α)
          (Classical.choose (p := fun (x : γ) ↦ ∀ (y : γ), y = x) hf₂))) :
    S.obj (op ε))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (g ≫ g₂ ≫ ↾fun (x : γ) ↦ PUnit.unit))) :
        (a : S.obj (op PUnit.{u + 1})) → S.obj (op ε))
      (f
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f₂ : (a : γ) → α)
          (Classical.choose (p := fun (x : γ) ↦ ∀ (y : γ), y = x) hf₂))) :
    S.obj (op ε))
Tactic: simp_rw [← comp_apply, ← Functor.map_comp, this, ← op_comp]