-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
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)
s : PullbackCone (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₂₄ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
fac :
  Eq (α := W ⟶ sq.X₄)
    (a ≫
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
        sq.f₂₄ sq.f₃₄)
    (b ≫
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left sq.f₂₄
        sq.f₃₄)
right :
  ∀ (φ : W ⟶ sq.pullbackCone.pt)
    (fac :
      Eq (α := W ⟶ sq.X₄)
        ((φ ≫ sq.pullbackCone.snd) ≫
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
            sq.f₂₄ sq.f₃₄)
        ((φ ≫ sq.pullbackCone.fst) ≫
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left
            sq.f₂₄ sq.f₃₄)),
    Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op W))
      ((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 (pairFunction sq.X₂ sq.X₃ j))))
          WalkingPair.right ≫
        F.obj (P := Presheaf.IsSheaf J).map (φ ≫ sq.pullbackCone.snd).op)
      ((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 (pairFunction sq.X₂ sq.X₃ j))))
          WalkingPair.left ≫
        F.obj (P := Presheaf.IsSheaf J).map (φ ≫ sq.pullbackCone.fst).op)
⊢ Eq (α := s.pt ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op W))
    ((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 (pairFunction sq.X₂ sq.X₃ j))))
        WalkingPair.right ≫
      F.obj (P := Presheaf.IsSheaf J).map a.op)
    ((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 (pairFunction sq.X₂ sq.X₃ j))))
        WalkingPair.left ≫
      F.obj (P := Presheaf.IsSheaf J).map b.op)

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac.symm

Premises used: CategoryTheory.Square.IsPullback.isLimit, CategoryTheory.Limits.PullbackCone.IsLimit.lift', Eq.symm, rfl