awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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 : ι
⊢ 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:
simp [Cofan.inj, e]

Premises used: CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
⊢ (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])
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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))
rw₁ 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))
⊢ 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 [← this, Presheaf.isLocallySurjective_comp_iff J]

Premises used: CategoryTheory.Presheaf.isLocallySurjective_comp_iff
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
⊢ Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (F := ∐ fun (i : ι) ↦ obj shrinkYoneda.{w, v, u} (X i)) (G :=
      obj shrinkYoneda.{w, v, u} S) (Sigma.desc fun (i : ι) ↦ map shrinkYoneda.{w, v, u} (f i))

Tactic:
ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map J f
    (coproductIsCoproduct _)

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, CategoryTheory.Limits.colimit.desc, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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
⊢ Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S ↔
    Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) (F := ∐ fun (i : ι) ↦ obj uliftYoneda.{w, v, u} (X i)) (G :=
      obj uliftYoneda.{w, v, u} S) (Sigma.desc fun (i : ι) ↦ map uliftYoneda.{w, v, u} (f i))

Tactic:
ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map J f
    (coproductIsCoproduct _)

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, CategoryTheory.Limits.colimit.desc, CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map, CategoryTheory.Limits.colimit.ι
-- 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₁₃
H : ∀ (F : Sheaf J (Type v)), (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).IsPullback
rw : ∀ (X : Sheaf J (Type v)), ((sq.map (yoneda ⋙ presheafToSheaf J (Type v))).op.map (Functor.obj yoneda X)).IsPullback
⊢ (sq.map (yoneda ⋙ presheafToSheaf J (Type v))).IsPushout

Tactic:
rw [Square.isPushout_iff_op_map_yoneda_isPullback]

Premises used: CategoryTheory.Square.isPushout_iff_op_map_yoneda_isPullback
-- 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₁₃
H : ∀ (F : Sheaf J (Type v)), (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).IsPullback
F : Sheaf J (Type v)
⊢ ((sq.map (yoneda ⋙ presheafToSheaf J (Type v))).op.map (Functor.obj yoneda F)).IsPullback

Tactic:
(F.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff sq).2 (H F)

Premises used: Iff.mpr, CategoryTheory.Square.op, CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Square.map
-- 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₁₃
H : ∀ (F : Sheaf J (Type v)), (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).IsPullback
F : Sheaf J (Type v)
⊢ ((sq.map (yoneda ⋙ presheafToSheaf J (Type v))).op.map (Functor.obj yoneda F)).IsPullback

Tactic:
exact (F.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff sq).2 (H F)

Premises used: Iff.mpr, CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff
-- 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 : IsLimit (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).pullbackCone
⊢ (sq.op.map (F.obj (P := Presheaf.IsSheaf J))).IsPullback

Tactic:
apply Square.IsPullback.mk

Premises used: CategoryTheory.Square.IsPullback.mk
-- 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 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₃₄)
⊢ a = b

Tactic:
simpa only [← cancel_mono sq.f₂₄] using fac

Premises used: CategoryTheory.Square.f₂₄, CategoryTheory.cancel_mono
-- 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 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₃₄)
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)
⊢ 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)

Tactic:
obtain rfl : a = b := by simpa only [← cancel_mono sq.f₂₄] using fac

Premises used: rfl
-- 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.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:
rfl
-- 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
φ : 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:
simpa using s.condition =≫ F.obj.map φ.op

Premises used: CategoryTheory.Limits.PullbackCone.condition, Quiver.Hom.op, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map
-- 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
φ : 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:
simpa using s.condition.symm =≫ F.obj.map φ.op

Premises used: CategoryTheory.Limits.PullbackCone.condition, Quiver.Hom.op, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, Eq.symm
-- 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 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.right
        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₃₄)
⊢ a = b

Tactic:
simpa only [← cancel_mono sq.f₃₄] using fac

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Square.f₃₄
-- 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 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.right
        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₃₄)
right :
  ∀
    (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₃₄)
        (a ≫
          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.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.right ≫
        F.obj (P := Presheaf.IsSheaf J).map a.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.right ≫
      F.obj (P := Presheaf.IsSheaf J).map b.op)

Tactic:
obtain rfl : a = b := by simpa only [← cancel_mono sq.f₃₄] using fac

Premises used: rfl