-- 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)
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
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₃₄) ↦
          (⋯.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₄)))
        s
⊢ IsLimit (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).pullbackCone

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₂ ↦ ?_)

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows, CategoryTheory.Square.f₂₄, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.PullbackCone.IsLimit.mk, CategoryTheory.Square.f₃₄, CategoryTheory.Limits.WalkingPair.casesOn