-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MayerVietorisSquare (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
sq : Square.{v, u} C
inst_2 : Mono sq.f₂₄
inst_3 : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ :
  Membership.mem (γ := Set (Sieve.{v, u} sq.X₄)) ((J : (a : C) → Set (Sieve a)) sq.X₄) (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄)
this : Mono sq.f₁₃
F : Sheaf J (Type v)
h :
  ∀
    (x :
      PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄),
    (fun
              (s :
                PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
                  (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
            (⋯.amalgamateOfArrows
                (fun (k : WalkingPair) ↦
                  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                    sq.f₃₄)
                h₂
                (fun (j : WalkingPair) ↦
                  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                    s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
                ⋯ :
              s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
          x ≫
        (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ =
      x.fst
h₃ :
  ∀
    (x :
      PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄),
    (fun
              (s :
                PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
                  (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
            (⋯.amalgamateOfArrows
                (fun (k : WalkingPair) ↦
                  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                    sq.f₃₄)
                h₂
                (fun (j : WalkingPair) ↦
                  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                    s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
                ⋯ :
              s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
          x ≫
        (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ =
      x.snd
⊢ IsLimit (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).pullbackCone
have h₄ : ∀ (s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄)
  (m : s.pt ⟶ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).X₁)
  (hm₁ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₂ = s.fst)
  (hm₂ : m ≫ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₁₃ = s.snd),
  m =
    (fun
          (s :
            PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄
              (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄) ↦
        (sorry.amalgamateOfArrows
            (fun (k : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) k sq.f₂₄
                sq.f₃₄)
            h₂
            (fun (j : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op (pairFunction sq.X₂ sq.X₃ x))) j s.fst s.snd)
            sorry :
          s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op sq.X₄)))
      s
Tactic: refine PullbackCone.IsLimit.mk _
      (fun s ↦ F.2.amalgamateOfArrows _ h₂
        (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
        (fun W ↦ by
          rintro (_ | _) (_ | _) a b fac
          · obtain rfl : a = b := by simpa only [← cancel_mono sq.f₂₄] using fac
            rfl
          · obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac
            simpa using s.condition =≫ F.obj.map φ.op
          · obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac.symm
            simpa using s.condition.symm =≫ F.obj.map φ.op
          · obtain rfl : a = b := by simpa only [← cancel_mono sq.f₃₄] using fac
            rfl)) (fun _ ↦ ?_) (fun _ ↦ ?_) (fun s m hm₁ hm₂ ↦ ?_)