-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map φ.op) :
          (a : P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) →
            P.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map ((Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op) :
              (a : P.obj (op ((Over.map p).obj (Y i₁)))) →
                P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
            ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₁) :
          P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map φ.op) :
          (a : P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) →
            P.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map ((Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op) :
              (a : P.obj (op ((Over.map p).obj (Y i₂)))) →
                P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
            ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₂) :
          P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) :
      P.obj (op Z))
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₁)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₂)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
have this₁ : Eq (α := P.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) sorry)).op) :
        (a : P.obj (op ((Over.map p).obj (Y i₁)))) → P.obj (op Z))
      ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₁) :
    P.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) sorry)).op) :
        (a : P.obj (op ((Over.map p).obj (Y i₂)))) → P.obj (op Z))
      ((↑s : (i : I) → P.obj (op ((Over.map p).obj (Y i)))) i₂) :
    P.obj (op Z))
Tactic: simp only [← comp_apply, ← Functor.map_comp, ← op_comp] at this
Cleared hypotheses: this