awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
U : C
u : unop (op U) ⟶ S
hf :
  Membership.mem (γ := Set (Sieve.{v, u} (unop (op U)))) ((J : (a : C) → Set (Sieve a)) (unop (op U)))
    (Sieve.pullback u (Sieve.ofArrows X f))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) u) ∈
    (J : (a : C) → Set (Sieve a)) U
have refine_1 : ∀
  (hf :
    Membership.mem (γ := Set (Sieve.{v, u} (unop (op U)))) ((J : (a : C) → Set (Sieve a)) (unop (op U)))
      (Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
        (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop (op (unop (op U))) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op (unop (op U))))
          u))),
  Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op U)) u) ∈
    (J : (a : C) → Set (Sieve a)) U
Tactic: rwa [← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc u] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst_2 : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)
hc : IsColimit c
hf :
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
    (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
⊢ Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
have refine_2 : Presheaf.imageSieve (FA := TypeCat.Fun) (G := obj shrinkYoneda.{w, v, u} S)
    (Cofan.IsColimit.desc hc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op S) ⟶ S) → (shrinkYoneda.{w, v, u}.obj S).obj (op S)) (𝟙 S)) ∈
  (J : (a : C) → Set (Sieve a)) S
Tactic: rw [← Sieve.pullback_id (S := Sieve.ofArrows X f),
      ← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc (𝟙 S)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Cᵒᵖ ⥤ Type (max w v)) fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i)
hc : IsColimit c
e : Iso (C := Discrete ι ⥤ Cᵒᵖ ⥤ Type (max w v)) (Discrete.functor fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i))
  (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{max w v, v, u} (X i)) :=
  Discrete.natIso fun (i : Discrete ι) ↦ Iso.app uliftYonedaIsoShrinkYoneda (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
⊢ Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))
have rw : Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{max w v, v, u} S)
    (Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max w v, v, u} (f i)) ↔
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
    (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))
Tactic: rw [ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map.{max w v} J f hc']
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Cᵒᵖ ⥤ Type (max w v)) fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i)
hc : IsColimit c
e : Iso (C := Discrete ι ⥤ Cᵒᵖ ⥤ Type (max w v)) (Discrete.functor fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i))
  (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{max w v, v, u} (X i)) :=
  Discrete.natIso fun (i : Discrete ι) ↦ Iso.app uliftYonedaIsoShrinkYoneda (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
i : ι
⊢ c.inj i ≫
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i)) ≫
        NatTrans.app (Iso.hom uliftYonedaIsoShrinkYoneda) S =
    c.inj i ≫ Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max v w, v, u} (f i)
have rw : Eq (α := Quiver.Hom (V := Cᵒᵖ ⥤ Type (max w v)) (obj uliftYoneda.{w, v, u} (X i)) (obj shrinkYoneda.{max w v, v, u} S))
  (NatTrans.app (Iso.hom uliftYonedaIsoShrinkYoneda) (X i) ≫
    Cofan.inj ((Cocone.precompose e.inv).obj c) i ≫
      Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max v w, v, u} (f i))
  (c.inj i ≫ Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max v w, v, u} (f i))
Tactic: rw [Cofan.IsColimit.fac_assoc, NatTrans.naturality,
        ← Cofan.IsColimit.fac hc' (fun i ↦ shrinkYoneda.map (f i)) i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Cᵒᵖ ⥤ Type (max w v)) fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i)
hc : IsColimit c
e : Iso (C := Discrete ι ⥤ Cᵒᵖ ⥤ Type (max w v)) (Discrete.functor fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i))
  (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{max w v, v, u} (X i)) :=
  Discrete.natIso fun (i : Discrete ι) ↦ Iso.app uliftYonedaIsoShrinkYoneda (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{max w v, v, u} S)
      (Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max w v, v, u} (f i)) ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))
have this : (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i)) ≫
    NatTrans.app (Iso.hom uliftYonedaIsoShrinkYoneda) S =
  Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max v w, v, u} (f i)
Tactic: have :
      Cofan.IsColimit.desc hc (fun i ↦ uliftYoneda.map (f i)) ≫
        uliftYonedaIsoShrinkYoneda.hom.app _ =
      Cofan.IsColimit.desc hc' (fun i ↦ shrinkYoneda.map (f i)) :=
    Cofan.IsColimit.hom_ext hc _ _ (fun i ↦ by
      rw [Cofan.IsColimit.fac_assoc, NatTrans.naturality,
        ← Cofan.IsColimit.fac hc' (fun i ↦ shrinkYoneda.map (f i)) i]
      simp [Cofan.inj, e])
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Cᵒᵖ ⥤ Type (max w v)) fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i)
hc : IsColimit c
e : Iso (C := Discrete ι ⥤ Cᵒᵖ ⥤ Type (max w v)) (Discrete.functor fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i))
  (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{max w v, v, u} (X i)) :=
  Discrete.natIso fun (i : Discrete ι) ↦ Iso.app uliftYonedaIsoShrinkYoneda (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
this :
  (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i)) ≫
      NatTrans.app (Iso.hom uliftYonedaIsoShrinkYoneda) S =
    Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max v w, v, u} (f i)
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{max w v, v, u} S)
      (Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max w v, v, u} (f i)) ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))
have rw : Presheaf.IsLocallySurjective J (FA := TypeCat.Fun)
    ((Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i)) ≫
      NatTrans.app (Iso.hom uliftYonedaIsoShrinkYoneda) S) ↔
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
    (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))
Tactic: rw [← this, Presheaf.isLocallySurjective_comp_iff J]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S : C
ι : Type u_2
inst_1 : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan (C := Cᵒᵖ ⥤ Type (max w v)) fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i)
hc : IsColimit c
e : Iso (C := Discrete ι ⥤ Cᵒᵖ ⥤ Type (max w v)) (Discrete.functor fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i))
  (Discrete.functor fun (i : ι) ↦ obj shrinkYoneda.{max w v, v, u} (X i)) :=
  Discrete.natIso fun (i : Discrete ι) ↦ Iso.app uliftYonedaIsoShrinkYoneda (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
this :
  (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i)) ≫
      NatTrans.app (Iso.hom uliftYonedaIsoShrinkYoneda) S =
    Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max v w, v, u} (f i)
rw :
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun)
      ((Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i)) ≫
        NatTrans.app (Iso.hom uliftYonedaIsoShrinkYoneda) S) ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj shrinkYoneda.{max w v, v, u} S)
      (Cofan.IsColimit.desc hc' fun (i : ι) ↦ map shrinkYoneda.{max w v, v, u} (f i)) ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
      (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))
have rw₁ : Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
    (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i)) ↔
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (G := obj uliftYoneda.{w, v, u} S)
    (Cofan.IsColimit.desc hc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))
Tactic: rw [← this, Presheaf.isLocallySurjective_comp_iff J]
-- 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₁₃
H : ∀ (F : Sheaf J (Type v)), (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).IsPullback
⊢ (sq.map (yoneda ⋙ presheafToSheaf J (Type v))).IsPushout
have rw : ∀ (X : Sheaf J (Type v)), ((sq.map (yoneda ⋙ presheafToSheaf J (Type v))).op.map (Functor.obj yoneda X)).IsPullback
Tactic: rw [Square.isPushout_iff_op_map_yoneda_isPullback]
-- 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)
⊢ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).IsPullback
have h : IsLimit (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).pullbackCone
Tactic: apply Square.IsPullback.mk
-- 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)
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 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.left 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₃₄)
⊢ 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.left ≫
      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)
have left : ∀
  (fac :
    Eq (α := W ⟶ sq.X₄)
      (a ≫
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left
          sq.f₂₄ sq.f₃₄)
      (a ≫
        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.left ≫
      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 a.op)
Tactic: obtain rfl : a = b := by simpa only [← cancel_mono sq.f₂₄] using fac
Cleared hypotheses: b, fac
-- 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)
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.left
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac :
  Eq (α := W ⟶ sq.X₄)
    (a ≫
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left sq.f₂₄
        sq.f₃₄)
    (b ≫
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
        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.left ≫
      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.right ≫
      F.obj (P := Presheaf.IsSheaf J).map b.op)
have left : ∀ (φ : W ⟶ sq.pullbackCone.pt)
  (fac :
    Eq (α := W ⟶ sq.X₄)
      ((φ ≫ sq.pullbackCone.fst) ≫
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.left
          sq.f₂₄ sq.f₃₄)
      ((φ ≫ sq.pullbackCone.snd) ≫
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction sq.X₂ sq.X₃ x ⟶ sq.X₄) WalkingPair.right
          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.left ≫
      F.obj (P := Presheaf.IsSheaf J).map (φ ≫ sq.pullbackCone.fst).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.right ≫
      F.obj (P := Presheaf.IsSheaf J).map (φ ≫ sq.pullbackCone.snd).op)
Tactic: obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac
Cleared hypotheses: a, b, fac
-- 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)
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₃₄)
⊢ 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)
have 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)
Tactic: obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac.symm
Cleared hypotheses: a, b, fac